Metamath Proof Explorer

Theorem unitscyglem5

Description: Lemma for unitscyg (Contributed by metakunt, 9-Aug-2025)

Ref Expression
Hypotheses unitscyglem5.1 ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
unitscyglem5.2 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
unitscyglem5.3 ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ Fin )
unitscyglem5.4 ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
unitscyglem5.5 ⊢ ( 𝜑 → 𝐷 ∥ ( ♯ ‘ ( Base ‘ 𝐺 ) ) )
Assertion unitscyglem5 ( 𝜑 → ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 unitscyglem5.1 ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
2 unitscyglem5.2 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
3 unitscyglem5.3 ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ Fin )
4 unitscyglem5.4 ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
5 unitscyglem5.5 ⊢ ( 𝜑 → 𝐷 ∥ ( ♯ ‘ ( Base ‘ 𝐺 ) ) )
6 4 phicld ⊢ ( 𝜑 → ( ϕ ‘ 𝐷 ) ∈ ℕ )
7 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
8 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
9 2 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
11 10 1 unitgrp ⊢ ( 𝑅 ∈ Ring → 𝐺 ∈ Grp )
12 9 11 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
13 eqid ⊢ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
14 1 13 ressbasss ⊢ ( Base ‘ 𝐺 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝑅 ) )
15 14 a1i ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
16 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
17 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
18 16 17 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
19 18 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
20 19 eqimsscd ⊢ ( 𝜑 → ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ⊆ ( Base ‘ 𝑅 ) )
21 15 20 sstrd ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) ⊆ ( Base ‘ 𝑅 ) )
22 3 21 ssfid ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) ∈ Fin )
23 18 eqcomi ⊢ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) = ( Base ‘ 𝑅 )
24 23 10 unitss ⊢ ( Unit ‘ 𝑅 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝑅 ) )
25 24 a1i ⊢ ( 𝜑 → ( Unit ‘ 𝑅 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( Unit ‘ 𝑅 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( Unit ‘ 𝑅 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
28 1 13 ressbasssg ⊢ ( Base ‘ 𝐺 ) ⊆ ( ( Unit ‘ 𝑅 ) ∩ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
29 28 a1i ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) ⊆ ( ( Unit ‘ 𝑅 ) ∩ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ) )
30 inss1 ⊢ ( ( Unit ‘ 𝑅 ) ∩ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ) ⊆ ( Unit ‘ 𝑅 )
31 30 a1i ⊢ ( 𝜑 → ( ( Unit ‘ 𝑅 ) ∩ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ) ⊆ ( Unit ‘ 𝑅 ) )
32 29 31 sstrd ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) ⊆ ( Unit ‘ 𝑅 ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( Base ‘ 𝐺 ) ⊆ ( Unit ‘ 𝑅 ) )
34 33 sseld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( 𝑧 ∈ ( Base ‘ 𝐺 ) → 𝑧 ∈ ( Unit ‘ 𝑅 ) ) )
35 34 imp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → 𝑧 ∈ ( Unit ‘ 𝑅 ) )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℕ )
37 36 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → 𝑦 ∈ ℕ )
38 1 27 35 37 ressmulgnnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) )
39 38 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) ↔ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) ) )
40 39 rabbidva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) } = { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } )
41 40 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) = ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) )
42 fvex ⊢ ( Base ‘ 𝐺 ) ∈ V
43 42 rabex ⊢ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ∈ V
44 43 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ∈ V )
45 hashxrcl ⊢ ( { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ∈ V → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ∈ ℝ* )
46 44 45 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ∈ ℝ* )
47 41 46 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ∈ ℝ* )
48 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
49 48 rabex ⊢ { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ∈ V
50 49 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ∈ V )
51 hashxrcl ⊢ ( { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ∈ V → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ∈ ℝ* )
52 50 51 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ∈ ℝ* )
53 nnre ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℝ )
55 54 rexrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℝ* )
56 simprl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐺 ) )
57 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) ) ) → ( Base ‘ 𝐺 ) ⊆ ( Base ‘ 𝑅 ) )
58 57 sseld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) ) ) → ( 𝑧 ∈ ( Base ‘ 𝐺 ) → 𝑧 ∈ ( Base ‘ 𝑅 ) ) )
59 56 58 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
60 59 rabss3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ⊆ { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } )
61 50 60 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ∈ V ∧ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ⊆ { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) )
62 hashss ⊢ ( ( { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ∈ V ∧ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ⊆ { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) )
63 61 62 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) )
64 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → 𝑅 ∈ IDomn )
65 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
66 10 1 65 unitgrpid ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝐺 ) )
67 9 66 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝐺 ) )
68 67 eqcomd ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) = ( 1r ‘ 𝑅 ) )
69 17 65 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
70 9 69 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
71 68 70 eqeltrd ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝑅 ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝑅 ) )
73 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑅 ) ) = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
74 17 73 idomrootle ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ℕ ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑦 )
75 64 72 36 74 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑦 )
76 47 52 55 63 75 xrletrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑦 )
77 41 76 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑦 )
78 77 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℕ ( ♯ ‘ { 𝑧 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑦 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) } ) ≤ 𝑦 )
79 7 8 12 22 78 4 5 unitscyglem4 ⊢ ( 𝜑 → ( ♯ ‘ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) = ( ϕ ‘ 𝐷 ) )
80 79 eleq1d ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ∈ ℕ ↔ ( ϕ ‘ 𝐷 ) ∈ ℕ ) )
81 6 80 mpbird ⊢ ( 𝜑 → ( ♯ ‘ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ∈ ℕ )
82 81 nngt0d ⊢ ( 𝜑 → 0 < ( ♯ ‘ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) )
83 42 rabex ⊢ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ∈ V
84 83 a1i ⊢ ( 𝜑 → { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ∈ V )
85 hashneq0 ⊢ ( { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ∈ V → ( 0 < ( ♯ ‘ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ↔ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ≠ ∅ ) )
86 84 85 syl ⊢ ( 𝜑 → ( 0 < ( ♯ ‘ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ↔ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ≠ ∅ ) )
87 82 86 mpbid ⊢ ( 𝜑 → { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ≠ ∅ )
88 n0 ⊢ ( { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ≠ ∅ ↔ ∃ 𝑚 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } )
89 87 88 sylib ⊢ ( 𝜑 → ∃ 𝑚 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } )
90 nfv ⊢ Ⅎ 𝑚 𝜑
91 fveqeq2 ⊢ ( 𝑤 = 𝑚 → ( ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) )
92 91 elrab ⊢ ( 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ↔ ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) )
93 92 biimpi ⊢ ( 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } → ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) )
94 93 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) → ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) )
95 simpll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ∧ ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ) → 𝜑 )
96 simprl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ∧ ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ) → 𝑚 ∈ ( Base ‘ 𝐺 ) )
97 simprr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ∧ ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 )
98 95 96 97 jca31 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ∧ ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ) → ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) )
99 2 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
100 16 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
101 99 100 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
102 101 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
103 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝐷 ∈ ℕ )
104 15 sselda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) → 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
105 104 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
106 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑅 ∈ Ring )
107 10 16 unitsubm ⊢ ( 𝑅 ∈ Ring → ( Unit ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
108 106 107 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( Unit ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
109 105 23 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑚 ∈ ( Base ‘ 𝑅 ) )
110 102 cmnmndd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
111 4 nnzd ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
112 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
113 111 112 zsubcld ⊢ ( 𝜑 → ( 𝐷 − 1 ) ∈ ℤ )
114 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
115 114 addridd ⊢ ( 𝜑 → ( 1 + 0 ) = 1 )
116 4 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐷 )
117 115 116 eqbrtrd ⊢ ( 𝜑 → ( 1 + 0 ) ≤ 𝐷 )
118 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
119 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
120 4 nnred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
121 118 119 120 leaddsub2d ⊢ ( 𝜑 → ( ( 1 + 0 ) ≤ 𝐷 ↔ 0 ≤ ( 𝐷 − 1 ) ) )
122 117 121 mpbid ⊢ ( 𝜑 → 0 ≤ ( 𝐷 − 1 ) )
123 113 122 jca ⊢ ( 𝜑 → ( ( 𝐷 − 1 ) ∈ ℤ ∧ 0 ≤ ( 𝐷 − 1 ) ) )
124 elnn0z ⊢ ( ( 𝐷 − 1 ) ∈ ℕ0 ↔ ( ( 𝐷 − 1 ) ∈ ℤ ∧ 0 ≤ ( 𝐷 − 1 ) ) )
125 123 124 sylibr ⊢ ( 𝜑 → ( 𝐷 − 1 ) ∈ ℕ0 )
126 125 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐷 − 1 ) ∈ ℕ0 )
127 126 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝐷 − 1 ) ∈ ℕ0 )
128 18 73 110 127 109 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ∈ ( Base ‘ 𝑅 ) )
129 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ∧ 𝑜 = ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ) → 𝑜 = ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
130 129 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ∧ 𝑜 = ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ) → ( 𝑜 ( .r ‘ 𝑅 ) 𝑚 ) = ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( .r ‘ 𝑅 ) 𝑚 ) )
131 130 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ∧ 𝑜 = ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ) → ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) ↔ ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) ) )
132 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
133 16 132 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
134 133 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) ) )
135 134 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
136 103 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝐷 ∈ ℂ )
137 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 1 ∈ ℂ )
138 136 137 npcand ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( 𝐷 − 1 ) + 1 ) = 𝐷 )
139 138 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝐷 = ( ( 𝐷 − 1 ) + 1 ) )
140 139 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝐷 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( ( ( 𝐷 − 1 ) + 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
141 eqid ⊢ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
142 13 73 141 mulgnn0p1 ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ ( 𝐷 − 1 ) ∈ ℕ0 ∧ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ) → ( ( ( 𝐷 − 1 ) + 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
143 110 127 105 142 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( 𝐷 − 1 ) + 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
144 140 143 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( 𝐷 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
145 16 65 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
146 145 a1i ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
147 146 eqcomd ⊢ ( 𝜑 → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
148 10 65 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
149 9 148 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
150 147 149 eqeltrd ⊢ ( 𝜑 → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
151 150 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
152 151 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
153 24 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( Unit ‘ 𝑅 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
154 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
155 1 13 154 ress0g ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) ∧ ( Unit ‘ 𝑅 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 0g ‘ 𝐺 ) )
156 110 152 153 155 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 0g ‘ 𝐺 ) )
157 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 )
158 157 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝐷 = ( ( od ‘ 𝐺 ) ‘ 𝑚 ) )
159 158 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝐷 ( .g ‘ 𝐺 ) 𝑚 ) = ( ( ( od ‘ 𝐺 ) ‘ 𝑚 ) ( .g ‘ 𝐺 ) 𝑚 ) )
160 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
161 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
162 7 160 8 161 odid ⊢ ( 𝑚 ∈ ( Base ‘ 𝐺 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑚 ) ( .g ‘ 𝐺 ) 𝑚 ) = ( 0g ‘ 𝐺 ) )
163 162 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑚 ) ( .g ‘ 𝐺 ) 𝑚 ) = ( 0g ‘ 𝐺 ) )
164 159 163 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝐷 ( .g ‘ 𝐺 ) 𝑚 ) = ( 0g ‘ 𝐺 ) )
165 164 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 0g ‘ 𝐺 ) = ( 𝐷 ( .g ‘ 𝐺 ) 𝑚 ) )
166 156 165 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 𝐷 ( .g ‘ 𝐺 ) 𝑚 ) )
167 32 sselda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) → 𝑚 ∈ ( Unit ‘ 𝑅 ) )
168 167 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑚 ∈ ( Unit ‘ 𝑅 ) )
169 1 153 168 103 ressmulgnnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝐷 ( .g ‘ 𝐺 ) 𝑚 ) = ( 𝐷 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
170 166 169 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝐷 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
171 144 170 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
172 145 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
173 172 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
174 171 173 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( 1r ‘ 𝑅 ) )
175 135 174 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) )
176 128 131 175 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ∃ 𝑜 ∈ ( Base ‘ 𝑅 ) ( 𝑜 ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) )
177 109 176 jca ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑜 ∈ ( Base ‘ 𝑅 ) ( 𝑜 ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) ) )
178 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
179 17 178 132 dvdsr ⊢ ( 𝑚 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ↔ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑜 ∈ ( Base ‘ 𝑅 ) ( 𝑜 ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) ) )
180 177 179 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑚 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
181 99 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) → 𝑅 ∈ CRing )
182 181 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑅 ∈ CRing )
183 10 65 178 crngunit ⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ ( Unit ‘ 𝑅 ) ↔ 𝑚 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
184 182 183 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝑚 ∈ ( Unit ‘ 𝑅 ) ↔ 𝑚 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
185 180 184 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑚 ∈ ( Unit ‘ 𝑅 ) )
186 eqid ⊢ ( od ‘ ( mulGrp ‘ 𝑅 ) ) = ( od ‘ ( mulGrp ‘ 𝑅 ) )
187 1 186 160 submod ⊢ ( ( ( Unit ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ∧ 𝑚 ∈ ( Unit ‘ 𝑅 ) ) → ( ( od ‘ ( mulGrp ‘ 𝑅 ) ) ‘ 𝑚 ) = ( ( od ‘ 𝐺 ) ‘ 𝑚 ) )
188 108 185 187 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( od ‘ ( mulGrp ‘ 𝑅 ) ) ‘ 𝑚 ) = ( ( od ‘ 𝐺 ) ‘ 𝑚 ) )
189 188 157 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( od ‘ ( mulGrp ‘ 𝑅 ) ) ‘ 𝑚 ) = 𝐷 )
190 102 103 105 189 isprimroot2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) )
191 98 190 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ∧ ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ) → 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) )
192 94 191 mpdan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) → 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) )
193 192 ex ⊢ ( 𝜑 → ( 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } → 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) ) )
194 90 193 eximd ⊢ ( 𝜑 → ( ∃ 𝑚 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } → ∃ 𝑚 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) ) )
195 89 194 mpd ⊢ ( 𝜑 → ∃ 𝑚 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) )
196 n0 ⊢ ( ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) ≠ ∅ ↔ ∃ 𝑚 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) )
197 195 196 sylibr ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) ≠ ∅ )