Metamath Proof Explorer

Theorem rngpropd

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 non-unital ring iff the other one is. (Contributed by AV, 15-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 rngpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 rngpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 rngpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 rngpropd.4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
5 simpll 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ph )
6 simprll 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. B )
7 simplrl 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> K e. Abel )
8 simprlr 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. B )
9 1 ad2antrr 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> B = ( Base ` K ) )
10 8 9 eleqtrd 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. ( Base ` K ) )
11 simprr 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. B )
12 11 9 eleqtrd 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. ( Base ` K ) )
13 ablgrp 
 |-  ( K e. Abel -> K e. Grp )
14 eqid 
 |-  ( Base ` K ) = ( Base ` K )
15 eqid 
 |-  ( +g ` K ) = ( +g ` K )
16 14 15 grpcl 
 |-  ( ( K e. Grp /\ v e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) )
17 13 16 syl3an1 
 |-  ( ( K e. Abel /\ v e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) )
18 7 10 12 17 syl3anc 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) )
19 18 9 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) e. B )
20 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 ) ) )
21 5 6 19 20 syl12anc 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` K ) w ) ) )
22 3 oveqrspc2v 
 |-  ( ( ph /\ ( v e. B /\ w e. B ) ) -> ( v ( +g ` K ) w ) = ( v ( +g ` L ) w ) )
23 5 8 11 22 syl12anc 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) = ( v ( +g ` L ) w ) )
24 23 oveq2d 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` L ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` L ) w ) ) )
25 21 24 eqtrd 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` L ) w ) ) )
26 simplrr 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( mulGrp ` K ) e. Smgrp )
27 6 9 eleqtrd 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. ( Base ` K ) )
28 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
29 28 14 mgpbas 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
30 eqid 
 |-  ( .r ` K ) = ( .r ` K )
31 28 30 mgpplusg 
 |-  ( .r ` K ) = ( +g ` ( mulGrp ` K ) )
32 29 31 sgrpcl 
 |-  ( ( ( mulGrp ` K ) e. Smgrp /\ u e. ( Base ` K ) /\ v e. ( Base ` K ) ) -> ( u ( .r ` K ) v ) e. ( Base ` K ) )
33 26 27 10 32 syl3anc 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) e. ( Base ` K ) )
34 33 9 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) e. B )
35 29 31 sgrpcl 
 |-  ( ( ( mulGrp ` K ) e. Smgrp /\ u e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( u ( .r ` K ) w ) e. ( Base ` K ) )
36 26 27 12 35 syl3anc 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) e. ( Base ` K ) )
37 36 9 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) e. B )
38 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 ) ) )
39 5 34 37 38 syl12anc 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( 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 ) ) )
40 4 oveqrspc2v 
 |-  ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u ( .r ` K ) v ) = ( u ( .r ` L ) v ) )
41 40 ad2ant2r 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) = ( u ( .r ` L ) v ) )
42 4 oveqrspc2v 
 |-  ( ( ph /\ ( u e. B /\ w e. B ) ) -> ( u ( .r ` K ) w ) = ( u ( .r ` L ) w ) )
43 5 6 11 42 syl12anc 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) = ( u ( .r ` L ) w ) )
44 41 43 oveq12d 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( 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 ) ) )
45 39 44 eqtrd 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( 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 ) ) )
46 25 45 eqeq12d 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( 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 ) ) ) )
47 14 15 grpcl 
 |-  ( ( K e. Grp /\ u e. ( Base ` K ) /\ v e. ( Base ` K ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) )
48 13 47 syl3an1 
 |-  ( ( K e. Abel /\ u e. ( Base ` K ) /\ v e. ( Base ` K ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) )
49 7 27 10 48 syl3anc 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) )
50 49 9 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) e. B )
51 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 ) )
52 5 50 11 51 syl12anc 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` K ) v ) ( .r ` L ) w ) )
53 3 oveqrspc2v 
 |-  ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) )
54 53 ad2ant2r 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) )
55 54 oveq1d 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` L ) w ) = ( ( u ( +g ` L ) v ) ( .r ` L ) w ) )
56 52 55 eqtrd 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` L ) v ) ( .r ` L ) w ) )
57 29 31 sgrpcl 
 |-  ( ( ( mulGrp ` K ) e. Smgrp /\ v e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( v ( .r ` K ) w ) e. ( Base ` K ) )
58 26 10 12 57 syl3anc 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) e. ( Base ` K ) )
59 58 9 eleqtrrd 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) e. B )
60 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 ) ) )
61 5 37 59 60 syl12anc 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( 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 ) ) )
62 4 oveqrspc2v 
 |-  ( ( ph /\ ( v e. B /\ w e. B ) ) -> ( v ( .r ` K ) w ) = ( v ( .r ` L ) w ) )
63 5 8 11 62 syl12anc 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) = ( v ( .r ` L ) w ) )
64 43 63 oveq12d 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( 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 ) ) )
65 61 64 eqtrd 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( 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 ) ) )
66 56 65 eqeq12d 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( 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 ) ) ) )
67 46 66 anbi12d 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( ( 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 ) ) ) ) )
68 67 anassrs 
 |-  ( ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( 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 ) ) ) ) )
69 68 ralbidva 
 |-  ( ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) /\ ( 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 ) ) ) ) )
70 69 2ralbidva 
 |-  ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( 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 ) ) ) ) )
71 1 adantr 
 |-  ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> B = ( Base ` K ) )
