Metamath Proof Explorer


Theorem ringpropd

Description: If two structures have the same group components (properties), 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 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
ringpropd.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
ringpropd.3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
ringpropd.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝐾 ) 𝑦 ) = ( 𝑥 ( .r𝐿 ) 𝑦 ) )
Assertion ringpropd ( 𝜑 → ( 𝐾 ∈ Ring ↔ 𝐿 ∈ Ring ) )

Proof

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