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 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
rngpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
rngpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
rngpropd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
Assertion rngpropd ( 𝜑 → ( 𝐾 ∈ Rng ↔ 𝐿 ∈ Rng ) )

Proof

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