72 71 raleqdv 
 |-  ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( 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 ) ) ) ) )
73 71 72 raleqbidv 
 |-  ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( 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 ) ) ) ) )
74 71 73 raleqbidv 
 |-  ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( 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 ) ) ) ) )
75 2 adantr 
 |-  ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> B = ( Base ` L ) )
76 75 raleqdv 
 |-  ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( 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 ) ) ) ) )
77 75 76 raleqbidv 
 |-  ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( 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 ) ) ) ) )
78 75 77 raleqbidv 
 |-  ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( 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 ) ) ) ) )
79 70 74 78 3bitr3d 
 |-  ( ( ph /\ ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) ) -> ( 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 ) ) ) ) )
80 79 pm5.32da 
 |-  ( ph -> ( ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp ) /\ 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. Abel /\ ( mulGrp ` K ) e. Smgrp ) /\ 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 df-3an 
 |-  ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ 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. Abel /\ ( mulGrp ` K ) e. Smgrp ) /\ 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 ) ) ) ) )
82 df-3an 
 |-  ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ 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. Abel /\ ( mulGrp ` K ) e. Smgrp ) /\ 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 ) ) ) ) )
83 80 81 82 3bitr4g 
 |-  ( ph -> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ 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. Abel /\ ( mulGrp ` K ) e. Smgrp /\ 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 ) ) ) ) ) )
84 1 2 3 ablpropd 
 |-  ( ph -> ( K e. Abel <-> L e. Abel ) )
85 fvexd 
 |-  ( ph -> ( mulGrp ` K ) e. _V )
86 fvexd 
 |-  ( ph -> ( mulGrp ` L ) e. _V )
87 29 a1i 
 |-  ( ph -> ( Base ` K ) = ( Base ` ( mulGrp ` K ) ) )
88 eqid 
 |-  ( mulGrp ` L ) = ( mulGrp ` L )
89 eqid 
 |-  ( Base ` L ) = ( Base ` L )
90 88 89 mgpbas 
 |-  ( Base ` L ) = ( Base ` ( mulGrp ` L ) )
91 2 90 eqtrdi 
 |-  ( ph -> B = ( Base ` ( mulGrp ` L ) ) )
92 1 91 eqtr3d 
 |-  ( ph -> ( Base ` K ) = ( Base ` ( mulGrp ` L ) ) )
93 4 ex 
 |-  ( ph -> ( ( x e. B /\ y e. B ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) ) )
94 1 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Base ` K ) ) )
95 1 eleq2d 
 |-  ( ph -> ( y e. B <-> y e. ( Base ` K ) ) )
96 94 95 anbi12d 
 |-  ( ph -> ( ( x e. B /\ y e. B ) <-> ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) )
97 96 bicomd 
 |-  ( ph -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) <-> ( x e. B /\ y e. B ) ) )
98 31 a1i 
 |-  ( ph -> ( .r ` K ) = ( +g ` ( mulGrp ` K ) ) )
99 98 eqcomd 
 |-  ( ph -> ( +g ` ( mulGrp ` K ) ) = ( .r ` K ) )
100 99 oveqd 
 |-  ( ph -> ( x ( +g ` ( mulGrp ` K ) ) y ) = ( x ( .r ` K ) y ) )
101 eqid 
 |-  ( .r ` L ) = ( .r ` L )
102 88 101 mgpplusg 
 |-  ( .r ` L ) = ( +g ` ( mulGrp ` L ) )
103 102 a1i 
 |-  ( ph -> ( .r ` L ) = ( +g ` ( mulGrp ` L ) ) )
104 103 eqcomd 
 |-  ( ph -> ( +g ` ( mulGrp ` L ) ) = ( .r ` L ) )
105 104 oveqd 
 |-  ( ph -> ( x ( +g ` ( mulGrp ` L ) ) y ) = ( x ( .r ` L ) y ) )
106 100 105 eqeq12d 
 |-  ( ph -> ( ( x ( +g ` ( mulGrp ` K ) ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y ) <-> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) ) )
107 93 97 106 3imtr4d 
 |-  ( ph -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> ( x ( +g ` ( mulGrp ` K ) ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y ) ) )
108 107 imp 
 |-  ( ( ph /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( +g ` ( mulGrp ` K ) ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y ) )
109 85 86 87 92 108 sgrppropd 
 |-  ( ph -> ( ( mulGrp ` K ) e. Smgrp <-> ( mulGrp ` L ) e. Smgrp ) )
110 84 109 3anbi12d 
 |-  ( ph -> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ 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. Abel /\ ( mulGrp ` L ) e. Smgrp /\ 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 ) ) ) ) ) )
111 83 110 bitrd 
 |-  ( ph -> ( ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ 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. Abel /\ ( mulGrp ` L ) e. Smgrp /\ 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 ) ) ) ) ) )
112 14 28 15 30 isrng 
 |-  ( K e. Rng <-> ( K e. Abel /\ ( mulGrp ` K ) e. Smgrp /\ 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 ) ) ) ) )
113 eqid 
 |-  ( +g ` L ) = ( +g ` L )
114 89 88 113 101 isrng 
 |-  ( L e. Rng <-> ( L e. Abel /\ ( mulGrp ` L ) e. Smgrp /\ 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 ) ) ) ) )
115 111 112 114 3bitr4g 
 |-  ( ph -> ( K e. Rng <-> L e. Rng ) )