Metamath Proof Explorer

Theorem lmodprop2d

Description: If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd also breaks up the components of the scalar ring. (Contributed by Mario Carneiro, 27-Jun-2015)

Ref Expression
Hypotheses lmodprop2d.b1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
lmodprop2d.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
lmodprop2d.f ⊢ 𝐹 = ( Scalar ‘ 𝐾 )
lmodprop2d.g ⊢ 𝐺 = ( Scalar ‘ 𝐿 )
lmodprop2d.p1 ⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐹 ) )
lmodprop2d.p2 ⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐺 ) )
lmodprop2d.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
lmodprop2d.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
lmodprop2d.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) )
lmodprop2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
Assertion lmodprop2d ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )

Proof

Step Hyp Ref Expression
1 lmodprop2d.b1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 lmodprop2d.b2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 lmodprop2d.f ⊢ 𝐹 = ( Scalar ‘ 𝐾 )
4 lmodprop2d.g ⊢ 𝐺 = ( Scalar ‘ 𝐿 )
5 lmodprop2d.p1 ⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐹 ) )
6 lmodprop2d.p2 ⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐺 ) )
7 lmodprop2d.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
8 lmodprop2d.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
9 lmodprop2d.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) )
10 lmodprop2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
11 lmodgrp ⊢ ( 𝐾 ∈ LMod → 𝐾 ∈ Grp )
12 11 a1i ⊢ ( 𝜑 → ( 𝐾 ∈ LMod → 𝐾 ∈ Grp ) )
13 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
15 eqid ⊢ ( ·𝑠 ‘ 𝐾 ) = ( ·𝑠 ‘ 𝐾 )
16 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
17 eqid ⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
18 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
19 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
20 13 14 15 3 16 17 18 19 islmod ⊢ ( 𝐾 ∈ LMod ↔ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ ( Base ‘ 𝐹 ) ∀ 𝑟 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) )
21 20 simp2bi ⊢ ( 𝐾 ∈ LMod → 𝐹 ∈ Ring )
22 21 a1i ⊢ ( 𝜑 → ( 𝐾 ∈ LMod → 𝐹 ∈ Ring ) )
23 simplr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐾 ∈ LMod )
24 simprl ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝑃 )
25 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 = ( Base ‘ 𝐹 ) )
26 24 25 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( Base ‘ 𝐹 ) )
27 simprr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
28 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐾 ) )
29 27 28 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
30 13 3 15 16 lmodvscl ⊢ ( ( 𝐾 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
31 23 26 29 30 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
32 31 28 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
33 32 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐾 ∈ LMod ) → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
34 33 ex ⊢ ( 𝜑 → ( 𝐾 ∈ LMod → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) )
35 12 22 34 3jcad ⊢ ( 𝜑 → ( 𝐾 ∈ LMod → ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) )
36 lmodgrp ⊢ ( 𝐿 ∈ LMod → 𝐿 ∈ Grp )
37 1 2 7 grppropd ⊢ ( 𝜑 → ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp ) )
38 36 37 syl5ibr ⊢ ( 𝜑 → ( 𝐿 ∈ LMod → 𝐾 ∈ Grp ) )
39 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
40 eqid ⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
41 eqid ⊢ ( ·𝑠 ‘ 𝐿 ) = ( ·𝑠 ‘ 𝐿 )
42 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
43 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
44 eqid ⊢ ( .r ‘ 𝐺 ) = ( .r ‘ 𝐺 )
45 eqid ⊢ ( 1r ‘ 𝐺 ) = ( 1r ‘ 𝐺 )
46 39 40 41 4 42 43 44 45 islmod ⊢ ( 𝐿 ∈ LMod ↔ ( 𝐿 ∈ Grp ∧ 𝐺 ∈ Ring ∧ ∀ 𝑞 ∈ ( Base ‘ 𝐺 ) ∀ 𝑟 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
47 46 simp2bi ⊢ ( 𝐿 ∈ LMod → 𝐺 ∈ Ring )
48 5 6 8 9 ringpropd ⊢ ( 𝜑 → ( 𝐹 ∈ Ring ↔ 𝐺 ∈ Ring ) )
49 47 48 syl5ibr ⊢ ( 𝜑 → ( 𝐿 ∈ LMod → 𝐹 ∈ Ring ) )
50 simplr ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐿 ∈ LMod )
51 simprl ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝑃 )
52 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 = ( Base ‘ 𝐺 ) )
53 51 52 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
54 simprr ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
55 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐿 ) )
56 54 55 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ 𝐿 ) )
57 39 4 41 42 lmodvscl ⊢ ( ( 𝐿 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐿 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) )
58 50 53 56 57 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) )
59 10 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
60 58 59 55 3eltr4d ⊢ ( ( ( 𝜑 ∧ 𝐿 ∈ LMod ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
61 60 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐿 ∈ LMod ) → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
62 61 ex ⊢ ( 𝜑 → ( 𝐿 ∈ LMod → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) )
63 38 49 62 3jcad ⊢ ( 𝜑 → ( 𝐿 ∈ LMod → ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) )
64 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp ) )
65 48 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( 𝐹 ∈ Ring ↔ 𝐺 ∈ Ring ) )
66 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝜑 )
67 simprlr ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑟 ∈ 𝑃 )
68 simprrr ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑤 ∈ 𝐵 )
69 10 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
70 66 67 68 69 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
71 70 eleq1d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ) )
72 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝐾 ∈ Grp )
73 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝐵 = ( Base ‘ 𝐾 ) )
74 68 73 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑤 ∈ ( Base ‘ 𝐾 ) )
75 simprrl ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑧 ∈ 𝐵 )
76 75 73 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐾 ) )
77 13 14 grpcl ⊢ ( ( 𝐾 ∈ Grp ∧ 𝑤 ∈ ( Base ‘ 𝐾 ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
78 72 74 76 77 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ∈ ( Base ‘ 𝐾 ) )
79 78 73 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ∈ 𝐵 )
80 10 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑃 ∧ ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ∈ 𝐵 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) )
81 66 67 79 80 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) )
82 7 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) = ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) )
83 66 68 75 82 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) = ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) )
84 83 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) )
85 81 84 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) )
86 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 )
87 ovrspc2v ⊢ ( ( ( 𝑟 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
88 67 68 86 87 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
89 ovrspc2v ⊢ ( ( ( 𝑟 ∈ 𝑃 ∧ 𝑧 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ∈ 𝐵 )
90 67 75 86 89 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ∈ 𝐵 )
91 7 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ∈ 𝐵 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) )
92 66 88 90 91 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) )
93 10 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑃 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) )
94 66 67 75 93 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) = ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) )
95 70 94 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) )
96 92 95 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) )
97 85 96 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ↔ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ) )
98 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝐹 ∈ Ring )
99 simprll ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑞 ∈ 𝑃 )
100 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑃 = ( Base ‘ 𝐹 ) )
101 99 100 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑞 ∈ ( Base ‘ 𝐹 ) )
102 67 100 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → 𝑟 ∈ ( Base ‘ 𝐹 ) )
103 16 17 ringacl ⊢ ( ( 𝐹 ∈ Ring ∧ 𝑞 ∈ ( Base ‘ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ 𝐹 ) ) → ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ∈ ( Base ‘ 𝐹 ) )
104 98 101 102 103 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ∈ ( Base ‘ 𝐹 ) )
105 104 100 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ∈ 𝑃 )
106 10 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
107 66 105 68 106 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
108 8 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) → ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) = ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) )
109 108 ad2ant2r ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) = ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) )
110 109 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
111 107 110 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
112 ovrspc2v ⊢ ( ( ( 𝑞 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
113 99 68 86 112 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 )
114 7 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ) ) → ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) )
115 66 113 88 114 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) )
116 10 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
117 66 99 68 116 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
118 117 70 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) )
119 115 118 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) )
120 111 119 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ↔ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) )
121 71 97 120 3anbi123d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ) )
122 16 18 ringcl ⊢ ( ( 𝐹 ∈ Ring ∧ 𝑞 ∈ ( Base ‘ 𝐹 ) ∧ 𝑟 ∈ ( Base ‘ 𝐹 ) ) → ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ∈ ( Base ‘ 𝐹 ) )
123 98 101 102 122 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ∈ ( Base ‘ 𝐹 ) )
124 123 100 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ∈ 𝑃 )
125 10 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
126 66 124 68 125 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
127 9 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) → ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) = ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) )
128 127 ad2ant2r ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) = ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) )
129 128 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
130 126 129 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
131 10 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑃 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) )
132 66 99 88 131 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) )
133 70 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) )
134 132 133 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) )
135 130 134 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ↔ ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) )
136 16 19 ringidcl ⊢ ( 𝐹 ∈ Ring → ( 1r ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
137 98 136 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 1r ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
138 137 100 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 1r ‘ 𝐹 ) ∈ 𝑃 )
139 10 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( ( 1r ‘ 𝐹 ) ∈ 𝑃 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
140 66 138 68 139 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
141 5 6 9 rngidpropd ⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐺 ) )
142 141 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐺 ) )
143 142 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
144 140 143 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) )
145 144 eqeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ↔ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) )
146 135 145 anbi12d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ↔ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) )
147 121 146 anbi12d ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
148 147 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
149 148 2ralbidva ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) ∧ ( 𝑞 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
150 149 2ralbidva ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑞 ∈ 𝑃 ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑞 ∈ 𝑃 ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
151 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → 𝑃 = ( Base ‘ 𝐹 ) )
152 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐾 ) )
153 152 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ) )
154 153 3anbi1d ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ) )
155 154 anbi1d ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) )
156 152 155 raleqbidv ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) )
157 152 156 raleqbidv ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) )
158 151 157 raleqbidv ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) )
159 151 158 raleqbidv ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑞 ∈ 𝑃 ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ 𝐹 ) ∀ 𝑟 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) )
160 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → 𝑃 = ( Base ‘ 𝐺 ) )
161 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐿 ) )
162 161 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ) )
163 162 3anbi1d ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ↔ ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ) )
164 163 anbi1d ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ↔ ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
165 161 164 raleqbidv ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
166 161 165 raleqbidv ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
167 160 166 raleqbidv ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
168 160 167 raleqbidv ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑞 ∈ 𝑃 ∀ 𝑟 ∈ 𝑃 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ 𝐵 ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ 𝐺 ) ∀ 𝑟 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
169 150 159 168 3bitr3d ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ∀ 𝑞 ∈ ( Base ‘ 𝐹 ) ∀ 𝑟 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ↔ ∀ 𝑞 ∈ ( Base ‘ 𝐺 ) ∀ 𝑟 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) )
170 64 65 169 3anbi123d ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑞 ∈ ( Base ‘ 𝐹 ) ∀ 𝑟 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑤 ∈ ( Base ‘ 𝐾 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐾 ) ( 𝑤 ( +g ‘ 𝐾 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ( +g ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐹 ) 𝑟 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐾 ) ( 𝑟 ( ·𝑠 ‘ 𝐾 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝐾 ) 𝑤 ) = 𝑤 ) ) ) ↔ ( 𝐿 ∈ Grp ∧ 𝐺 ∈ Ring ∧ ∀ 𝑞 ∈ ( Base ‘ 𝐺 ) ∀ 𝑟 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐿 ) ∀ 𝑤 ∈ ( Base ‘ 𝐿 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ∈ ( Base ‘ 𝐿 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝐿 ) ( 𝑤 ( +g ‘ 𝐿 ) 𝑧 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑧 ) ) ∧ ( ( 𝑞 ( +g ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ( +g ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ 𝐺 ) 𝑟 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝐿 ) ( 𝑟 ( ·𝑠 ‘ 𝐿 ) 𝑤 ) ) ∧ ( ( 1r ‘ 𝐺 ) ( ·𝑠 ‘ 𝐿 ) 𝑤 ) = 𝑤 ) ) ) ) )
171 170 20 46 3bitr4g ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) ) → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )
172 171 ex ⊢ ( 𝜑 → ( ( 𝐾 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ 𝐵 ) → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) ) )
173 35 63 172 pm5.21ndd ⊢ ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )