Deje que$a,b \in$ group$G$, de manera que$ab^3a^{-1}=b^2, b^{-1}a^2b=a^3$ pruebe que$a=b=e$ (identidad)

Question

Obtuve$ab^3=b^2a$ y$a^2b=ba^3$ al deshacerme de los inversos a través de la composición en ambos lados.

Intenté escribir$a=aaa^{-1}$, lo cual no ayudó. ¿Alguna sugerencia por favor?

Answer 1

Estoy utilizando comprobadores de teoremas automáticos, específicamente Prover 9 puede obtener la prueba con el siguiente código:

 cnf(left_identity,axiom,
( multiply(identity,X) = X )).


cnf(left_inverse,axiom,
    ( multiply(inverse(X),X) = identity )).


cnf(associativity,axiom,
    ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) )).


cnf(axio1,axiom,
   (multiply(multiply(a,multiply(b,multiply(b,b))),inverse(a)) = multiply(b,b)           )).

cnf(axio2,axiom,
  (multiply(inverse(b),multiply(multiply(a,a),b)) = multiply(a,multiply(a,a) )      )).

cnf(goal1,negated_conjecture,
 (  a != identity  )).
 

La prueba automática generada por Prover 9 es

     1 multiply(identity,A) = A # label(left_identity) # label(axiom).  [assumption].
2 multiply(inverse(A),A) = identity # label(left_inverse) # label(axiom).  [assumption].
3 multiply(multiply(A,B),C) = multiply(A,multiply(B,C)) # label(associativity) # label(axiom).  [assumption].
4 multiply(multiply(a,multiply(b,multiply(b,b))),inverse(a)) = multiply(b,b) # label(axio1) # label(axiom).  [assumption].
5 multiply(a,multiply(b,multiply(b,multiply(b,inverse(a))))) = multiply(b,b).  [copy(4),rewrite([3(10),3(9),3(8)])].
6 multiply(inverse(b),multiply(multiply(a,a),b)) = multiply(a,multiply(a,a)) # label(axio2) # label(axiom).  [assumption].
7 multiply(inverse(b),multiply(a,multiply(a,b))) = multiply(a,multiply(a,a)).  [copy(6),rewrite([3(7)])].
8 a != identity # label(goal1) # label(negated_conjecture) # answer(goal1).  [assumption].
9 identity != a # answer(goal1).  [copy(8),flip(a)].
10 multiply(inverse(A),multiply(A,B)) = B.  [para(2(a,1),3(a,1,1)),rewrite([1(2)]),flip(a)].
11 multiply(a,multiply(b,multiply(b,multiply(b,multiply(inverse(a),A))))) = multiply(b,multiply(b,A)).  [para(5(a,1),3(a,1,1)),rewrite([3(4),3(14),3(13),3(12)]),flip(a)].
12 multiply(inverse(b),multiply(a,multiply(a,multiply(b,A)))) = multiply(a,multiply(a,multiply(a,A))).  [para(7(a,1),3(a,1,1)),rewrite([3(6),3(5),3(14),3(13)]),flip(a)].
14 multiply(inverse(inverse(A)),identity) = A.  [para(2(a,1),10(a,1,2))].
16 multiply(b,multiply(b,multiply(b,inverse(a)))) = multiply(inverse(a),multiply(b,b)).  [para(5(a,1),10(a,1,2)),flip(a)].
17 multiply(inverse(inverse(b)),multiply(a,multiply(a,a))) = multiply(a,multiply(a,b)).  [para(7(a,1),10(a,1,2))].
18 multiply(inverse(inverse(A)),B) = multiply(A,B).  [para(10(a,1),10(a,1,2))].
20 multiply(b,multiply(a,multiply(a,a))) = multiply(a,multiply(a,b)).  [back_rewrite(17),rewrite([18(9)])].
21 multiply(A,identity) = A.  [back_rewrite(14),rewrite([18(4)])].
23 multiply(A,inverse(A)) = identity.  [para(18(a,1),2(a,1))].
24 multiply(A,multiply(inverse(A),B)) = B.  [para(18(a,1),10(a,1))].
25 inverse(inverse(A)) = A.  [para(18(a,1),21(a,1)),rewrite([21(2)]),flip(a)].
27 multiply(b,multiply(b,multiply(b,multiply(inverse(a),A)))) = multiply(inverse(a),multiply(b,multiply(b,A))).  [para(11(a,1),10(a,1,2)),flip(a)].
28 multiply(a,multiply(b,multiply(b,multiply(b,A)))) = multiply(b,multiply(b,multiply(a,A))).  [para(10(a,1),11(a,1,2,2,2,2))].
29 multiply(A,multiply(B,inverse(multiply(A,B)))) = identity.  [para(23(a,1),3(a,1)),flip(a)].
32 multiply(A,inverse(multiply(B,A))) = inverse(B).  [para(29(a,1),10(a,1,2)),rewrite([21(3)]),flip(a)].
37 inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)).  [para(32(a,1),10(a,1,2)),flip(a)].
39 multiply(b,multiply(a,multiply(a,multiply(a,A)))) = multiply(a,multiply(a,multiply(b,A))).  [para(12(a,1),10(a,1,2)),rewrite([25(3)])].
40 multiply(a,multiply(a,multiply(a,inverse(b)))) = multiply(inverse(b),multiply(a,a)).  [para(23(a,1),12(a,1,2,2,2)),rewrite([21(6)]),flip(a)].
41 multiply(a,multiply(a,multiply(a,multiply(inverse(b),A)))) = multiply(inverse(b),multiply(a,multiply(a,A))).  [para(24(a,1),12(a,1,2,2,2)),flip(a)].
51 multiply(inverse(b),multiply(inverse(a),multiply(b,b))) = multiply(b,multiply(b,inverse(a))).  [para(16(a,1),10(a,1,2))].
53 multiply(a,multiply(inverse(b),multiply(inverse(b),inverse(b)))) = multiply(inverse(b),multiply(inverse(b),a)).  [para(16(a,1),37(a,1,1)),rewrite([37(7),37(4),25(8),3(7),37(14),37(12),25(10),3(14),3(17),3(16)]),flip(a)].
54 multiply(inverse(a),multiply(inverse(b),multiply(a,a))) = multiply(a,multiply(a,inverse(b))).  [para(40(a,1),10(a,1,2))].
56 multiply(inverse(b),multiply(inverse(a),multiply(b,multiply(b,A)))) = multiply(b,multiply(b,multiply(inverse(a),A))).  [para(51(a,1),3(a,1,1)),rewrite([3(7),3(6),3(16),3(15)]),flip(a)].
57 multiply(inverse(b),multiply(inverse(b),multiply(a,b))) = multiply(a,multiply(inverse(b),inverse(b))).  [para(51(a,1),37(a,1,1)),rewrite([37(7),37(5),25(3),3(7),37(14),37(11),25(15),3(14),25(17),3(16),3(15)]),flip(a)].
60 multiply(b,multiply(b,multiply(a,inverse(b)))) = multiply(a,multiply(b,b)).  [para(23(a,1),28(a,1,2,2,2)),rewrite([21(5)]),flip(a)].
62 multiply(inverse(b),multiply(a,multiply(b,multiply(b,multiply(a,A))))) = multiply(a,multiply(a,multiply(a,multiply(b,multiply(b,A))))).  [para(28(a,1),12(a,1,2,2))].
65 multiply(b,multiply(b,multiply(a,multiply(b,inverse(a))))) = multiply(a,multiply(b,multiply(inverse(a),multiply(b,b)))).  [para(16(a,1),28(a,1,2,2)),flip(a)].
67 multiply(inverse(a),multiply(b,multiply(a,multiply(a,b)))) = multiply(b,multiply(b,multiply(b,multiply(a,a)))).  [para(20(a,1),27(a,2,2,2)),rewrite([10(11)]),flip(a)].
69 multiply(b,multiply(b,multiply(b,multiply(a,multiply(a,inverse(b)))))) = multiply(inverse(a),multiply(b,multiply(a,a))).  [para(54(a,1),27(a,1,2,2,2)),rewrite([24(23)])].
72 multiply(inverse(b),multiply(a,multiply(b,b))) = multiply(b,multiply(a,inverse(b))).  [para(60(a,1),10(a,1,2))].
76 multiply(b,multiply(b,multiply(a,multiply(a,inverse(b))))) = multiply(a,multiply(b,multiply(a,multiply(b,b)))).  [para(60(a,1),28(a,1,2,2)),flip(a)].
78 multiply(b,multiply(a,multiply(b,multiply(a,multiply(b,b))))) = multiply(inverse(a),multiply(b,multiply(a,a))).  [back_rewrite(69),rewrite([76(11)])].
79 multiply(inverse(b),multiply(a,multiply(b,multiply(b,A)))) = multiply(b,multiply(a,multiply(inverse(b),A))).  [para(72(a,1),3(a,1,1)),rewrite([3(7),3(6),3(15),3(14)]),flip(a)].
82 multiply(a,multiply(a,multiply(a,multiply(b,multiply(b,A))))) = multiply(b,multiply(a,multiply(inverse(b),multiply(a,A)))).  [back_rewrite(62),rewrite([79(11)]),flip(a)].
85 multiply(a,multiply(a,multiply(b,inverse(a)))) = multiply(b,multiply(a,a)).  [para(23(a,1),39(a,1,2,2,2)),rewrite([21(5)]),flip(a)].
94 multiply(inverse(a),multiply(b,multiply(a,a))) = multiply(a,multiply(b,inverse(a))).  [para(85(a,1),10(a,1,2))].
99 multiply(b,multiply(a,multiply(b,multiply(a,multiply(b,b))))) = multiply(a,multiply(b,inverse(a))).  [back_rewrite(78),rewrite([94(19)])].
102 multiply(inverse(a),multiply(b,multiply(a,multiply(a,A)))) = multiply(a,multiply(b,multiply(inverse(a),A))).  [para(94(a,1),3(a,1,1)),rewrite([3(7),3(6),3(15),3(14)]),flip(a)].
106 multiply(b,multiply(b,multiply(b,multiply(a,a)))) = multiply(a,multiply(b,multiply(inverse(a),b))).  [back_rewrite(67),rewrite([102(10)]),flip(a)].
108 multiply(inverse(b),multiply(inverse(b),multiply(a,multiply(b,A)))) = multiply(a,multiply(inverse(b),multiply(inverse(b),A))).  [para(57(a,1),3(a,1,1)),rewrite([3(8),3(7),3(17),3(16)]),flip(a)].
110 multiply(inverse(b),multiply(a,multiply(a,multiply(inverse(b),multiply(a,b))))) = multiply(a,multiply(inverse(b),multiply(a,multiply(a,inverse(b))))).  [para(57(a,1),41(a,1,2,2,2)),rewrite([41(12)]),flip(a)].
136 multiply(a,multiply(inverse(b),multiply(inverse(b),multiply(inverse(b),A)))) = multiply(inverse(b),multiply(inverse(b),multiply(a,A))).  [para(53(a,1),3(a,1,1)),rewrite([3(8),3(7),3(18),3(17)]),flip(a)].
139 multiply(a,multiply(a,multiply(inverse(b),multiply(inverse(b),multiply(a,inverse(b)))))) = multiply(inverse(b),multiply(a,multiply(inverse(b),multiply(inverse(b),a)))).  [para(53(a,1),41(a,2,2,2)),rewrite([136(15)])].
166 multiply(a,multiply(b,multiply(a,multiply(b,b)))) = multiply(inverse(b),multiply(a,multiply(b,inverse(a)))).  [para(99(a,1),10(a,1,2)),flip(a)].
186 multiply(b,multiply(a,multiply(a,inverse(b)))) = multiply(a,multiply(inverse(b),multiply(inverse(b),inverse(a)))).  [para(60(a,1),79(a,1,2,2,2)),rewrite([166(11),108(12),10(21)]),flip(a)].
187 multiply(b,multiply(a,multiply(inverse(b),multiply(a,inverse(b))))) = multiply(a,multiply(a,multiply(a,b))).  [para(60(a,1),79(a,1,2,2)),rewrite([12(10)]),flip(a)].
206 multiply(a,multiply(b,multiply(inverse(a),multiply(b,b)))) = multiply(inverse(a),b).  [para(94(a,1),56(a,2,2,2)),rewrite([106(13),10(13),10(9),65(14)]),flip(a)].
219 multiply(a,multiply(a,multiply(b,b))) = identity.  [para(206(a,1),12(a,1,2,2)),rewrite([24(8),2(4),24(11)]),flip(a)].
233 multiply(a,multiply(a,multiply(b,multiply(b,A)))) = A.  [para(219(a,1),3(a,1,1)),rewrite([1(2),3(7),3(6)]),flip(a)].
234 multiply(a,multiply(b,b)) = inverse(a).  [para(219(a,1),10(a,1,2)),rewrite([21(4)]),flip(a)].
235 multiply(a,multiply(a,multiply(a,b))) = inverse(b).  [para(219(a,1),12(a,1,2)),rewrite([21(4)]),flip(a)].
244 multiply(b,multiply(a,multiply(inverse(b),multiply(a,A)))) = multiply(a,A).  [back_rewrite(82),rewrite([233(9)]),flip(a)].
249 multiply(b,multiply(a,inverse(b))) = multiply(inverse(b),inverse(a)).  [back_rewrite(72),rewrite([234(7)]),flip(a)].
250 multiply(a,inverse(b)) = inverse(b).  [back_rewrite(187),rewrite([244(11),235(11)])].
264 multiply(inverse(b),inverse(a)) = identity.  [back_rewrite(249),rewrite([250(5),23(4)]),flip(a)].
265 inverse(b) = identity.  [back_rewrite(186),rewrite([250(6),250(5),23(4),264(9),21(6),250(5)]),flip(a)].
266 multiply(a,multiply(a,a)) = multiply(a,a).  [back_rewrite(139),rewrite([265(4),265(5),265(7),21(7),1(6),1(5),265(7),265(9),265(10),1(11),1(10),1(10)])].
267 multiply(a,a) = identity.  [back_rewrite(110),rewrite([265(2),265(5),1(8),235(8),265(3),21(3),265(4),265(7),21(7),1(7),266(6)]),flip(a)].
269 identity = a.  [back_rewrite(40),rewrite([265(5),21(5),267(4),21(3),265(3),267(5),21(4)]),flip(a)].
270 $F # answer(goal1).  [resolve(269,a,9,a)].

% SZS output end Refutation
 

Answer 2

Sugerencia: intente comenzar con$ab^3= b^2a$ y solo multiplique$a$ 's al final, intente obtener siempre$ba^3$ para reemplazarlo con$a^2b$ e intente simplificar a una expresión mínima y repetir.