Metamath Proof Explorer

Theorem mndpropd

Description: If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses mndpropd.1 
|- ( ph -> B = ( Base ` K ) )
mndpropd.2 
|- ( ph -> B = ( Base ` L ) )
mndpropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
Assertion mndpropd 
|- ( ph -> ( K e. Mnd <-> L e. Mnd ) )

Proof

Step Hyp Ref Expression
1 mndpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 mndpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 mndpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 simplr 
 |-  ( ( ( ph /\ K e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> K e. Mnd )
5 simprl 
 |-  ( ( ( ph /\ K e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> x e. B )
6 1 ad2antrr 
 |-  ( ( ( ph /\ K e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> B = ( Base ` K ) )
7 5 6 eleqtrd 
 |-  ( ( ( ph /\ K e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> x e. ( Base ` K ) )
8 simprr 
 |-  ( ( ( ph /\ K e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> y e. B )
9 8 6 eleqtrd 
 |-  ( ( ( ph /\ K e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> y e. ( Base ` K ) )
10 eqid 
 |-  ( Base ` K ) = ( Base ` K )
11 eqid 
 |-  ( +g ` K ) = ( +g ` K )
12 10 11 mndcl 
 |-  ( ( K e. Mnd /\ x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> ( x ( +g ` K ) y ) e. ( Base ` K ) )
13 4 7 9 12 syl3anc 
 |-  ( ( ( ph /\ K e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) e. ( Base ` K ) )
14 13 6 eleqtrrd 
 |-  ( ( ( ph /\ K e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) e. B )
15 14 ralrimivva 
 |-  ( ( ph /\ K e. Mnd ) -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B )
16 15 ex 
 |-  ( ph -> ( K e. Mnd -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) )
17 simplr 
 |-  ( ( ( ph /\ L e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> L e. Mnd )
18 simprl 
 |-  ( ( ( ph /\ L e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> x e. B )
19 2 ad2antrr 
 |-  ( ( ( ph /\ L e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> B = ( Base ` L ) )
20 18 19 eleqtrd 
 |-  ( ( ( ph /\ L e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> x e. ( Base ` L ) )
21 simprr 
 |-  ( ( ( ph /\ L e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> y e. B )
22 21 19 eleqtrd 
 |-  ( ( ( ph /\ L e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> y e. ( Base ` L ) )
23 eqid 
 |-  ( Base ` L ) = ( Base ` L )
24 eqid 
 |-  ( +g ` L ) = ( +g ` L )
25 23 24 mndcl 
 |-  ( ( L e. Mnd /\ x e. ( Base ` L ) /\ y e. ( Base ` L ) ) -> ( x ( +g ` L ) y ) e. ( Base ` L ) )
26 17 20 22 25 syl3anc 
 |-  ( ( ( ph /\ L e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` L ) y ) e. ( Base ` L ) )
27 3 adantlr 
 |-  ( ( ( ph /\ L e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
28 26 27 19 3eltr4d 
 |-  ( ( ( ph /\ L e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) e. B )
29 28 ralrimivva 
 |-  ( ( ph /\ L e. Mnd ) -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B )
30 29 ex 
 |-  ( ph -> ( L e. Mnd -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) )
31 3 oveqrspc2v 
 |-  ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) )
32 31 adantlr 
 |-  ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) )
33 32 eleq1d 
 |-  ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) -> ( ( u ( +g ` K ) v ) e. B <-> ( u ( +g ` L ) v ) e. B ) )
34 simplll 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ph )
35 simplrl 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> u e. B )
36 simplrr 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> v e. B )
37 simpllr 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B )
38 ovrspc2v 
 |-  ( ( ( u e. B /\ v e. B ) /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( u ( +g ` K ) v ) e. B )
39 35 36 37 38 syl21anc 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( u ( +g ` K ) v ) e. B )
40 simpr 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> w e. B )
41 3 oveqrspc2v 
 |-  ( ( ph /\ ( ( u ( +g ` K ) v ) e. B /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( ( u ( +g ` K ) v ) ( +g ` L ) w ) )
42 34 39 40 41 syl12anc 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( ( u ( +g ` K ) v ) ( +g ` L ) w ) )
43 34 35 36 31 syl12anc 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) )
44 43 oveq1d 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( ( u ( +g ` K ) v ) ( +g ` L ) w ) = ( ( u ( +g ` L ) v ) ( +g ` L ) w ) )
45 42 44 eqtrd 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( ( u ( +g ` L ) v ) ( +g ` L ) w ) )
46 ovrspc2v 
 |-  ( ( ( v e. B /\ w e. B ) /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( v ( +g ` K ) w ) e. B )
47 36 40 37 46 syl21anc 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( v ( +g ` K ) w ) e. B )
48 3 oveqrspc2v 
 |-  ( ( ph /\ ( u e. B /\ ( v ( +g ` K ) w ) e. B ) ) -> ( u ( +g ` K ) ( v ( +g ` K ) w ) ) = ( u ( +g ` L ) ( v ( +g ` K ) w ) ) )
49 34 35 47 48 syl12anc 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( u ( +g ` K ) ( v ( +g ` K ) w ) ) = ( u ( +g ` L ) ( v ( +g ` K ) w ) ) )
50 3 oveqrspc2v 
 |-  ( ( ph /\ ( v e. B /\ w e. B ) ) -> ( v ( +g ` K ) w ) = ( v ( +g ` L ) w ) )
51 34 36 40 50 syl12anc 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( v ( +g ` K ) w ) = ( v ( +g ` L ) w ) )
52 51 oveq2d 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( u ( +g ` L ) ( v ( +g ` K ) w ) ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) )
53 49 52 eqtrd 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( u ( +g ` K ) ( v ( +g ` K ) w ) ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) )
54 45 53 eqeq12d 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) <-> ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) )
55 54 ralbidva 
 |-  ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) -> ( A. w e. B ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) <-> A. w e. B ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) )
56 33 55 anbi12d 
 |-  ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ ( u e. B /\ v e. B ) ) -> ( ( ( u ( +g ` K ) v ) e. B /\ A. w e. B ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) <-> ( ( u ( +g ` L ) v ) e. B /\ A. w e. B ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) ) )
57 56 2ralbidva 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( A. u e. B A. v e. B ( ( u ( +g ` K ) v ) e. B /\ A. w e. B ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) <-> A. u e. B A. v e. B ( ( u ( +g ` L ) v ) e. B /\ A. w e. B ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) ) )
58 1 adantr 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> B = ( Base ` K ) )
59 58 eleq2d 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( ( u ( +g ` K ) v ) e. B <-> ( u ( +g ` K ) v ) e. ( Base ` K ) ) )
60 58 raleqdv 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( A. w e. B ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) <-> A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) )
61 59 60 anbi12d 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( ( ( u ( +g ` K ) v ) e. B /\ A. w e. B ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) <-> ( ( u ( +g ` K ) v ) e. ( Base ` K ) /\ A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) ) )
62 58 61 raleqbidv 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( A. v e. B ( ( u ( +g ` K ) v ) e. B /\ A. w e. B ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) <-> A. v e. ( Base ` K ) ( ( u ( +g ` K ) v ) e. ( Base ` K ) /\ A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) ) )
63 58 62 raleqbidv 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( A. u e. B A. v e. B ( ( u ( +g ` K ) v ) e. B /\ A. w e. B ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( ( u ( +g ` K ) v ) e. ( Base ` K ) /\ A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) ) )
64 2 adantr 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> B = ( Base ` L ) )
65 64 eleq2d 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( ( u ( +g ` L ) v ) e. B <-> ( u ( +g ` L ) v ) e. ( Base ` L ) ) )
66 64 raleqdv 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( A. w e. B ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) <-> A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) )
67 65 66 anbi12d 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( ( ( u ( +g ` L ) v ) e. B /\ A. w e. B ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) <-> ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) ) )
68 64 67 raleqbidv 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( A. v e. B ( ( u ( +g ` L ) v ) e. B /\ A. w e. B ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) <-> A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) ) )
69 64 68 raleqbidv 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( A. u e. B A. v e. B ( ( u ( +g ` L ) v ) e. B /\ A. w e. B ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) ) )
70 57 63 69 3bitr3d 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( ( u ( +g ` K ) v ) e. ( Base ` K ) /\ A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) ) )
71 simplll 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ s e. B ) /\ u e. B ) -> ph )
72 simplr 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ s e. B ) /\ u e. B ) -> s e. B )
73 simpr 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ s e. B ) /\ u e. B ) -> u e. B )
74 3 oveqrspc2v 
 |-  ( ( ph /\ ( s e. B /\ u e. B ) ) -> ( s ( +g ` K ) u ) = ( s ( +g ` L ) u ) )
75 71 72 73 74 syl12anc 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ s e. B ) /\ u e. B ) -> ( s ( +g ` K ) u ) = ( s ( +g ` L ) u ) )
76 75 eqeq1d 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ s e. B ) /\ u e. B ) -> ( ( s ( +g ` K ) u ) = u <-> ( s ( +g ` L ) u ) = u ) )
77 3 oveqrspc2v 
 |-  ( ( ph /\ ( u e. B /\ s e. B ) ) -> ( u ( +g ` K ) s ) = ( u ( +g ` L ) s ) )
78 71 73 72 77 syl12anc 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ s e. B ) /\ u e. B ) -> ( u ( +g ` K ) s ) = ( u ( +g ` L ) s ) )
79 78 eqeq1d 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ s e. B ) /\ u e. B ) -> ( ( u ( +g ` K ) s ) = u <-> ( u ( +g ` L ) s ) = u ) )
80 76 79 anbi12d 
 |-  ( ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ s e. B ) /\ u e. B ) -> ( ( ( s ( +g ` K ) u ) = u /\ ( u ( +g ` K ) s ) = u ) <-> ( ( s ( +g ` L ) u ) = u /\ ( u ( +g ` L ) s ) = u ) ) )
