Metamath Proof Explorer

Theorem ringpropd

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

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

Proof

Step Hyp Ref Expression
1 ringpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 ringpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 ringpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 ringpropd.4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
5 simpll 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ph )
6 simprll 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. B )
7 simplrl 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> K e. Grp )
8 simprlr 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. B )
9 1 ad2antrr 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> B = ( Base ` K ) )
10 8 9 eleqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. ( Base ` K ) )
11 simprr 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. B )
12 11 9 eleqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. ( Base ` K ) )
13 eqid 
 |-  ( Base ` K ) = ( Base ` K )
14 eqid 
 |-  ( +g ` K ) = ( +g ` K )
15 13 14 grpcl 
 |-  ( ( K e. Grp /\ v e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) )
16 7 10 12 15 syl3anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) )
17 16 9 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) e. B )
18 4 oveqrspc2v 
 |-  ( ( ph /\ ( u e. B /\ ( v ( +g ` K ) w ) e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` K ) w ) ) )
19 5 6 17 18 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` K ) w ) ) )
20 3 oveqrspc2v 
 |-  ( ( ph /\ ( v e. B /\ w e. B ) ) -> ( v ( +g ` K ) w ) = ( v ( +g ` L ) w ) )
21 5 8 11 20 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) = ( v ( +g ` L ) w ) )
22 21 oveq2d 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` L ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` L ) w ) ) )
23 19 22 eqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` L ) w ) ) )
24 simplrr 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( mulGrp ` K ) e. Mnd )
25 6 9 eleqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. ( Base ` K ) )
26 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
27 26 13 mgpbas 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
28 eqid 
 |-  ( .r ` K ) = ( .r ` K )
29 26 28 mgpplusg 
 |-  ( .r ` K ) = ( +g ` ( mulGrp ` K ) )
30 27 29 mndcl 
 |-  ( ( ( mulGrp ` K ) e. Mnd /\ u e. ( Base ` K ) /\ v e. ( Base ` K ) ) -> ( u ( .r ` K ) v ) e. ( Base ` K ) )
31 24 25 10 30 syl3anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) e. ( Base ` K ) )
32 31 9 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) e. B )
33 27 29 mndcl 
 |-  ( ( ( mulGrp ` K ) e. Mnd /\ u e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( u ( .r ` K ) w ) e. ( Base ` K ) )
34 24 25 12 33 syl3anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) e. ( Base ` K ) )
35 34 9 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) e. B )
36 3 oveqrspc2v 
 |-  ( ( ph /\ ( ( u ( .r ` K ) v ) e. B /\ ( u ( .r ` K ) w ) e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) )
37 5 32 35 36 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) )
38 4 oveqrspc2v 
 |-  ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u ( .r ` K ) v ) = ( u ( .r ` L ) v ) )
39 5 6 8 38 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) = ( u ( .r ` L ) v ) )
40 4 oveqrspc2v 
 |-  ( ( ph /\ ( u e. B /\ w e. B ) ) -> ( u ( .r ` K ) w ) = ( u ( .r ` L ) w ) )
41 5 6 11 40 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) = ( u ( .r ` L ) w ) )
42 39 41 oveq12d 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) )
43 37 42 eqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) )
44 23 43 eqeq12d 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) <-> ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) ) )
45 13 14 grpcl 
 |-  ( ( K e. Grp /\ u e. ( Base ` K ) /\ v e. ( Base ` K ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) )
46 7 25 10 45 syl3anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) )
47 46 9 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) e. B )
48 4 oveqrspc2v 
 |-  ( ( ph /\ ( ( u ( +g ` K ) v ) e. B /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` K ) v ) ( .r ` L ) w ) )
49 5 47 11 48 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` K ) v ) ( .r ` L ) w ) )
50 3 oveqrspc2v 
 |-  ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) )
51 5 6 8 50 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) )
52 51 oveq1d 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` L ) w ) = ( ( u ( +g ` L ) v ) ( .r ` L ) w ) )
53 49 52 eqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` L ) v ) ( .r ` L ) w ) )
54 27 29 mndcl 
 |-  ( ( ( mulGrp ` K ) e. Mnd /\ v e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( v ( .r ` K ) w ) e. ( Base ` K ) )
