| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | zndvdchrrhm.6 | . . . 4
⊢ 𝐹 = (𝑥 ∈ (Base‘𝑍) ↦ ∪
((ℤRHom‘𝑅)
“ 𝑥)) | 
| 2 |  | zndvdchrrhm.2 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 3 | 2 | nnnn0d 12587 | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 4 |  | eqid 2737 | . . . . . . . 8
⊢
(RSpan‘ℤring) =
(RSpan‘ℤring) | 
| 5 |  | eqid 2737 | . . . . . . . 8
⊢
(ℤring /s (ℤring
~QG ((RSpan‘ℤring)‘{𝑁}))) = (ℤring
/s (ℤring ~QG
((RSpan‘ℤring)‘{𝑁}))) | 
| 6 |  | zndvdchrrhm.5 | . . . . . . . 8
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) | 
| 7 | 4, 5, 6 | znbas2 21555 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (Base‘(ℤring /s
(ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) = (Base‘𝑍)) | 
| 8 | 3, 7 | syl 17 | . . . . . 6
⊢ (𝜑 →
(Base‘(ℤring /s
(ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) = (Base‘𝑍)) | 
| 9 | 8 | eqcomd 2743 | . . . . 5
⊢ (𝜑 → (Base‘𝑍) =
(Base‘(ℤring /s
(ℤring ~QG
((RSpan‘ℤring)‘{𝑁}))))) | 
| 10 | 9 | mpteq1d 5237 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑍) ↦ ∪
((ℤRHom‘𝑅)
“ 𝑥)) = (𝑥 ∈
(Base‘(ℤring /s
(ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) ↦ ∪
((ℤRHom‘𝑅)
“ 𝑥))) | 
| 11 | 1, 10 | eqtrid 2789 | . . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (Base‘(ℤring
/s (ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) ↦ ∪
((ℤRHom‘𝑅)
“ 𝑥))) | 
| 12 |  | eqid 2737 | . . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 13 |  | zndvdchrrhm.1 | . . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 14 |  | eqid 2737 | . . . . . 6
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) | 
| 15 | 14 | zrhrhm 21522 | . . . . 5
⊢ (𝑅 ∈ Ring →
(ℤRHom‘𝑅)
∈ (ℤring RingHom 𝑅)) | 
| 16 | 13, 15 | syl 17 | . . . 4
⊢ (𝜑 → (ℤRHom‘𝑅) ∈ (ℤring
RingHom 𝑅)) | 
| 17 |  | eqid 2737 | . . . 4
⊢ (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)}) = (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)}) | 
| 18 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑦∪ ((ℤRHom‘𝑅) “ 𝑥) | 
| 19 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑥∪ ((ℤRHom‘𝑅) “ 𝑦) | 
| 20 |  | imaeq2 6074 | . . . . . 6
⊢ (𝑥 = 𝑦 → ((ℤRHom‘𝑅) “ 𝑥) = ((ℤRHom‘𝑅) “ 𝑦)) | 
| 21 | 20 | unieqd 4920 | . . . . 5
⊢ (𝑥 = 𝑦 → ∪
((ℤRHom‘𝑅)
“ 𝑥) = ∪ ((ℤRHom‘𝑅) “ 𝑦)) | 
| 22 | 18, 19, 21 | cbvmpt 5253 | . . . 4
⊢ (𝑥 ∈
(Base‘(ℤring /s
(ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) ↦ ∪
((ℤRHom‘𝑅)
“ 𝑥)) = (𝑦 ∈
(Base‘(ℤring /s
(ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) ↦ ∪
((ℤRHom‘𝑅)
“ 𝑦)) | 
| 23 |  | zringcrng 21459 | . . . . 5
⊢
ℤring ∈ CRing | 
| 24 | 23 | a1i 11 | . . . 4
⊢ (𝜑 → ℤring
∈ CRing) | 
| 25 |  | zringring 21460 | . . . . . 6
⊢
ℤring ∈ Ring | 
| 26 | 25 | a1i 11 | . . . . 5
⊢ (𝜑 → ℤring
∈ Ring) | 
| 27 |  | eqid 2737 | . . . . . . 7
⊢
(LIdeal‘ℤring) =
(LIdeal‘ℤring) | 
| 28 | 27, 12 | kerlidl 21288 | . . . . . 6
⊢
((ℤRHom‘𝑅) ∈ (ℤring RingHom
𝑅) → (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)}) ∈
(LIdeal‘ℤring)) | 
| 29 | 16, 28 | syl 17 | . . . . 5
⊢ (𝜑 → (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)}) ∈
(LIdeal‘ℤring)) | 
| 30 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑁}) → 𝑎 ∈ {𝑁}) | 
| 31 |  | elsng 4640 | . . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑁} → (𝑎 ∈ {𝑁} ↔ 𝑎 = 𝑁)) | 
| 32 | 30, 31 | syl5ibcom 245 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑁}) → (𝑎 ∈ {𝑁} → 𝑎 = 𝑁)) | 
| 33 | 32 | imp 406 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ {𝑁}) ∧ 𝑎 ∈ {𝑁}) → 𝑎 = 𝑁) | 
| 34 | 30, 33 | mpdan 687 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑁}) → 𝑎 = 𝑁) | 
| 35 |  | zringbas 21464 | . . . . . . . . . . . . . 14
⊢ ℤ =
(Base‘ℤring) | 
| 36 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 37 | 35, 36 | rhmf 20485 | . . . . . . . . . . . . 13
⊢
((ℤRHom‘𝑅) ∈ (ℤring RingHom
𝑅) →
(ℤRHom‘𝑅):ℤ⟶(Base‘𝑅)) | 
| 38 | 15, 37 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
(ℤRHom‘𝑅):ℤ⟶(Base‘𝑅)) | 
| 39 | 13, 38 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (ℤRHom‘𝑅):ℤ⟶(Base‘𝑅)) | 
| 40 | 39 | ffnd 6737 | . . . . . . . . . 10
⊢ (𝜑 → (ℤRHom‘𝑅) Fn ℤ) | 
| 41 | 2 | nnzd 12640 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 42 |  | zndvdchrrhm.4 | . . . . . . . . . . . 12
⊢ (𝜑 → (chr‘𝑅) ∥ 𝑁) | 
| 43 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(chr‘𝑅) =
(chr‘𝑅) | 
| 44 | 43, 14, 12 | chrdvds 21541 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) →
((chr‘𝑅) ∥
𝑁 ↔
((ℤRHom‘𝑅)‘𝑁) = (0g‘𝑅))) | 
| 45 | 13, 41, 44 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → ((chr‘𝑅) ∥ 𝑁 ↔ ((ℤRHom‘𝑅)‘𝑁) = (0g‘𝑅))) | 
| 46 | 42, 45 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 → ((ℤRHom‘𝑅)‘𝑁) = (0g‘𝑅)) | 
| 47 |  | fvexd 6921 | . . . . . . . . . . . 12
⊢ (𝜑 → ((ℤRHom‘𝑅)‘𝑁) ∈ V) | 
| 48 |  | elsng 4640 | . . . . . . . . . . . 12
⊢
(((ℤRHom‘𝑅)‘𝑁) ∈ V → (((ℤRHom‘𝑅)‘𝑁) ∈ {(0g‘𝑅)} ↔
((ℤRHom‘𝑅)‘𝑁) = (0g‘𝑅))) | 
| 49 | 47, 48 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (((ℤRHom‘𝑅)‘𝑁) ∈ {(0g‘𝑅)} ↔
((ℤRHom‘𝑅)‘𝑁) = (0g‘𝑅))) | 
| 50 | 46, 49 | mpbird 257 | . . . . . . . . . 10
⊢ (𝜑 → ((ℤRHom‘𝑅)‘𝑁) ∈ {(0g‘𝑅)}) | 
| 51 | 40, 41, 50 | elpreimad 7079 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)})) | 
| 52 | 51 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑁}) → 𝑁 ∈ (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)})) | 
| 53 | 34, 52 | eqeltrd 2841 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑁}) → 𝑎 ∈ (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)})) | 
| 54 | 53 | ex 412 | . . . . . 6
⊢ (𝜑 → (𝑎 ∈ {𝑁} → 𝑎 ∈ (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)}))) | 
| 55 | 54 | ssrdv 3989 | . . . . 5
⊢ (𝜑 → {𝑁} ⊆ (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)})) | 
| 56 | 4, 27 | rspssp 21249 | . . . . 5
⊢
((ℤring ∈ Ring ∧ (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)}) ∈
(LIdeal‘ℤring) ∧ {𝑁} ⊆ (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)})) →
((RSpan‘ℤring)‘{𝑁}) ⊆ (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)})) | 
| 57 | 26, 29, 55, 56 | syl3anc 1373 | . . . 4
⊢ (𝜑 →
((RSpan‘ℤring)‘{𝑁}) ⊆ (◡(ℤRHom‘𝑅) “ {(0g‘𝑅)})) | 
| 58 | 24 | crngringd 20243 | . . . . 5
⊢ (𝜑 → ℤring
∈ Ring) | 
| 59 | 41 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑁}) → 𝑁 ∈ ℤ) | 
| 60 | 34, 59 | eqeltrd 2841 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑁}) → 𝑎 ∈ ℤ) | 
| 61 | 60 | ex 412 | . . . . . 6
⊢ (𝜑 → (𝑎 ∈ {𝑁} → 𝑎 ∈ ℤ)) | 
| 62 | 61 | ssrdv 3989 | . . . . 5
⊢ (𝜑 → {𝑁} ⊆ ℤ) | 
| 63 | 4, 35, 27 | rspcl 21245 | . . . . 5
⊢
((ℤring ∈ Ring ∧ {𝑁} ⊆ ℤ) →
((RSpan‘ℤring)‘{𝑁}) ∈
(LIdeal‘ℤring)) | 
| 64 | 58, 62, 63 | syl2anc 584 | . . . 4
⊢ (𝜑 →
((RSpan‘ℤring)‘{𝑁}) ∈
(LIdeal‘ℤring)) | 
| 65 | 12, 16, 17, 5, 22, 24, 57, 64 | rhmqusnsg 21295 | . . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘(ℤring
/s (ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) ↦ ∪
((ℤRHom‘𝑅)
“ 𝑥)) ∈
((ℤring /s (ℤring
~QG ((RSpan‘ℤring)‘{𝑁}))) RingHom 𝑅)) | 
| 66 | 11, 65 | eqeltrd 2841 | . 2
⊢ (𝜑 → 𝐹 ∈ ((ℤring
/s (ℤring ~QG
((RSpan‘ℤring)‘{𝑁}))) RingHom 𝑅)) | 
| 67 |  | eqidd 2738 | . . 3
⊢ (𝜑 →
(Base‘(ℤring /s
(ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) = (Base‘(ℤring
/s (ℤring ~QG
((RSpan‘ℤring)‘{𝑁}))))) | 
| 68 |  | eqidd 2738 | . . 3
⊢ (𝜑 → (Base‘𝑅) = (Base‘𝑅)) | 
| 69 | 4, 5, 6 | znadd 21557 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (+g‘(ℤring /s
(ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) = (+g‘𝑍)) | 
| 70 | 3, 69 | syl 17 | . . . 4
⊢ (𝜑 →
(+g‘(ℤring /s
(ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) = (+g‘𝑍)) | 
| 71 | 70 | oveqdr 7459 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘(ℤring
/s (ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) ∧ 𝑏 ∈ (Base‘(ℤring
/s (ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))))) → (𝑎(+g‘(ℤring
/s (ℤring ~QG
((RSpan‘ℤring)‘{𝑁}))))𝑏) = (𝑎(+g‘𝑍)𝑏)) | 
| 72 |  | eqidd 2738 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎(+g‘𝑅)𝑏) = (𝑎(+g‘𝑅)𝑏)) | 
| 73 | 4, 5, 6 | znmul 21559 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (.r‘(ℤring /s
(ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) = (.r‘𝑍)) | 
| 74 | 3, 73 | syl 17 | . . . 4
⊢ (𝜑 →
(.r‘(ℤring /s
(ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) = (.r‘𝑍)) | 
| 75 | 74 | oveqdr 7459 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘(ℤring
/s (ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))) ∧ 𝑏 ∈ (Base‘(ℤring
/s (ℤring ~QG
((RSpan‘ℤring)‘{𝑁})))))) → (𝑎(.r‘(ℤring
/s (ℤring ~QG
((RSpan‘ℤring)‘{𝑁}))))𝑏) = (𝑎(.r‘𝑍)𝑏)) | 
| 76 |  | eqidd 2738 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎(.r‘𝑅)𝑏) = (𝑎(.r‘𝑅)𝑏)) | 
| 77 | 67, 68, 8, 68, 71, 72, 75, 76 | rhmpropd 20609 | . 2
⊢ (𝜑 → ((ℤring
/s (ℤring ~QG
((RSpan‘ℤring)‘{𝑁}))) RingHom 𝑅) = (𝑍 RingHom 𝑅)) | 
| 78 | 66, 77 | eleqtrd 2843 | 1
⊢ (𝜑 → 𝐹 ∈ (𝑍 RingHom 𝑅)) |