81 80 ralbidva 
 |-  ( ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) /\ s e. B ) -> ( A. u e. B ( ( s ( +g ` K ) u ) = u /\ ( u ( +g ` K ) s ) = u ) <-> A. u e. B ( ( s ( +g ` L ) u ) = u /\ ( u ( +g ` L ) s ) = u ) ) )
82 81 rexbidva 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( E. s e. B A. u e. B ( ( s ( +g ` K ) u ) = u /\ ( u ( +g ` K ) s ) = u ) <-> E. s e. B A. u e. B ( ( s ( +g ` L ) u ) = u /\ ( u ( +g ` L ) s ) = u ) ) )
83 58 raleqdv 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( A. u e. B ( ( s ( +g ` K ) u ) = u /\ ( u ( +g ` K ) s ) = u ) <-> A. u e. ( Base ` K ) ( ( s ( +g ` K ) u ) = u /\ ( u ( +g ` K ) s ) = u ) ) )
84 58 83 rexeqbidv 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( E. s e. B A. u e. B ( ( s ( +g ` K ) u ) = u /\ ( u ( +g ` K ) s ) = u ) <-> E. s e. ( Base ` K ) A. u e. ( Base ` K ) ( ( s ( +g ` K ) u ) = u /\ ( u ( +g ` K ) s ) = u ) ) )
85 64 raleqdv 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( A. u e. B ( ( s ( +g ` L ) u ) = u /\ ( u ( +g ` L ) s ) = u ) <-> A. u e. ( Base ` L ) ( ( s ( +g ` L ) u ) = u /\ ( u ( +g ` L ) s ) = u ) ) )
86 64 85 rexeqbidv 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( E. s e. B A. u e. B ( ( s ( +g ` L ) u ) = u /\ ( u ( +g ` L ) s ) = u ) <-> E. s e. ( Base ` L ) A. u e. ( Base ` L ) ( ( s ( +g ` L ) u ) = u /\ ( u ( +g ` L ) s ) = u ) ) )
87 82 84 86 3bitr3d 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( E. s e. ( Base ` K ) A. u e. ( Base ` K ) ( ( s ( +g ` K ) u ) = u /\ ( u ( +g ` K ) s ) = u ) <-> E. s e. ( Base ` L ) A. u e. ( Base ` L ) ( ( s ( +g ` L ) u ) = u /\ ( u ( +g ` L ) s ) = u ) ) )
88 70 87 anbi12d 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( ( A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( ( u ( +g ` K ) v ) e. ( Base ` K ) /\ A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) /\ E. s e. ( Base ` K ) A. u e. ( Base ` K ) ( ( s ( +g ` K ) u ) = u /\ ( u ( +g ` K ) s ) = u ) ) <-> ( A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) /\ E. s e. ( Base ` L ) A. u e. ( Base ` L ) ( ( s ( +g ` L ) u ) = u /\ ( u ( +g ` L ) s ) = u ) ) ) )
89 10 11 ismnd 
 |-  ( K e. Mnd <-> ( A. u e. ( Base ` K ) A. v e. ( Base ` K ) ( ( u ( +g ` K ) v ) e. ( Base ` K ) /\ A. w e. ( Base ` K ) ( ( u ( +g ` K ) v ) ( +g ` K ) w ) = ( u ( +g ` K ) ( v ( +g ` K ) w ) ) ) /\ E. s e. ( Base ` K ) A. u e. ( Base ` K ) ( ( s ( +g ` K ) u ) = u /\ ( u ( +g ` K ) s ) = u ) ) )
90 23 24 ismnd 
 |-  ( L e. Mnd <-> ( A. u e. ( Base ` L ) A. v e. ( Base ` L ) ( ( u ( +g ` L ) v ) e. ( Base ` L ) /\ A. w e. ( Base ` L ) ( ( u ( +g ` L ) v ) ( +g ` L ) w ) = ( u ( +g ` L ) ( v ( +g ` L ) w ) ) ) /\ E. s e. ( Base ` L ) A. u e. ( Base ` L ) ( ( s ( +g ` L ) u ) = u /\ ( u ( +g ` L ) s ) = u ) ) )
91 88 89 90 3bitr4g 
 |-  ( ( ph /\ A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B ) -> ( K e. Mnd <-> L e. Mnd ) )
92 91 ex 
 |-  ( ph -> ( A. x e. B A. y e. B ( x ( +g ` K ) y ) e. B -> ( K e. Mnd <-> L e. Mnd ) ) )
93 16 30 92 pm5.21ndd 
 |-  ( ph -> ( K e. Mnd <-> L e. Mnd ) )