55 24 10 12 54 syl3anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) e. ( Base ` K ) )
56 55 9 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) e. B )
57 3 oveqrspc2v 
 |-  ( ( ph /\ ( ( u ( .r ` K ) w ) e. B /\ ( v ( .r ` K ) w ) e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) )
58 5 35 56 57 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) )
59 4 oveqrspc2v 
 |-  ( ( ph /\ ( v e. B /\ w e. B ) ) -> ( v ( .r ` K ) w ) = ( v ( .r ` L ) w ) )
60 5 8 11 59 syl12anc 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) = ( v ( .r ` L ) w ) )
61 41 60 oveq12d 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) )
62 58 61 eqtrd 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) )
63 53 62 eqeq12d 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) <-> ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) )
64 44 63 anbi12d 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
65 64 anassrs 
 |-  ( ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
66 65 ralbidva 
 |-  ( ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) /\ ( u e. B /\ v e. B ) ) -> ( A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
67 66 2ralbidva 
 |-  ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. B A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
68 1 adantr 
 |-  ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) -> B = ( Base ` K ) )
69 68 raleqdv 
 |-  ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) -> ( A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
70 68 69 raleqbidv 
 |-  ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) -> ( A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
71 68 70 raleqbidv 
 |-  ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
72 2 adantr 
 |-  ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) -> B = ( Base ` L ) )
73 72 raleqdv 
 |-  ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) -> ( A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
74 72 73 raleqbidv 
 |-  ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) -> ( A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
75 72 74 raleqbidv 
 |-  ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
76 67 71 75 3bitr3d 
 |-  ( ( ph /\ ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) ) -> ( A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
77 76 pm5.32da 
 |-  ( ph -> ( ( ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
78 df-3an 
 |-  ( ( K e. Grp /\ ( mulGrp ` K ) e. Mnd /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
79 df-3an 
 |-  ( ( K e. Grp /\ ( mulGrp ` K ) e. Mnd /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( ( K e. Grp /\ ( mulGrp ` K ) e. Mnd ) /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
80 77 78 79 3bitr4g 
 |-  ( ph -> ( ( K e. Grp /\ ( mulGrp ` K ) e. Mnd /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( K e. Grp /\ ( mulGrp ` K ) e. Mnd /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
81 1 2 3 grppropd 
 |-  ( ph -> ( K e. Grp <-> L e. Grp ) )
82 1 27 eqtrdi 
 |-  ( ph -> B = ( Base ` ( mulGrp ` K ) ) )
83 eqid 
 |-  ( mulGrp ` L ) = ( mulGrp ` L )
84 eqid 
 |-  ( Base ` L ) = ( Base ` L )
85 83 84 mgpbas 
 |-  ( Base ` L ) = ( Base ` ( mulGrp ` L ) )
86 2 85 eqtrdi 
 |-  ( ph -> B = ( Base ` ( mulGrp ` L ) ) )
87 29 oveqi 
 |-  ( x ( .r ` K ) y ) = ( x ( +g ` ( mulGrp ` K ) ) y )
88 eqid 
 |-  ( .r ` L ) = ( .r ` L )
89 83 88 mgpplusg 
 |-  ( .r ` L ) = ( +g ` ( mulGrp ` L ) )
90 89 oveqi 
 |-  ( x ( .r ` L ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y )
91 4 87 90 3eqtr3g 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` ( mulGrp ` K ) ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y ) )
92 82 86 91 mndpropd 
 |-  ( ph -> ( ( mulGrp ` K ) e. Mnd <-> ( mulGrp ` L ) e. Mnd ) )
93 81 92 3anbi12d 
 |-  ( ph -> ( ( K e. Grp /\ ( mulGrp ` K ) e. Mnd /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( L e. Grp /\ ( mulGrp ` L ) e. Mnd /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
94 80 93 bitrd 
 |-  ( ph -> ( ( K e. Grp /\ ( mulGrp ` K ) e. Mnd /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( L e. Grp /\ ( mulGrp ` L ) e. Mnd /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
95 13 26 14 28 isring 
 |-  ( K e. Ring <-> ( K e. Grp /\ ( mulGrp ` K ) e. Mnd /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
96 eqid 
 |-  ( +g ` L ) = ( +g ` L )
97 84 83 96 88 isring 
 |-  ( L e. Ring <-> ( L e. Grp /\ ( mulGrp ` L ) e. Mnd /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
98 94 95 97 3bitr4g 
 |-  ( ph -> ( K e. Ring <-> L e. Ring ) )