Step | Hyp | Ref
| Expression |
1 | | znval.y |
. 2
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
2 | | zringring 19640 |
. . . . 5
⊢
ℤring ∈ Ring |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝑛 = 𝑁 → ℤring ∈
Ring) |
4 | | ovex 6577 |
. . . . . 6
⊢ (𝑧 /s (𝑧 ~QG
((RSpan‘𝑧)‘{𝑛}))) ∈ V |
5 | 4 | a1i 11 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑧 = ℤring) → (𝑧 /s (𝑧 ~QG
((RSpan‘𝑧)‘{𝑛}))) ∈ V) |
6 | | id 22 |
. . . . . . 7
⊢ (𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) → 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) |
7 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑧 = ℤring) → 𝑧 =
ℤring) |
8 | 7 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝑛 = 𝑁 ∧ 𝑧 = ℤring) →
(RSpan‘𝑧) =
(RSpan‘ℤring)) |
9 | | znval.s |
. . . . . . . . . . . 12
⊢ 𝑆 =
(RSpan‘ℤring) |
10 | 8, 9 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ ((𝑛 = 𝑁 ∧ 𝑧 = ℤring) →
(RSpan‘𝑧) = 𝑆) |
11 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑛 = 𝑁 ∧ 𝑧 = ℤring) → 𝑛 = 𝑁) |
12 | 11 | sneqd 4137 |
. . . . . . . . . . 11
⊢ ((𝑛 = 𝑁 ∧ 𝑧 = ℤring) → {𝑛} = {𝑁}) |
13 | 10, 12 | fveq12d 6109 |
. . . . . . . . . 10
⊢ ((𝑛 = 𝑁 ∧ 𝑧 = ℤring) →
((RSpan‘𝑧)‘{𝑛}) = (𝑆‘{𝑁})) |
14 | 7, 13 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑧 = ℤring) → (𝑧 ~QG
((RSpan‘𝑧)‘{𝑛})) = (ℤring
~QG (𝑆‘{𝑁}))) |
15 | 7, 14 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑧 = ℤring) → (𝑧 /s (𝑧 ~QG
((RSpan‘𝑧)‘{𝑛}))) = (ℤring
/s (ℤring ~QG (𝑆‘{𝑁})))) |
16 | | znval.u |
. . . . . . . 8
⊢ 𝑈 = (ℤring
/s (ℤring ~QG (𝑆‘{𝑁}))) |
17 | 15, 16 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑧 = ℤring) → (𝑧 /s (𝑧 ~QG
((RSpan‘𝑧)‘{𝑛}))) = 𝑈) |
18 | 6, 17 | sylan9eqr 2666 |
. . . . . 6
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) → 𝑠 = 𝑈) |
19 | | fvex 6113 |
. . . . . . . . . 10
⊢
(ℤRHom‘𝑠) ∈ V |
20 | 19 | resex 5363 |
. . . . . . . . 9
⊢
((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) ∈ V |
21 | 20 | a1i 11 |
. . . . . . . 8
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) → ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) ∈ V) |
22 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑓 = ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) → 𝑓 = ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))) |
23 | 18 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) → (ℤRHom‘𝑠) = (ℤRHom‘𝑈)) |
24 | | simpll 786 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) → 𝑛 = 𝑁) |
25 | 24 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) → (𝑛 = 0 ↔ 𝑁 = 0)) |
26 | 24 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) → (0..^𝑛) = (0..^𝑁)) |
27 | 25, 26 | ifbieq2d 4061 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) → if(𝑛 = 0, ℤ, (0..^𝑛)) = if(𝑁 = 0, ℤ, (0..^𝑁))) |
28 | | znval.w |
. . . . . . . . . . . . . . 15
⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) |
29 | 27, 28 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) → if(𝑛 = 0, ℤ, (0..^𝑛)) = 𝑊) |
30 | 23, 29 | reseq12d 5318 |
. . . . . . . . . . . . 13
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) → ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) = ((ℤRHom‘𝑈) ↾ 𝑊)) |
31 | | znval.f |
. . . . . . . . . . . . 13
⊢ 𝐹 = ((ℤRHom‘𝑈) ↾ 𝑊) |
32 | 30, 31 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) → ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) = 𝐹) |
33 | 22, 32 | sylan9eqr 2666 |
. . . . . . . . . . 11
⊢ ((((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) ∧ 𝑓 = ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))) → 𝑓 = 𝐹) |
34 | 33 | coeq1d 5205 |
. . . . . . . . . 10
⊢ ((((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) ∧ 𝑓 = ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))) → (𝑓 ∘ ≤ ) = (𝐹 ∘ ≤ )) |
35 | 33 | cnveqd 5220 |
. . . . . . . . . 10
⊢ ((((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) ∧ 𝑓 = ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))) → ◡𝑓 = ◡𝐹) |
36 | 34, 35 | coeq12d 5208 |
. . . . . . . . 9
⊢ ((((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) ∧ 𝑓 = ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))) → ((𝑓 ∘ ≤ ) ∘ ◡𝑓) = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) |
37 | | znval.l |
. . . . . . . . 9
⊢ ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹) |
38 | 36, 37 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) ∧ 𝑓 = ((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛)))) → ((𝑓 ∘ ≤ ) ∘ ◡𝑓) = ≤ ) |
39 | 21, 38 | csbied 3526 |
. . . . . . 7
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) →
⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓) = ≤ ) |
40 | 39 | opeq2d 4347 |
. . . . . 6
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) → 〈(le‘ndx),
⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉 = 〈(le‘ndx), ≤
〉) |
41 | 18, 40 | oveq12d 6567 |
. . . . 5
⊢ (((𝑛 = 𝑁 ∧ 𝑧 = ℤring) ∧ 𝑠 = (𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛})))) → (𝑠 sSet 〈(le‘ndx),
⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉) = (𝑈 sSet 〈(le‘ndx), ≤
〉)) |
42 | 5, 41 | csbied 3526 |
. . . 4
⊢ ((𝑛 = 𝑁 ∧ 𝑧 = ℤring) →
⦋(𝑧
/s (𝑧
~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet 〈(le‘ndx),
⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉) = (𝑈 sSet 〈(le‘ndx), ≤
〉)) |
43 | 3, 42 | csbied 3526 |
. . 3
⊢ (𝑛 = 𝑁 →
⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG
((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet 〈(le‘ndx),
⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉) = (𝑈 sSet 〈(le‘ndx), ≤
〉)) |
44 | | df-zn 19674 |
. . 3
⊢
ℤ/nℤ = (𝑛 ∈ ℕ0 ↦
⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG
((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet 〈(le‘ndx),
⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉)) |
45 | | ovex 6577 |
. . 3
⊢ (𝑈 sSet 〈(le‘ndx),
≤
〉) ∈ V |
46 | 43, 44, 45 | fvmpt 6191 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (ℤ/nℤ‘𝑁) = (𝑈 sSet 〈(le‘ndx), ≤
〉)) |
47 | 1, 46 | syl5eq 2656 |
1
⊢ (𝑁 ∈ ℕ0
→ 𝑌 = (𝑈 sSet 〈(le‘ndx),
≤
〉)) |