Metamath Proof Explorer

Theorem primrootsunit1

Description: Primitive roots have left inverses. (Contributed by metakunt, 25-Apr-2025)

Ref Expression
Hypotheses primrootsunit1.1 ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
primrootsunit1.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
primrootsunit1.3 ⊢ 𝑈 = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) }
Assertion primrootsunit1 ( 𝜑 → ( ( 𝑅 PrimRoots 𝐾 ) = ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ∧ ( 𝑅 ↾s 𝑈 ) ∈ Abel ) )

Proof

Step Hyp Ref Expression
1 primrootsunit1.1 ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
2 primrootsunit1.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 primrootsunit1.3 ⊢ 𝑈 = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) }
4 1 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝑅 ∈ CMnd )
5 2 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
6 5 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝐾 ∈ ℕ0 )
7 eqid ⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
8 4 6 7 isprimroot ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ↔ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
9 8 biimpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) → ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
10 9 syldbl2 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
11 10 simp1d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝑐 ∈ ( Base ‘ 𝑅 ) )
12 1 cmnmndd ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝑅 ∈ Mnd )
14 nnm1nn0 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ0 )
15 2 14 syl ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ0 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝐾 − 1 ) ∈ ℕ0 )
17 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
18 17 7 mulgnn0cl ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝐾 − 1 ) ∈ ℕ0 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 − 1 ) ( .g ‘ 𝑅 ) 𝑐 ) ∈ ( Base ‘ 𝑅 ) )
19 13 16 11 18 syl3anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( ( 𝐾 − 1 ) ( .g ‘ 𝑅 ) 𝑐 ) ∈ ( Base ‘ 𝑅 ) )
20 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) ∧ 𝑖 = ( ( 𝐾 − 1 ) ( .g ‘ 𝑅 ) 𝑐 ) ) → 𝑖 = ( ( 𝐾 − 1 ) ( .g ‘ 𝑅 ) 𝑐 ) )
21 20 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) ∧ 𝑖 = ( ( 𝐾 − 1 ) ( .g ‘ 𝑅 ) 𝑐 ) ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑐 ) = ( ( ( 𝐾 − 1 ) ( .g ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) 𝑐 ) )
22 21 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) ∧ 𝑖 = ( ( 𝐾 − 1 ) ( .g ‘ 𝑅 ) 𝑐 ) ) → ( ( 𝑖 ( +g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ↔ ( ( ( 𝐾 − 1 ) ( .g ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
23 2 nncnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
24 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
25 23 24 npcand ⊢ ( 𝜑 → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
26 25 eqcomd ⊢ ( 𝜑 → 𝐾 = ( ( 𝐾 − 1 ) + 1 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝐾 = ( ( 𝐾 − 1 ) + 1 ) )
28 27 oveq1d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) = ( ( ( 𝐾 − 1 ) + 1 ) ( .g ‘ 𝑅 ) 𝑐 ) )
29 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
30 17 7 29 mulgnn0p1 ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝐾 − 1 ) ∈ ℕ0 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝐾 − 1 ) + 1 ) ( .g ‘ 𝑅 ) 𝑐 ) = ( ( ( 𝐾 − 1 ) ( .g ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) 𝑐 ) )
31 13 16 11 30 syl3anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( ( ( 𝐾 − 1 ) + 1 ) ( .g ‘ 𝑅 ) 𝑐 ) = ( ( ( 𝐾 − 1 ) ( .g ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) 𝑐 ) )
32 28 31 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( ( ( 𝐾 − 1 ) ( .g ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) 𝑐 ) = ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) )
33 10 simp2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) )
34 32 33 eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( ( ( 𝐾 − 1 ) ( .g ‘ 𝑅 ) 𝑐 ) ( +g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) )
35 19 22 34 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) )
36 11 35 jca ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
37 oveq2 ⊢ ( 𝑎 = 𝑐 → ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 𝑖 ( +g ‘ 𝑅 ) 𝑐 ) )
38 37 eqeq1d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑖 ( +g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
39 38 rexbidv ⊢ ( 𝑎 = 𝑐 → ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
40 39 elrab ⊢ ( 𝑐 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ↔ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
41 36 40 sylibr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝑐 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } )
42 3 eleq2i ⊢ ( 𝑐 ∈ 𝑈 ↔ 𝑐 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } )
43 41 42 sylibr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝑐 ∈ 𝑈 )
44 simpl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → 𝜑 )
45 3 a1i ⊢ ( 𝜑 → 𝑈 = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } )
46 45 eleq2d ⊢ ( 𝜑 → ( 𝑏 ∈ 𝑈 ↔ 𝑏 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ) )
47 46 biimpd ⊢ ( 𝜑 → ( 𝑏 ∈ 𝑈 → 𝑏 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ) )
48 47 imp ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → 𝑏 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } )
49 44 48 jca ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( 𝜑 ∧ 𝑏 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ) )
50 elrabi ⊢ ( 𝑏 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } → 𝑏 ∈ ( Base ‘ 𝑅 ) )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
52 49 51 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
53 52 ex ⊢ ( 𝜑 → ( 𝑏 ∈ 𝑈 → 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
54 53 ssrdv ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝑅 ) )
55 eqid ⊢ ( 𝑅 ↾s 𝑈 ) = ( 𝑅 ↾s 𝑈 )
56 55 17 ressbas2 ⊢ ( 𝑈 ⊆ ( Base ‘ 𝑅 ) → 𝑈 = ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
57 54 56 syl ⊢ ( 𝜑 → 𝑈 = ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝑈 = ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
59 58 eleq2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝑐 ∈ 𝑈 ↔ 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
60 43 59 mpbid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
61 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → 𝑅 ∈ Mnd )
62 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
63 simpl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑈 ) → 𝜑 )
64 45 eleq2d ⊢ ( 𝜑 → ( 𝑑 ∈ 𝑈 ↔ 𝑑 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ) )
65 64 biimpd ⊢ ( 𝜑 → ( 𝑑 ∈ 𝑈 → 𝑑 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ) )
66 65 imp ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑈 ) → 𝑑 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } )
67 63 66 jca ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑈 ) → ( 𝜑 ∧ 𝑑 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ) )
68 elrabi ⊢ ( 𝑑 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } → 𝑑 ∈ ( Base ‘ 𝑅 ) )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ) → 𝑑 ∈ ( Base ‘ 𝑅 ) )
70 67 69 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑈 ) → 𝑑 ∈ ( Base ‘ 𝑅 ) )
71 44 70 sylan ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → 𝑑 ∈ ( Base ‘ 𝑅 ) )
72 17 29 mndcl ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑑 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
73 61 62 71 72 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
74 3 eleq2i ⊢ ( 𝑑 ∈ 𝑈 ↔ 𝑑 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } )
75 oveq2 ⊢ ( 𝑎 = 𝑑 → ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) )
76 75 eqeq1d ⊢ ( 𝑎 = 𝑑 → ( ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) )
77 76 rexbidv ⊢ ( 𝑎 = 𝑑 → ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) )
78 77 elrab ⊢ ( 𝑑 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ↔ ( 𝑑 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) )
79 74 78 bitri ⊢ ( 𝑑 ∈ 𝑈 ↔ ( 𝑑 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) )
80 79 biimpi ⊢ ( 𝑑 ∈ 𝑈 → ( 𝑑 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) )
81 80 simprd ⊢ ( 𝑑 ∈ 𝑈 → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) )
82 81 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) )
83 1 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ CMnd )
84 71 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) → 𝑑 ∈ ( Base ‘ 𝑅 ) )
85 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) → 𝑖 ∈ ( Base ‘ 𝑅 ) )
86 17 29 cmncom ⊢ ( ( 𝑅 ∈ CMnd ∧ 𝑑 ∈ ( Base ‘ 𝑅 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑑 ( +g ‘ 𝑅 ) 𝑖 ) = ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) )
87 83 84 85 86 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑑 ( +g ‘ 𝑅 ) 𝑖 ) = ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) )
88 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) )
89 87 88 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑑 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) )
90 89 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) → ( 𝑑 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) ) )
91 90 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑑 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) ) )
92 82 91 mpd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑑 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) )
93 17 61 71 92 mndmolinv ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ∃* 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) )
94 82 93 jca ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ∧ ∃* 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) )
95 reu5 ⊢ ( ∃! 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ↔ ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ∧ ∃* 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) )
96 94 95 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ∃! 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) )
97 riotacl ⊢ ( ∃! 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) → ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
98 96 97 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
99 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
100 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
101 17 29 99 100 grpinvval ⊢ ( 𝑑 ∈ ( Base ‘ 𝑅 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) = ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) )
102 71 101 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) = ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) )
103 102 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) ↔ ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) ) )
104 98 103 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
105 3 eleq2i ⊢ ( 𝑏 ∈ 𝑈 ↔ 𝑏 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } )
106 oveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) )
107 106 eqeq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) )
108 107 rexbidv ⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) )
109 108 elrab ⊢ ( 𝑏 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ↔ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) )
110 105 109 bitri ⊢ ( 𝑏 ∈ 𝑈 ↔ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) )
111 110 biimpi ⊢ ( 𝑏 ∈ 𝑈 → ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) )
112 111 simprd ⊢ ( 𝑏 ∈ 𝑈 → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) )
113 112 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) )
114 1 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ CMnd )
115 62 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
116 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → 𝑖 ∈ ( Base ‘ 𝑅 ) )
117 17 29 cmncom ⊢ ( ( 𝑅 ∈ CMnd ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑏 ( +g ‘ 𝑅 ) 𝑖 ) = ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) )
118 114 115 116 117 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑏 ( +g ‘ 𝑅 ) 𝑖 ) = ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) )
119 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) )
120 118 119 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑏 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) )
121 120 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) → ( 𝑏 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) ) )
122 121 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) ) )
123 113 122 mpd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) )
124 17 61 62 123 mndmolinv ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ∃* 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) )
125 113 124 jca ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ∧ ∃* 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) )
126 reu5 ⊢ ( ∃! 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ↔ ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ∧ ∃* 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) )
127 125 126 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ∃! 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) )
128 riotacl ⊢ ( ∃! 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) → ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
129 127 128 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
130 17 29 99 100 grpinvval ⊢ ( 𝑏 ∈ ( Base ‘ 𝑅 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) = ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) )
131 62 130 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) = ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) )
132 131 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) ↔ ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) ) )
133 129 132 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
134 17 29 mndcl ⊢ ( ( 𝑅 ∈ Mnd ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ) ∈ ( Base ‘ 𝑅 ) )
135 61 104 133 134 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ) ∈ ( Base ‘ 𝑅 ) )
136 oveq1 ⊢ ( 𝑖 = ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ) → ( 𝑖 ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) )
137 136 eqeq1d ⊢ ( 𝑖 = ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ) → ( ( 𝑖 ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( 0g ‘ 𝑅 ) ↔ ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( 0g ‘ 𝑅 ) ) )
138 137 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) ∧ 𝑖 = ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ) ) → ( ( 𝑖 ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( 0g ‘ 𝑅 ) ↔ ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( 0g ‘ 𝑅 ) ) )
139 104 133 73 3jca ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ ( Base ‘ 𝑅 ) ) )
140 17 29 mndass ⊢ ( ( 𝑅 ∈ Mnd ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) ) )
141 61 139 140 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) ) )
142 133 62 71 3jca ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑑 ∈ ( Base ‘ 𝑅 ) ) )
143 17 29 mndass ⊢ ( ( 𝑅 ∈ Mnd ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑑 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) 𝑑 ) = ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) )
144 143 eqcomd ⊢ ( ( 𝑅 ∈ Mnd ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑑 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) 𝑑 ) )
145 61 142 144 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) 𝑑 ) )
146 145 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) ) = ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) 𝑑 ) ) )
147 62 127 linvh ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) 𝑏 ) = ( 0g ‘ 𝑅 ) )
148 147 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) 𝑑 ) = ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑑 ) )
149 148 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) 𝑑 ) ) = ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑑 ) ) )
150 17 29 99 mndlid ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑑 ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑑 ) = 𝑑 )
151 61 71 150 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑑 ) = 𝑑 )
152 151 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑑 ) ) = ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) 𝑑 ) )
153 71 96 linvh ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) 𝑑 ) = ( 0g ‘ 𝑅 ) )
154 152 153 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) 𝑑 ) ) = ( 0g ‘ 𝑅 ) )
155 149 154 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) 𝑏 ) ( +g ‘ 𝑅 ) 𝑑 ) ) = ( 0g ‘ 𝑅 ) )
156 146 155 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) ) = ( 0g ‘ 𝑅 ) )
157 141 156 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( ( ( invg ‘ 𝑅 ) ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑏 ) ) ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( 0g ‘ 𝑅 ) )
158 135 138 157 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( 0g ‘ 𝑅 ) )
159 73 158 jca ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( 0g ‘ 𝑅 ) ) )
160 oveq2 ⊢ ( 𝑎 = ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 𝑖 ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) )
161 160 eqeq1d ⊢ ( 𝑎 = ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) → ( ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑖 ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( 0g ‘ 𝑅 ) ) )
162 161 rexbidv ⊢ ( 𝑎 = ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) → ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( 0g ‘ 𝑅 ) ) )
163 162 elrab ⊢ ( ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ↔ ( ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ) = ( 0g ‘ 𝑅 ) ) )
164 159 163 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } )
165 3 eleq2i ⊢ ( ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ 𝑈 ↔ ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } )
166 165 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ 𝑈 ↔ ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ) )
167 164 166 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ 𝑈 )
168 167 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ∀ 𝑑 ∈ 𝑈 ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ 𝑈 )
169 168 ralrimiva ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝑈 ∀ 𝑑 ∈ 𝑈 ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ 𝑈 )
170 oveq2 ⊢ ( 𝑎 = ( 0g ‘ 𝑅 ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 𝑖 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
171 170 eqeq1d ⊢ ( 𝑎 = ( 0g ‘ 𝑅 ) → ( ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑖 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
172 171 rexbidv ⊢ ( 𝑎 = ( 0g ‘ 𝑅 ) → ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
173 17 99 mndidcl ⊢ ( 𝑅 ∈ Mnd → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
174 12 173 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
175 12 174 jca ⊢ ( 𝜑 → ( 𝑅 ∈ Mnd ∧ ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) )
176 17 29 99 mndlid ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
177 175 176 syl ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
178 174 177 jca ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
179 oveq1 ⊢ ( 𝑖 = ( 0g ‘ 𝑅 ) → ( 𝑖 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
180 179 eqeq1d ⊢ ( 𝑖 = ( 0g ‘ 𝑅 ) → ( ( 𝑖 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ↔ ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
181 180 rspcev ⊢ ( ( ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 0g ‘ 𝑅 ) ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
182 178 181 syl ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
183 172 174 182 elrabd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } )
184 45 eleq2d ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) ∈ 𝑈 ↔ ( 0g ‘ 𝑅 ) ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ) )
185 183 184 mpbird ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝑈 )
186 17 29 99 55 issubmnd ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑈 ⊆ ( Base ‘ 𝑅 ) ∧ ( 0g ‘ 𝑅 ) ∈ 𝑈 ) → ( ( 𝑅 ↾s 𝑈 ) ∈ Mnd ↔ ∀ 𝑏 ∈ 𝑈 ∀ 𝑑 ∈ 𝑈 ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ 𝑈 ) )
187 12 54 185 186 syl3anc ⊢ ( 𝜑 → ( ( 𝑅 ↾s 𝑈 ) ∈ Mnd ↔ ∀ 𝑏 ∈ 𝑈 ∀ 𝑑 ∈ 𝑈 ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ 𝑈 ) )
188 169 187 mpbird ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑈 ) ∈ Mnd )
189 45 eleq2d ⊢ ( 𝜑 → ( 𝑞 ∈ 𝑈 ↔ 𝑞 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ) )
190 189 biimpd ⊢ ( 𝜑 → ( 𝑞 ∈ 𝑈 → 𝑞 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ) )
191 190 imp ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) → 𝑞 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } )
192 oveq2 ⊢ ( 𝑎 = 𝑞 → ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) )
193 192 eqeq1d ⊢ ( 𝑎 = 𝑞 → ( ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) )
194 193 rexbidv ⊢ ( 𝑎 = 𝑞 → ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) )
195 194 elrab ⊢ ( 𝑞 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ↔ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) )
196 191 195 sylib ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) → ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) )
197 196 simprd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) )
198 simprl ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) ) → 𝑖 ∈ ( Base ‘ 𝑅 ) )
199 196 simpld ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) → 𝑞 ∈ ( Base ‘ 𝑅 ) )
200 199 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) ) → 𝑞 ∈ ( Base ‘ 𝑅 ) )
201 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) ) ∧ 𝑗 = 𝑞 ) → 𝑗 = 𝑞 )
202 201 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) ) ∧ 𝑗 = 𝑞 ) → ( 𝑗 ( +g ‘ 𝑅 ) 𝑖 ) = ( 𝑞 ( +g ‘ 𝑅 ) 𝑖 ) )
203 202 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) ) ∧ 𝑗 = 𝑞 ) → ( ( 𝑗 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑞 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) ) )
204 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) ) → 𝑅 ∈ CMnd )
205 17 29 cmncom ⊢ ( ( 𝑅 ∈ CMnd ∧ 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ 𝑞 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 𝑞 ( +g ‘ 𝑅 ) 𝑖 ) )
206 204 198 200 205 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 𝑞 ( +g ‘ 𝑅 ) 𝑖 ) )
207 simprr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) )
208 206 207 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝑞 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) )
209 200 203 208 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) ) → ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) )
210 198 209 jca ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) ) )
211 nfv ⊢ Ⅎ 𝑗 ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 )
212 nfv ⊢ Ⅎ 𝑖 ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 )
213 oveq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) )
214 213 eqeq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ) )
215 211 212 214 cbvrexw ⊢ ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) )
216 215 rabbii ⊢ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) }
217 3 216 eqtri ⊢ 𝑈 = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) }
218 217 eleq2i ⊢ ( 𝑖 ∈ 𝑈 ↔ 𝑖 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } )
219 oveq2 ⊢ ( 𝑎 = 𝑖 → ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 𝑗 ( +g ‘ 𝑅 ) 𝑖 ) )
220 219 eqeq1d ⊢ ( 𝑎 = 𝑖 → ( ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑗 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) ) )
221 220 rexbidv ⊢ ( 𝑎 = 𝑖 → ( ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) ) )
222 221 elrab ⊢ ( 𝑖 ∈ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } ↔ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) ) )
223 218 222 bitri ⊢ ( 𝑖 ∈ 𝑈 ↔ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑖 ) = ( 0g ‘ 𝑅 ) ) )
224 210 223 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝑖 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) ) → 𝑖 ∈ 𝑈 )
225 197 224 207 reximssdv ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) → ∃ 𝑖 ∈ 𝑈 ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) )
226 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V )
227 3 226 rabexd ⊢ ( 𝜑 → 𝑈 ∈ V )
228 55 29 ressplusg ⊢ ( 𝑈 ∈ V → ( +g ‘ 𝑅 ) = ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) )
229 227 228 syl ⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) )
230 229 eqcomd ⊢ ( 𝜑 → ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( +g ‘ 𝑅 ) )
231 230 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) → ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( +g ‘ 𝑅 ) )
232 231 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ 𝑤 = 𝑖 ) → ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( +g ‘ 𝑅 ) )
233 simpr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ 𝑤 = 𝑖 ) → 𝑤 = 𝑖 )
234 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ 𝑤 = 𝑖 ) → 𝑞 = 𝑞 )
235 232 233 234 oveq123d ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ 𝑤 = 𝑖 ) → ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) )
236 55 17 99 ress0g ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0g ‘ 𝑅 ) ∈ 𝑈 ∧ 𝑈 ⊆ ( Base ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
237 12 185 54 236 syl3anc ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
238 237 eqcomd ⊢ ( 𝜑 → ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( 0g ‘ 𝑅 ) )
239 238 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) → ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( 0g ‘ 𝑅 ) )
240 239 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ 𝑤 = 𝑖 ) → ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( 0g ‘ 𝑅 ) )
241 235 240 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ 𝑤 = 𝑖 ) → ( ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ↔ ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) )
242 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) ∧ 𝑤 = 𝑖 ) → 𝑈 = 𝑈 )
243 241 242 cbvrexdva2 ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) → ( ∃ 𝑤 ∈ 𝑈 ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ↔ ∃ 𝑖 ∈ 𝑈 ( 𝑖 ( +g ‘ 𝑅 ) 𝑞 ) = ( 0g ‘ 𝑅 ) ) )
244 225 243 mpbird ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
245 57 eqcomd ⊢ ( 𝜑 → ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) = 𝑈 )
246 245 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) → ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) = 𝑈 )
247 244 246 rexeqtrrdv ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑈 ) → ∃ 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
248 247 ex ⊢ ( 𝜑 → ( 𝑞 ∈ 𝑈 → ∃ 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
249 57 eleq2d ⊢ ( 𝜑 → ( 𝑞 ∈ 𝑈 ↔ 𝑞 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
250 249 imbi1d ⊢ ( 𝜑 → ( ( 𝑞 ∈ 𝑈 → ∃ 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ) ↔ ( 𝑞 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) → ∃ 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ) ) )
251 248 250 mpbid ⊢ ( 𝜑 → ( 𝑞 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) → ∃ 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
252 251 imp ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) → ∃ 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
253 252 ralrimiva ⊢ ( 𝜑 → ∀ 𝑞 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∃ 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
254 188 253 jca ⊢ ( 𝜑 → ( ( 𝑅 ↾s 𝑈 ) ∈ Mnd ∧ ∀ 𝑞 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∃ 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
255 eqid ⊢ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) = ( Base ‘ ( 𝑅 ↾s 𝑈 ) )
256 eqid ⊢ ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( +g ‘ ( 𝑅 ↾s 𝑈 ) )
257 eqid ⊢ ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) )
258 255 256 257 isgrp ⊢ ( ( 𝑅 ↾s 𝑈 ) ∈ Grp ↔ ( ( 𝑅 ↾s 𝑈 ) ∈ Mnd ∧ ∀ 𝑞 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∃ 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑤 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑞 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
259 254 258 sylibr ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑈 ) ∈ Grp )
260 259 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( 𝑅 ↾s 𝑈 ) ∈ Grp )
261 simplr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → 𝑏 ∈ 𝑈 )
262 57 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → 𝑈 = ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
263 262 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → 𝑈 = ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
264 263 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( 𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
265 261 264 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → 𝑏 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
266 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → 𝑑 ∈ 𝑈 )
267 263 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( 𝑑 ∈ 𝑈 ↔ 𝑑 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
268 266 267 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → 𝑑 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
269 255 256 grpcl ⊢ ( ( ( 𝑅 ↾s 𝑈 ) ∈ Grp ∧ 𝑏 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ 𝑑 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) → ( 𝑏 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑑 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
270 260 265 268 269 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( 𝑏 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑑 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
271 263 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( 𝑏 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑑 ) ∈ 𝑈 ↔ ( 𝑏 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑑 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
272 270 271 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( 𝑏 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑑 ) ∈ 𝑈 )
273 229 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( +g ‘ 𝑅 ) = ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) )
274 273 oveqdr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) = ( 𝑏 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑑 ) )
275 274 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ 𝑈 ↔ ( 𝑏 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑑 ) ∈ 𝑈 ) )
276 272 275 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑑 ∈ 𝑈 ) → ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ 𝑈 )
277 276 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ∀ 𝑑 ∈ 𝑈 ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ 𝑈 )
278 277 ralrimiva ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝑈 ∀ 𝑑 ∈ 𝑈 ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) ∈ 𝑈 )
279 278 187 mpbird ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑈 ) ∈ Mnd )
280 12 279 jca ⊢ ( 𝜑 → ( 𝑅 ∈ Mnd ∧ ( 𝑅 ↾s 𝑈 ) ∈ Mnd ) )
281 54 185 jca ⊢ ( 𝜑 → ( 𝑈 ⊆ ( Base ‘ 𝑅 ) ∧ ( 0g ‘ 𝑅 ) ∈ 𝑈 ) )
282 280 281 jca ⊢ ( 𝜑 → ( ( 𝑅 ∈ Mnd ∧ ( 𝑅 ↾s 𝑈 ) ∈ Mnd ) ∧ ( 𝑈 ⊆ ( Base ‘ 𝑅 ) ∧ ( 0g ‘ 𝑅 ) ∈ 𝑈 ) ) )
283 17 99 issubmndb ⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝑅 ) ↔ ( ( 𝑅 ∈ Mnd ∧ ( 𝑅 ↾s 𝑈 ) ∈ Mnd ) ∧ ( 𝑈 ⊆ ( Base ‘ 𝑅 ) ∧ ( 0g ‘ 𝑅 ) ∈ 𝑈 ) ) )
284 282 283 sylibr ⊢ ( 𝜑 → 𝑈 ∈ ( SubMnd ‘ 𝑅 ) )
285 284 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝑈 ∈ ( SubMnd ‘ 𝑅 ) )
286 285 6 43 3jca ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝑈 ∈ ( SubMnd ‘ 𝑅 ) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈 ) )
287 eqid ⊢ ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( .g ‘ ( 𝑅 ↾s 𝑈 ) )
288 7 55 287 submmulg ⊢ ( ( 𝑈 ∈ ( SubMnd ‘ 𝑅 ) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈 ) → ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) = ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) )
289 288 eqcomd ⊢ ( ( 𝑈 ∈ ( SubMnd ‘ 𝑅 ) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈 ) → ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) )
290 286 289 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) )
291 238 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( 0g ‘ 𝑅 ) )
292 290 291 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ↔ ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
293 33 292 mpbird ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
294 10 simp3d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) )
295 eqidd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ℕ0 = ℕ0 )
296 285 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → 𝑈 ∈ ( SubMnd ‘ 𝑅 ) )
297 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → 𝑙 ∈ ℕ0 )
298 43 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → 𝑐 ∈ 𝑈 )
299 296 297 298 3jca ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝑈 ∈ ( SubMnd ‘ 𝑅 ) ∧ 𝑙 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈 ) )
300 7 55 287 submmulg ⊢ ( ( 𝑈 ∈ ( SubMnd ‘ 𝑅 ) ∧ 𝑙 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈 ) → ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) )
301 299 300 syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) )
302 237 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
303 301 302 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
304 303 imbi1d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ↔ ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) )
305 295 304 raleqbidva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ↔ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) )
306 294 305 mpbid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) )
307 60 293 306 3jca ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) )
308 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) → 𝑅 ∈ CMnd )
309 62 3impa ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
310 71 3impa ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) → 𝑑 ∈ ( Base ‘ 𝑅 ) )
311 17 29 cmncom ⊢ ( ( 𝑅 ∈ CMnd ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑑 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) = ( 𝑑 ( +g ‘ 𝑅 ) 𝑏 ) )
312 308 309 310 311 syl3anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) → ( 𝑏 ( +g ‘ 𝑅 ) 𝑑 ) = ( 𝑑 ( +g ‘ 𝑅 ) 𝑏 ) )
313 57 229 279 312 iscmnd ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑈 ) ∈ CMnd )
314 313 5 287 isprimroot ⊢ ( 𝜑 → ( 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ↔ ( 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) ) )
315 314 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → ( 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ↔ ( 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) ) )
316 307 315 mpbird ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) → 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) )
317 316 ex ⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) → 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) )
318 317 ssrdv ⊢ ( 𝜑 → ( 𝑅 PrimRoots 𝐾 ) ⊆ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) )
319 313 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( 𝑅 ↾s 𝑈 ) ∈ CMnd )
320 5 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → 𝐾 ∈ ℕ0 )
321 319 320 287 isprimroot ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ↔ ( 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) ) )
322 321 biimpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) → ( 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) ) )
323 322 syldbl2 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) )
324 323 simp1d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
325 54 sselda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑈 ) → 𝑐 ∈ ( Base ‘ 𝑅 ) )
326 325 ex ⊢ ( 𝜑 → ( 𝑐 ∈ 𝑈 → 𝑐 ∈ ( Base ‘ 𝑅 ) ) )
327 57 eleq2d ⊢ ( 𝜑 → ( 𝑐 ∈ 𝑈 ↔ 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
328 327 imbi1d ⊢ ( 𝜑 → ( ( 𝑐 ∈ 𝑈 → 𝑐 ∈ ( Base ‘ 𝑅 ) ) ↔ ( 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) )
329 326 328 mpbid ⊢ ( 𝜑 → ( 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝑐 ∈ ( Base ‘ 𝑅 ) ) )
330 329 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝑐 ∈ ( Base ‘ 𝑅 ) ) )
331 330 imp ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) ∧ 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) → 𝑐 ∈ ( Base ‘ 𝑅 ) )
332 324 331 mpdan ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → 𝑐 ∈ ( Base ‘ 𝑅 ) )
333 284 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → 𝑈 ∈ ( SubMnd ‘ 𝑅 ) )
334 327 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( 𝑐 ∈ 𝑈 ↔ 𝑐 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
335 324 334 mpbird ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → 𝑐 ∈ 𝑈 )
336 333 320 335 288 syl3anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) = ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) )
337 323 simp2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
338 238 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( 0g ‘ 𝑅 ) )
339 336 337 338 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) )
340 323 simp3d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) )
341 333 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → 𝑈 ∈ ( SubMnd ‘ 𝑅 ) )
342 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → 𝑙 ∈ ℕ0 )
343 335 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → 𝑐 ∈ 𝑈 )
344 341 342 343 300 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) )
345 344 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) )
346 338 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( 0g ‘ 𝑅 ) )
347 345 346 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ↔ ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
348 347 imbi1d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ↔ ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
349 348 ralbidva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ↔ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
350 340 349 mpbid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) )
351 332 339 350 3jca ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
352 1 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → 𝑅 ∈ CMnd )
353 352 320 7 isprimroot ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → ( 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ↔ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑐 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
354 351 353 mpbird ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ) → 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) )
355 354 ex ⊢ ( 𝜑 → ( 𝑐 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) → 𝑐 ∈ ( 𝑅 PrimRoots 𝐾 ) ) )
356 355 ssrdv ⊢ ( 𝜑 → ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ⊆ ( 𝑅 PrimRoots 𝐾 ) )
357 318 356 eqssd ⊢ ( 𝜑 → ( 𝑅 PrimRoots 𝐾 ) = ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) )
358 259 313 jca ⊢ ( 𝜑 → ( ( 𝑅 ↾s 𝑈 ) ∈ Grp ∧ ( 𝑅 ↾s 𝑈 ) ∈ CMnd ) )
359 isabl ⊢ ( ( 𝑅 ↾s 𝑈 ) ∈ Abel ↔ ( ( 𝑅 ↾s 𝑈 ) ∈ Grp ∧ ( 𝑅 ↾s 𝑈 ) ∈ CMnd ) )
360 358 359 sylibr ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑈 ) ∈ Abel )
361 357 360 jca ⊢ ( 𝜑 → ( ( 𝑅 PrimRoots 𝐾 ) = ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ∧ ( 𝑅 ↾s 𝑈 ) ∈ Abel ) )