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 syl6eq ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
83 eqid ⊢ ( mulGrp ‘ 𝐿 ) = ( mulGrp ‘ 𝐿 )
84 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
85 83 84 mgpbas ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ ( mulGrp ‘ 𝐿 ) )
86 2 85 syl6eq ⊢ ( 𝜑 → 𝐵 = ( 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 ) )