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 bilani ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) → ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) )
94 simpll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ∧ ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ) → 𝜑 )
95 simprl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ∧ ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ) → 𝑚 ∈ ( Base ‘ 𝐺 ) )
96 simprr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ∧ ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 )
97 94 95 96 jca31 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ∧ ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ) → ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) )
98 2 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
99 16 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
100 98 99 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
101 100 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
102 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝐷 ∈ ℕ )
103 15 sselda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) → 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
104 103 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
105 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑅 ∈ Ring )
106 10 16 unitsubm ⊢ ( 𝑅 ∈ Ring → ( Unit ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
107 105 106 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( Unit ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
108 104 23 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑚 ∈ ( Base ‘ 𝑅 ) )
109 101 cmnmndd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
110 4 nnzd ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
111 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
112 110 111 zsubcld ⊢ ( 𝜑 → ( 𝐷 − 1 ) ∈ ℤ )
113 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
114 113 addridd ⊢ ( 𝜑 → ( 1 + 0 ) = 1 )
115 4 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐷 )
116 114 115 eqbrtrd ⊢ ( 𝜑 → ( 1 + 0 ) ≤ 𝐷 )
117 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
118 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
119 4 nnred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
120 117 118 119 leaddsub2d ⊢ ( 𝜑 → ( ( 1 + 0 ) ≤ 𝐷 ↔ 0 ≤ ( 𝐷 − 1 ) ) )
121 116 120 mpbid ⊢ ( 𝜑 → 0 ≤ ( 𝐷 − 1 ) )
122 112 121 jca ⊢ ( 𝜑 → ( ( 𝐷 − 1 ) ∈ ℤ ∧ 0 ≤ ( 𝐷 − 1 ) ) )
123 elnn0z ⊢ ( ( 𝐷 − 1 ) ∈ ℕ0 ↔ ( ( 𝐷 − 1 ) ∈ ℤ ∧ 0 ≤ ( 𝐷 − 1 ) ) )
124 122 123 sylibr ⊢ ( 𝜑 → ( 𝐷 − 1 ) ∈ ℕ0 )
125 124 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐷 − 1 ) ∈ ℕ0 )
126 125 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝐷 − 1 ) ∈ ℕ0 )
127 18 73 109 126 108 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ∈ ( Base ‘ 𝑅 ) )
128 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ∧ 𝑜 = ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ) → 𝑜 = ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
129 128 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ∧ 𝑜 = ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ) → ( 𝑜 ( .r ‘ 𝑅 ) 𝑚 ) = ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( .r ‘ 𝑅 ) 𝑚 ) )
130 129 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ∧ 𝑜 = ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ) → ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) ↔ ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) ) )
131 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
132 16 131 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
133 132 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) ) )
134 133 oveqd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
135 102 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝐷 ∈ ℂ )
136 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 1 ∈ ℂ )
137 135 136 npcand ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( 𝐷 − 1 ) + 1 ) = 𝐷 )
138 137 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝐷 = ( ( 𝐷 − 1 ) + 1 ) )
139 138 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝐷 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( ( ( 𝐷 − 1 ) + 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
140 eqid ⊢ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
141 13 73 140 mulgnn0p1 ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ ( 𝐷 − 1 ) ∈ ℕ0 ∧ 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ) → ( ( ( 𝐷 − 1 ) + 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
142 109 126 104 141 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( 𝐷 − 1 ) + 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
143 139 142 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( 𝐷 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
144 16 65 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
145 144 a1i ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
146 145 eqcomd ⊢ ( 𝜑 → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
147 10 65 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
148 9 147 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
149 146 148 eqeltrd ⊢ ( 𝜑 → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
150 149 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
151 150 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
152 24 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( Unit ‘ 𝑅 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
153 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
154 1 13 153 ress0g ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) ∧ ( Unit ‘ 𝑅 ) ⊆ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 0g ‘ 𝐺 ) )
155 109 151 152 154 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 0g ‘ 𝐺 ) )
156 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 )
157 156 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝐷 = ( ( od ‘ 𝐺 ) ‘ 𝑚 ) )
158 157 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝐷 ( .g ‘ 𝐺 ) 𝑚 ) = ( ( ( od ‘ 𝐺 ) ‘ 𝑚 ) ( .g ‘ 𝐺 ) 𝑚 ) )
159 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
160 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
161 7 159 8 160 odid ⊢ ( 𝑚 ∈ ( Base ‘ 𝐺 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑚 ) ( .g ‘ 𝐺 ) 𝑚 ) = ( 0g ‘ 𝐺 ) )
162 161 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑚 ) ( .g ‘ 𝐺 ) 𝑚 ) = ( 0g ‘ 𝐺 ) )
163 158 162 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝐷 ( .g ‘ 𝐺 ) 𝑚 ) = ( 0g ‘ 𝐺 ) )
164 163 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 0g ‘ 𝐺 ) = ( 𝐷 ( .g ‘ 𝐺 ) 𝑚 ) )
165 155 164 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 𝐷 ( .g ‘ 𝐺 ) 𝑚 ) )
166 32 sselda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) → 𝑚 ∈ ( Unit ‘ 𝑅 ) )
167 166 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑚 ∈ ( Unit ‘ 𝑅 ) )
168 1 152 167 102 ressmulgnnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝐷 ( .g ‘ 𝐺 ) 𝑚 ) = ( 𝐷 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) )
169 165 168 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝐷 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
170 143 169 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
171 144 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
172 171 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
173 170 172 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) = ( 1r ‘ 𝑅 ) )
174 134 173 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( ( 𝐷 − 1 ) ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑚 ) ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) )
175 127 130 174 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ∃ 𝑜 ∈ ( Base ‘ 𝑅 ) ( 𝑜 ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) )
176 108 175 jca ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑜 ∈ ( Base ‘ 𝑅 ) ( 𝑜 ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) ) )
177 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
178 17 177 131 dvdsr ⊢ ( 𝑚 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ↔ ( 𝑚 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑜 ∈ ( Base ‘ 𝑅 ) ( 𝑜 ( .r ‘ 𝑅 ) 𝑚 ) = ( 1r ‘ 𝑅 ) ) )
179 176 178 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑚 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
180 98 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) → 𝑅 ∈ CRing )
181 180 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑅 ∈ CRing )
182 10 65 177 crngunit ⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ ( Unit ‘ 𝑅 ) ↔ 𝑚 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
183 181 182 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( 𝑚 ∈ ( Unit ‘ 𝑅 ) ↔ 𝑚 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
184 179 183 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑚 ∈ ( Unit ‘ 𝑅 ) )
185 eqid ⊢ ( od ‘ ( mulGrp ‘ 𝑅 ) ) = ( od ‘ ( mulGrp ‘ 𝑅 ) )
186 1 185 159 submod ⊢ ( ( ( Unit ‘ 𝑅 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ∧ 𝑚 ∈ ( Unit ‘ 𝑅 ) ) → ( ( od ‘ ( mulGrp ‘ 𝑅 ) ) ‘ 𝑚 ) = ( ( od ‘ 𝐺 ) ‘ 𝑚 ) )
187 107 184 186 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( od ‘ ( mulGrp ‘ 𝑅 ) ) ‘ 𝑚 ) = ( ( od ‘ 𝐺 ) ‘ 𝑚 ) )
188 187 156 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → ( ( od ‘ ( mulGrp ‘ 𝑅 ) ) ‘ 𝑚 ) = 𝐷 )
189 101 102 104 188 isprimroot2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( Base ‘ 𝐺 ) ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) → 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) )
190 97 189 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) ∧ ( 𝑚 ∈ ( Base ‘ 𝐺 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑚 ) = 𝐷 ) ) → 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) )
191 93 190 mpdan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } ) → 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) )
192 191 ex ⊢ ( 𝜑 → ( 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } → 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) ) )
193 90 192 eximd ⊢ ( 𝜑 → ( ∃ 𝑚 𝑚 ∈ { 𝑤 ∈ ( Base ‘ 𝐺 ) ∣ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝐷 } → ∃ 𝑚 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) ) )
194 89 193 mpd ⊢ ( 𝜑 → ∃ 𝑚 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) )
195 n0 ⊢ ( ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) ≠ ∅ ↔ ∃ 𝑚 𝑚 ∈ ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) )
196 194 195 sylibr ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑅 ) PrimRoots 𝐷 ) ≠ ∅ )