| Step | Hyp | Ref
| Expression |
| 1 | | unitscyglem5.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ℕ) |
| 2 | 1 | phicld 16809 |
. . . . . . 7
⊢ (𝜑 → (ϕ‘𝐷) ∈
ℕ) |
| 3 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 4 | | eqid 2737 |
. . . . . . . . 9
⊢
(.g‘𝐺) = (.g‘𝐺) |
| 5 | | unitscyglem5.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ IDomn) |
| 6 | 5 | idomringd 20728 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 7 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
| 8 | | unitscyglem5.1 |
. . . . . . . . . . 11
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s
(Unit‘𝑅)) |
| 9 | 7, 8 | unitgrp 20383 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝐺 ∈ Grp) |
| 10 | 6, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 11 | | unitscyglem5.3 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝑅) ∈ Fin) |
| 12 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅)) |
| 13 | 8, 12 | ressbasss 17284 |
. . . . . . . . . . . 12
⊢
(Base‘𝐺)
⊆ (Base‘(mulGrp‘𝑅)) |
| 14 | 13 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝐺) ⊆
(Base‘(mulGrp‘𝑅))) |
| 15 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 16 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 17 | 15, 16 | mgpbas 20142 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
| 18 | 17 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(mulGrp‘𝑅))) |
| 19 | 18 | eqimsscd 4041 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Base‘(mulGrp‘𝑅)) ⊆ (Base‘𝑅)) |
| 20 | 14, 19 | sstrd 3994 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝐺) ⊆ (Base‘𝑅)) |
| 21 | 11, 20 | ssfid 9301 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝐺) ∈ Fin) |
| 22 | 17 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘(mulGrp‘𝑅)) = (Base‘𝑅) |
| 23 | 22, 7 | unitss 20376 |
. . . . . . . . . . . . . . . . . 18
⊢
(Unit‘𝑅)
⊆ (Base‘(mulGrp‘𝑅)) |
| 24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Unit‘𝑅) ⊆
(Base‘(mulGrp‘𝑅))) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (Unit‘𝑅) ⊆
(Base‘(mulGrp‘𝑅))) |
| 26 | 25 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (Base‘𝐺)) → (Unit‘𝑅) ⊆ (Base‘(mulGrp‘𝑅))) |
| 27 | 8, 12 | ressbasssg 17282 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘𝐺)
⊆ ((Unit‘𝑅)
∩ (Base‘(mulGrp‘𝑅))) |
| 28 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (Base‘𝐺) ⊆ ((Unit‘𝑅) ∩
(Base‘(mulGrp‘𝑅)))) |
| 29 | | inss1 4237 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((Unit‘𝑅)
∩ (Base‘(mulGrp‘𝑅))) ⊆ (Unit‘𝑅) |
| 30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((Unit‘𝑅) ∩
(Base‘(mulGrp‘𝑅))) ⊆ (Unit‘𝑅)) |
| 31 | 28, 30 | sstrd 3994 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (Base‘𝐺) ⊆ (Unit‘𝑅)) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (Base‘𝐺) ⊆ (Unit‘𝑅)) |
| 33 | 32 | sseld 3982 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (𝑧 ∈ (Base‘𝐺) → 𝑧 ∈ (Unit‘𝑅))) |
| 34 | 33 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (Base‘𝐺)) → 𝑧 ∈ (Unit‘𝑅)) |
| 35 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ) |
| 36 | 35 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (Base‘𝐺)) → 𝑦 ∈ ℕ) |
| 37 | 8, 26, 34, 36 | ressmulgnnd 19096 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑦(.g‘𝐺)𝑧) = (𝑦(.g‘(mulGrp‘𝑅))𝑧)) |
| 38 | 37 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝑧 ∈ (Base‘𝐺)) → ((𝑦(.g‘𝐺)𝑧) = (0g‘𝐺) ↔ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺))) |
| 39 | 38 | rabbidva 3443 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → {𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘𝐺)𝑧) = (0g‘𝐺)} = {𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)}) |
| 40 | 39 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (♯‘{𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘𝐺)𝑧) = (0g‘𝐺)}) = (♯‘{𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)})) |
| 41 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐺)
∈ V |
| 42 | 41 | rabex 5339 |
. . . . . . . . . . . . . . 15
⊢ {𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘𝐺)𝑧) = (0g‘𝐺)} ∈ V |
| 43 | 42 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → {𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘𝐺)𝑧) = (0g‘𝐺)} ∈ V) |
| 44 | | hashxrcl 14396 |
. . . . . . . . . . . . . 14
⊢ ({𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘𝐺)𝑧) = (0g‘𝐺)} ∈ V → (♯‘{𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘𝐺)𝑧) = (0g‘𝐺)}) ∈
ℝ*) |
| 45 | 43, 44 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (♯‘{𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘𝐺)𝑧) = (0g‘𝐺)}) ∈
ℝ*) |
| 46 | 40, 45 | eqeltrrd 2842 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (♯‘{𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)}) ∈
ℝ*) |
| 47 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑅)
∈ V |
| 48 | 47 | rabex 5339 |
. . . . . . . . . . . . . 14
⊢ {𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)} ∈ V |
| 49 | 48 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → {𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)} ∈ V) |
| 50 | | hashxrcl 14396 |
. . . . . . . . . . . . 13
⊢ ({𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)} ∈ V → (♯‘{𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)}) ∈
ℝ*) |
| 51 | 49, 50 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (♯‘{𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)}) ∈
ℝ*) |
| 52 | | nnre 12273 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
| 53 | 52 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ) |
| 54 | 53 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ*) |
| 55 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ (Base‘𝐺) ∧ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺))) → 𝑧 ∈ (Base‘𝐺)) |
| 56 | 20 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ (Base‘𝐺) ∧ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺))) → (Base‘𝐺) ⊆ (Base‘𝑅)) |
| 57 | 56 | sseld 3982 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ (Base‘𝐺) ∧ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺))) → (𝑧 ∈ (Base‘𝐺) → 𝑧 ∈ (Base‘𝑅))) |
| 58 | 55, 57 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ (𝑧 ∈ (Base‘𝐺) ∧ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺))) → 𝑧 ∈ (Base‘𝑅)) |
| 59 | 58 | rabss3d 4081 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → {𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)} ⊆ {𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)}) |
| 60 | 49, 59 | jca 511 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → ({𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)} ∈ V ∧ {𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)} ⊆ {𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)})) |
| 61 | | hashss 14448 |
. . . . . . . . . . . . 13
⊢ (({𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)} ∈ V ∧ {𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)} ⊆ {𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)}) → (♯‘{𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)}) ≤ (♯‘{𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)})) |
| 62 | 60, 61 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (♯‘{𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)}) ≤ (♯‘{𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)})) |
| 63 | 5 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → 𝑅 ∈ IDomn) |
| 64 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 65 | 7, 8, 64 | unitgrpid 20385 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring →
(1r‘𝑅) =
(0g‘𝐺)) |
| 66 | 6, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1r‘𝑅) = (0g‘𝐺)) |
| 67 | 66 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0g‘𝐺) = (1r‘𝑅)) |
| 68 | 16, 64 | ringidcl 20262 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
| 69 | 6, 68 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) |
| 70 | 67, 69 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐺) ∈ (Base‘𝑅)) |
| 71 | 70 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) →
(0g‘𝐺)
∈ (Base‘𝑅)) |
| 72 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(.g‘(mulGrp‘𝑅)) =
(.g‘(mulGrp‘𝑅)) |
| 73 | 16, 72 | idomrootle 26212 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ IDomn ∧
(0g‘𝐺)
∈ (Base‘𝑅) ∧
𝑦 ∈ ℕ) →
(♯‘{𝑧 ∈
(Base‘𝑅) ∣
(𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)}) ≤ 𝑦) |
| 74 | 63, 71, 35, 73 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (♯‘{𝑧 ∈ (Base‘𝑅) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)}) ≤ 𝑦) |
| 75 | 46, 51, 54, 62, 74 | xrletrd 13204 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (♯‘{𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘(mulGrp‘𝑅))𝑧) = (0g‘𝐺)}) ≤ 𝑦) |
| 76 | 40, 75 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ) → (♯‘{𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘𝐺)𝑧) = (0g‘𝐺)}) ≤ 𝑦) |
| 77 | 76 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ ℕ (♯‘{𝑧 ∈ (Base‘𝐺) ∣ (𝑦(.g‘𝐺)𝑧) = (0g‘𝐺)}) ≤ 𝑦) |
| 78 | | unitscyglem5.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∥ (♯‘(Base‘𝐺))) |
| 79 | 3, 4, 10, 21, 77, 1, 78 | unitscyglem4 42199 |
. . . . . . . 8
⊢ (𝜑 → (♯‘{𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷}) = (ϕ‘𝐷)) |
| 80 | 79 | eleq1d 2826 |
. . . . . . 7
⊢ (𝜑 → ((♯‘{𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷}) ∈ ℕ ↔ (ϕ‘𝐷) ∈
ℕ)) |
| 81 | 2, 80 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → (♯‘{𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷}) ∈ ℕ) |
| 82 | 81 | nngt0d 12315 |
. . . . 5
⊢ (𝜑 → 0 <
(♯‘{𝑤 ∈
(Base‘𝐺) ∣
((od‘𝐺)‘𝑤) = 𝐷})) |
| 83 | 41 | rabex 5339 |
. . . . . . 7
⊢ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷} ∈ V |
| 84 | 83 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷} ∈ V) |
| 85 | | hashneq0 14403 |
. . . . . 6
⊢ ({𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷} ∈ V → (0 <
(♯‘{𝑤 ∈
(Base‘𝐺) ∣
((od‘𝐺)‘𝑤) = 𝐷}) ↔ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷} ≠ ∅)) |
| 86 | 84, 85 | syl 17 |
. . . . 5
⊢ (𝜑 → (0 <
(♯‘{𝑤 ∈
(Base‘𝐺) ∣
((od‘𝐺)‘𝑤) = 𝐷}) ↔ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷} ≠ ∅)) |
| 87 | 82, 86 | mpbid 232 |
. . . 4
⊢ (𝜑 → {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷} ≠ ∅) |
| 88 | | n0 4353 |
. . . 4
⊢ ({𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷} ≠ ∅ ↔ ∃𝑚 𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷}) |
| 89 | 87, 88 | sylib 218 |
. . 3
⊢ (𝜑 → ∃𝑚 𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷}) |
| 90 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑚𝜑 |
| 91 | | fveqeq2 6915 |
. . . . . . . . 9
⊢ (𝑤 = 𝑚 → (((od‘𝐺)‘𝑤) = 𝐷 ↔ ((od‘𝐺)‘𝑚) = 𝐷)) |
| 92 | 91 | elrab 3692 |
. . . . . . . 8
⊢ (𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷} ↔ (𝑚 ∈ (Base‘𝐺) ∧ ((od‘𝐺)‘𝑚) = 𝐷)) |
| 93 | 92 | biimpi 216 |
. . . . . . 7
⊢ (𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷} → (𝑚 ∈ (Base‘𝐺) ∧ ((od‘𝐺)‘𝑚) = 𝐷)) |
| 94 | 93 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷}) → (𝑚 ∈ (Base‘𝐺) ∧ ((od‘𝐺)‘𝑚) = 𝐷)) |
| 95 | | simpll 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷}) ∧ (𝑚 ∈ (Base‘𝐺) ∧ ((od‘𝐺)‘𝑚) = 𝐷)) → 𝜑) |
| 96 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷}) ∧ (𝑚 ∈ (Base‘𝐺) ∧ ((od‘𝐺)‘𝑚) = 𝐷)) → 𝑚 ∈ (Base‘𝐺)) |
| 97 | | simprr 773 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷}) ∧ (𝑚 ∈ (Base‘𝐺) ∧ ((od‘𝐺)‘𝑚) = 𝐷)) → ((od‘𝐺)‘𝑚) = 𝐷) |
| 98 | 95, 96, 97 | jca31 514 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷}) ∧ (𝑚 ∈ (Base‘𝐺) ∧ ((od‘𝐺)‘𝑚) = 𝐷)) → ((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷)) |
| 99 | 5 | idomcringd 20727 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 100 | 15 | crngmgp 20238 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
CMnd) |
| 101 | 99, 100 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd) |
| 102 | 101 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (mulGrp‘𝑅) ∈ CMnd) |
| 103 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 𝐷 ∈ ℕ) |
| 104 | 14 | sselda 3983 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) → 𝑚 ∈ (Base‘(mulGrp‘𝑅))) |
| 105 | 104 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 𝑚 ∈ (Base‘(mulGrp‘𝑅))) |
| 106 | 6 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 𝑅 ∈ Ring) |
| 107 | 7, 15 | unitsubm 20386 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
(Unit‘𝑅) ∈
(SubMnd‘(mulGrp‘𝑅))) |
| 108 | 106, 107 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (Unit‘𝑅) ∈ (SubMnd‘(mulGrp‘𝑅))) |
| 109 | 105, 22 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 𝑚 ∈ (Base‘𝑅)) |
| 110 | 102 | cmnmndd 19822 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (mulGrp‘𝑅) ∈ Mnd) |
| 111 | 1 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐷 ∈ ℤ) |
| 112 | | 1zzd 12648 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
ℤ) |
| 113 | 111, 112 | zsubcld 12727 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐷 − 1) ∈ ℤ) |
| 114 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 ∈
ℂ) |
| 115 | 114 | addridd 11461 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1 + 0) =
1) |
| 116 | 1 | nnge1d 12314 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ≤ 𝐷) |
| 117 | 115, 116 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 + 0) ≤ 𝐷) |
| 118 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ∈
ℝ) |
| 119 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 ∈
ℝ) |
| 120 | 1 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐷 ∈ ℝ) |
| 121 | 118, 119,
120 | leaddsub2d 11865 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((1 + 0) ≤ 𝐷 ↔ 0 ≤ (𝐷 − 1))) |
| 122 | 117, 121 | mpbid 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≤ (𝐷 − 1)) |
| 123 | 113, 122 | jca 511 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐷 − 1) ∈ ℤ ∧ 0 ≤
(𝐷 −
1))) |
| 124 | | elnn0z 12626 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 − 1) ∈
ℕ0 ↔ ((𝐷 − 1) ∈ ℤ ∧ 0 ≤
(𝐷 −
1))) |
| 125 | 123, 124 | sylibr 234 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷 − 1) ∈
ℕ0) |
| 126 | 125 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) → (𝐷 − 1) ∈
ℕ0) |
| 127 | 126 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (𝐷 − 1) ∈
ℕ0) |
| 128 | 17, 72, 110, 127, 109 | mulgnn0cld 19113 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → ((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚) ∈ (Base‘𝑅)) |
| 129 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) ∧ 𝑜 = ((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)) → 𝑜 = ((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)) |
| 130 | 129 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) ∧ 𝑜 = ((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)) → (𝑜(.r‘𝑅)𝑚) = (((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)(.r‘𝑅)𝑚)) |
| 131 | 130 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) ∧ 𝑜 = ((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)) → ((𝑜(.r‘𝑅)𝑚) = (1r‘𝑅) ↔ (((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)(.r‘𝑅)𝑚) = (1r‘𝑅))) |
| 132 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 133 | 15, 132 | mgpplusg 20141 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
| 134 | 133 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (.r‘𝑅) =
(+g‘(mulGrp‘𝑅))) |
| 135 | 134 | oveqd 7448 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)(.r‘𝑅)𝑚) = (((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)(+g‘(mulGrp‘𝑅))𝑚)) |
| 136 | 103 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 𝐷 ∈ ℂ) |
| 137 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 1 ∈ ℂ) |
| 138 | 136, 137 | npcand 11624 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → ((𝐷 − 1) + 1) = 𝐷) |
| 139 | 138 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 𝐷 = ((𝐷 − 1) + 1)) |
| 140 | 139 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (𝐷(.g‘(mulGrp‘𝑅))𝑚) = (((𝐷 − 1) +
1)(.g‘(mulGrp‘𝑅))𝑚)) |
| 141 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(+g‘(mulGrp‘𝑅)) =
(+g‘(mulGrp‘𝑅)) |
| 142 | 12, 72, 141 | mulgnn0p1 19103 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ (𝐷 −
1) ∈ ℕ0 ∧ 𝑚 ∈ (Base‘(mulGrp‘𝑅))) → (((𝐷 − 1) +
1)(.g‘(mulGrp‘𝑅))𝑚) = (((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)(+g‘(mulGrp‘𝑅))𝑚)) |
| 143 | 110, 127,
105, 142 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (((𝐷 − 1) +
1)(.g‘(mulGrp‘𝑅))𝑚) = (((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)(+g‘(mulGrp‘𝑅))𝑚)) |
| 144 | 140, 143 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)(+g‘(mulGrp‘𝑅))𝑚) = (𝐷(.g‘(mulGrp‘𝑅))𝑚)) |
| 145 | 15, 64 | ringidval 20180 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(1r‘𝑅) = (0g‘(mulGrp‘𝑅)) |
| 146 | 145 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (1r‘𝑅) =
(0g‘(mulGrp‘𝑅))) |
| 147 | 146 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 →
(0g‘(mulGrp‘𝑅)) = (1r‘𝑅)) |
| 148 | 7, 64 | 1unit 20374 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Unit‘𝑅)) |
| 149 | 6, 148 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1r‘𝑅) ∈ (Unit‘𝑅)) |
| 150 | 147, 149 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 →
(0g‘(mulGrp‘𝑅)) ∈ (Unit‘𝑅)) |
| 151 | 150 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) →
(0g‘(mulGrp‘𝑅)) ∈ (Unit‘𝑅)) |
| 152 | 151 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) →
(0g‘(mulGrp‘𝑅)) ∈ (Unit‘𝑅)) |
| 153 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (Unit‘𝑅) ⊆ (Base‘(mulGrp‘𝑅))) |
| 154 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘(mulGrp‘𝑅)) =
(0g‘(mulGrp‘𝑅)) |
| 155 | 8, 12, 154 | ress0g 18775 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ (0g‘(mulGrp‘𝑅)) ∈ (Unit‘𝑅) ∧ (Unit‘𝑅) ⊆ (Base‘(mulGrp‘𝑅))) →
(0g‘(mulGrp‘𝑅)) = (0g‘𝐺)) |
| 156 | 110, 152,
153, 155 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) →
(0g‘(mulGrp‘𝑅)) = (0g‘𝐺)) |
| 157 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → ((od‘𝐺)‘𝑚) = 𝐷) |
| 158 | 157 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 𝐷 = ((od‘𝐺)‘𝑚)) |
| 159 | 158 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (𝐷(.g‘𝐺)𝑚) = (((od‘𝐺)‘𝑚)(.g‘𝐺)𝑚)) |
| 160 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(od‘𝐺) =
(od‘𝐺) |
| 161 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 162 | 3, 160, 4, 161 | odid 19556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ (Base‘𝐺) → (((od‘𝐺)‘𝑚)(.g‘𝐺)𝑚) = (0g‘𝐺)) |
| 163 | 162 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (((od‘𝐺)‘𝑚)(.g‘𝐺)𝑚) = (0g‘𝐺)) |
| 164 | 159, 163 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (𝐷(.g‘𝐺)𝑚) = (0g‘𝐺)) |
| 165 | 164 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (0g‘𝐺) = (𝐷(.g‘𝐺)𝑚)) |
| 166 | 156, 165 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) →
(0g‘(mulGrp‘𝑅)) = (𝐷(.g‘𝐺)𝑚)) |
| 167 | 31 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) → 𝑚 ∈ (Unit‘𝑅)) |
| 168 | 167 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 𝑚 ∈ (Unit‘𝑅)) |
| 169 | 8, 153, 168, 103 | ressmulgnnd 19096 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (𝐷(.g‘𝐺)𝑚) = (𝐷(.g‘(mulGrp‘𝑅))𝑚)) |
| 170 | 166, 169 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (𝐷(.g‘(mulGrp‘𝑅))𝑚) = (0g‘(mulGrp‘𝑅))) |
| 171 | 144, 170 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)(+g‘(mulGrp‘𝑅))𝑚) = (0g‘(mulGrp‘𝑅))) |
| 172 | 145 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (1r‘𝑅) =
(0g‘(mulGrp‘𝑅))) |
| 173 | 172 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) →
(0g‘(mulGrp‘𝑅)) = (1r‘𝑅)) |
| 174 | 171, 173 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)(+g‘(mulGrp‘𝑅))𝑚) = (1r‘𝑅)) |
| 175 | 135, 174 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (((𝐷 −
1)(.g‘(mulGrp‘𝑅))𝑚)(.r‘𝑅)𝑚) = (1r‘𝑅)) |
| 176 | 128, 131,
175 | rspcedvd 3624 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → ∃𝑜 ∈ (Base‘𝑅)(𝑜(.r‘𝑅)𝑚) = (1r‘𝑅)) |
| 177 | 109, 176 | jca 511 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (𝑚 ∈ (Base‘𝑅) ∧ ∃𝑜 ∈ (Base‘𝑅)(𝑜(.r‘𝑅)𝑚) = (1r‘𝑅))) |
| 178 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
| 179 | 16, 178, 132 | dvdsr 20362 |
. . . . . . . . . . . 12
⊢ (𝑚(∥r‘𝑅)(1r‘𝑅) ↔ (𝑚 ∈ (Base‘𝑅) ∧ ∃𝑜 ∈ (Base‘𝑅)(𝑜(.r‘𝑅)𝑚) = (1r‘𝑅))) |
| 180 | 177, 179 | sylibr 234 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 𝑚(∥r‘𝑅)(1r‘𝑅)) |
| 181 | 99 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) → 𝑅 ∈ CRing) |
| 182 | 181 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 𝑅 ∈ CRing) |
| 183 | 7, 64, 178 | crngunit 20378 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → (𝑚 ∈ (Unit‘𝑅) ↔ 𝑚(∥r‘𝑅)(1r‘𝑅))) |
| 184 | 182, 183 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → (𝑚 ∈ (Unit‘𝑅) ↔ 𝑚(∥r‘𝑅)(1r‘𝑅))) |
| 185 | 180, 184 | mpbird 257 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 𝑚 ∈ (Unit‘𝑅)) |
| 186 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(od‘(mulGrp‘𝑅)) = (od‘(mulGrp‘𝑅)) |
| 187 | 8, 186, 160 | submod 19587 |
. . . . . . . . . 10
⊢
(((Unit‘𝑅)
∈ (SubMnd‘(mulGrp‘𝑅)) ∧ 𝑚 ∈ (Unit‘𝑅)) → ((od‘(mulGrp‘𝑅))‘𝑚) = ((od‘𝐺)‘𝑚)) |
| 188 | 108, 185,
187 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → ((od‘(mulGrp‘𝑅))‘𝑚) = ((od‘𝐺)‘𝑚)) |
| 189 | 188, 157 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → ((od‘(mulGrp‘𝑅))‘𝑚) = 𝐷) |
| 190 | 102, 103,
105, 189 | isprimroot2 42095 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (Base‘𝐺)) ∧ ((od‘𝐺)‘𝑚) = 𝐷) → 𝑚 ∈ ((mulGrp‘𝑅) PrimRoots 𝐷)) |
| 191 | 98, 190 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷}) ∧ (𝑚 ∈ (Base‘𝐺) ∧ ((od‘𝐺)‘𝑚) = 𝐷)) → 𝑚 ∈ ((mulGrp‘𝑅) PrimRoots 𝐷)) |
| 192 | 94, 191 | mpdan 687 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷}) → 𝑚 ∈ ((mulGrp‘𝑅) PrimRoots 𝐷)) |
| 193 | 192 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷} → 𝑚 ∈ ((mulGrp‘𝑅) PrimRoots 𝐷))) |
| 194 | 90, 193 | eximd 2216 |
. . 3
⊢ (𝜑 → (∃𝑚 𝑚 ∈ {𝑤 ∈ (Base‘𝐺) ∣ ((od‘𝐺)‘𝑤) = 𝐷} → ∃𝑚 𝑚 ∈ ((mulGrp‘𝑅) PrimRoots 𝐷))) |
| 195 | 89, 194 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑚 𝑚 ∈ ((mulGrp‘𝑅) PrimRoots 𝐷)) |
| 196 | | n0 4353 |
. 2
⊢
(((mulGrp‘𝑅)
PrimRoots 𝐷) ≠ ∅
↔ ∃𝑚 𝑚 ∈ ((mulGrp‘𝑅) PrimRoots 𝐷)) |
| 197 | 195, 196 | sylibr 234 |
1
⊢ (𝜑 → ((mulGrp‘𝑅) PrimRoots 𝐷) ≠ ∅) |