| Step | Hyp | Ref
| Expression |
| 1 | | eqcom 2744 |
. 2
⊢ ((𝐿‘𝐴) = (𝐿‘𝐵) ↔ (𝐿‘𝐵) = (𝐿‘𝐴)) |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(RSpan‘ℤring) =
(RSpan‘ℤring) |
| 3 | | eqid 2737 |
. . . . . 6
⊢
(ℤring ~QG
((RSpan‘ℤring)‘{𝑁})) = (ℤring
~QG ((RSpan‘ℤring)‘{𝑁})) |
| 4 | | zncyg.y |
. . . . . 6
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
| 5 | | zndvds.2 |
. . . . . 6
⊢ 𝐿 = (ℤRHom‘𝑌) |
| 6 | 2, 3, 4, 5 | znzrhval 21565 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵 ∈ ℤ)
→ (𝐿‘𝐵) = [𝐵](ℤring
~QG ((RSpan‘ℤring)‘{𝑁}))) |
| 7 | 6 | 3adant2 1132 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (𝐿‘𝐵) = [𝐵](ℤring
~QG ((RSpan‘ℤring)‘{𝑁}))) |
| 8 | 2, 3, 4, 5 | znzrhval 21565 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (𝐿‘𝐴) = [𝐴](ℤring
~QG ((RSpan‘ℤring)‘{𝑁}))) |
| 9 | 8 | 3adant3 1133 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (𝐿‘𝐴) = [𝐴](ℤring
~QG ((RSpan‘ℤring)‘{𝑁}))) |
| 10 | 7, 9 | eqeq12d 2753 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((𝐿‘𝐵) = (𝐿‘𝐴) ↔ [𝐵](ℤring
~QG ((RSpan‘ℤring)‘{𝑁})) = [𝐴](ℤring
~QG ((RSpan‘ℤring)‘{𝑁})))) |
| 11 | | zringring 21460 |
. . . . . 6
⊢
ℤring ∈ Ring |
| 12 | | nn0z 12638 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 13 | 12 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ 𝑁 ∈
ℤ) |
| 14 | 13 | snssd 4809 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ {𝑁} ⊆
ℤ) |
| 15 | | zringbas 21464 |
. . . . . . . 8
⊢ ℤ =
(Base‘ℤring) |
| 16 | | eqid 2737 |
. . . . . . . 8
⊢
(LIdeal‘ℤring) =
(LIdeal‘ℤring) |
| 17 | 2, 15, 16 | rspcl 21245 |
. . . . . . 7
⊢
((ℤring ∈ Ring ∧ {𝑁} ⊆ ℤ) →
((RSpan‘ℤring)‘{𝑁}) ∈
(LIdeal‘ℤring)) |
| 18 | 11, 14, 17 | sylancr 587 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((RSpan‘ℤring)‘{𝑁}) ∈
(LIdeal‘ℤring)) |
| 19 | 16 | lidlsubg 21233 |
. . . . . 6
⊢
((ℤring ∈ Ring ∧
((RSpan‘ℤring)‘{𝑁}) ∈
(LIdeal‘ℤring)) →
((RSpan‘ℤring)‘{𝑁}) ∈
(SubGrp‘ℤring)) |
| 20 | 11, 18, 19 | sylancr 587 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((RSpan‘ℤring)‘{𝑁}) ∈
(SubGrp‘ℤring)) |
| 21 | 15, 3 | eqger 19196 |
. . . . 5
⊢
(((RSpan‘ℤring)‘{𝑁}) ∈
(SubGrp‘ℤring) → (ℤring
~QG ((RSpan‘ℤring)‘{𝑁})) Er ℤ) |
| 22 | 20, 21 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (ℤring ~QG
((RSpan‘ℤring)‘{𝑁})) Er ℤ) |
| 23 | | simp3 1139 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ 𝐵 ∈
ℤ) |
| 24 | 22, 23 | erth 8796 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (𝐵(ℤring
~QG ((RSpan‘ℤring)‘{𝑁}))𝐴 ↔ [𝐵](ℤring
~QG ((RSpan‘ℤring)‘{𝑁})) = [𝐴](ℤring
~QG ((RSpan‘ℤring)‘{𝑁})))) |
| 25 | | zringabl 21462 |
. . . . 5
⊢
ℤring ∈ Abel |
| 26 | 15, 16 | lidlss 21222 |
. . . . . 6
⊢
(((RSpan‘ℤring)‘{𝑁}) ∈
(LIdeal‘ℤring) →
((RSpan‘ℤring)‘{𝑁}) ⊆ ℤ) |
| 27 | 18, 26 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((RSpan‘ℤring)‘{𝑁}) ⊆ ℤ) |
| 28 | | eqid 2737 |
. . . . . 6
⊢
(-g‘ℤring) =
(-g‘ℤring) |
| 29 | 15, 28, 3 | eqgabl 19852 |
. . . . 5
⊢
((ℤring ∈ Abel ∧
((RSpan‘ℤring)‘{𝑁}) ⊆ ℤ) → (𝐵(ℤring
~QG ((RSpan‘ℤring)‘{𝑁}))𝐴 ↔ (𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝐴(-g‘ℤring)𝐵) ∈
((RSpan‘ℤring)‘{𝑁})))) |
| 30 | 25, 27, 29 | sylancr 587 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (𝐵(ℤring
~QG ((RSpan‘ℤring)‘{𝑁}))𝐴 ↔ (𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝐴(-g‘ℤring)𝐵) ∈
((RSpan‘ℤring)‘{𝑁})))) |
| 31 | | simp2 1138 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ 𝐴 ∈
ℤ) |
| 32 | 23, 31 | jca 511 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (𝐵 ∈ ℤ
∧ 𝐴 ∈
ℤ)) |
| 33 | 32 | biantrurd 532 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((𝐴(-g‘ℤring)𝐵) ∈
((RSpan‘ℤring)‘{𝑁}) ↔ ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ (𝐴(-g‘ℤring)𝐵) ∈
((RSpan‘ℤring)‘{𝑁})))) |
| 34 | | df-3an 1089 |
. . . . 5
⊢ ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝐴(-g‘ℤring)𝐵) ∈
((RSpan‘ℤring)‘{𝑁})) ↔ ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ (𝐴(-g‘ℤring)𝐵) ∈
((RSpan‘ℤring)‘{𝑁}))) |
| 35 | 33, 34 | bitr4di 289 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((𝐴(-g‘ℤring)𝐵) ∈
((RSpan‘ℤring)‘{𝑁}) ↔ (𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝐴(-g‘ℤring)𝐵) ∈
((RSpan‘ℤring)‘{𝑁})))) |
| 36 | | zsubrg 21438 |
. . . . . . . . 9
⊢ ℤ
∈ (SubRing‘ℂfld) |
| 37 | | subrgsubg 20577 |
. . . . . . . . 9
⊢ (ℤ
∈ (SubRing‘ℂfld) → ℤ ∈
(SubGrp‘ℂfld)) |
| 38 | 36, 37 | mp1i 13 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ℤ ∈ (SubGrp‘ℂfld)) |
| 39 | | cnfldsub 21410 |
. . . . . . . . 9
⊢ −
= (-g‘ℂfld) |
| 40 | | df-zring 21458 |
. . . . . . . . 9
⊢
ℤring = (ℂfld ↾s
ℤ) |
| 41 | 39, 40, 28 | subgsub 19156 |
. . . . . . . 8
⊢ ((ℤ
∈ (SubGrp‘ℂfld) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) = (𝐴(-g‘ℤring)𝐵)) |
| 42 | 38, 41 | syld3an1 1412 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (𝐴 − 𝐵) = (𝐴(-g‘ℤring)𝐵)) |
| 43 | 42 | eqcomd 2743 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (𝐴(-g‘ℤring)𝐵) = (𝐴 − 𝐵)) |
| 44 | | dvdsrzring 21472 |
. . . . . . . 8
⊢ ∥
= (∥r‘ℤring) |
| 45 | 15, 2, 44 | rspsn 21343 |
. . . . . . 7
⊢
((ℤring ∈ Ring ∧ 𝑁 ∈ ℤ) →
((RSpan‘ℤring)‘{𝑁}) = {𝑥 ∣ 𝑁 ∥ 𝑥}) |
| 46 | 11, 13, 45 | sylancr 587 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((RSpan‘ℤring)‘{𝑁}) = {𝑥 ∣ 𝑁 ∥ 𝑥}) |
| 47 | 43, 46 | eleq12d 2835 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((𝐴(-g‘ℤring)𝐵) ∈
((RSpan‘ℤring)‘{𝑁}) ↔ (𝐴 − 𝐵) ∈ {𝑥 ∣ 𝑁 ∥ 𝑥})) |
| 48 | | ovex 7464 |
. . . . . 6
⊢ (𝐴 − 𝐵) ∈ V |
| 49 | | breq2 5147 |
. . . . . 6
⊢ (𝑥 = (𝐴 − 𝐵) → (𝑁 ∥ 𝑥 ↔ 𝑁 ∥ (𝐴 − 𝐵))) |
| 50 | 48, 49 | elab 3679 |
. . . . 5
⊢ ((𝐴 − 𝐵) ∈ {𝑥 ∣ 𝑁 ∥ 𝑥} ↔ 𝑁 ∥ (𝐴 − 𝐵)) |
| 51 | 47, 50 | bitrdi 287 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((𝐴(-g‘ℤring)𝐵) ∈
((RSpan‘ℤring)‘{𝑁}) ↔ 𝑁 ∥ (𝐴 − 𝐵))) |
| 52 | 30, 35, 51 | 3bitr2d 307 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (𝐵(ℤring
~QG ((RSpan‘ℤring)‘{𝑁}))𝐴 ↔ 𝑁 ∥ (𝐴 − 𝐵))) |
| 53 | 10, 24, 52 | 3bitr2d 307 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((𝐿‘𝐵) = (𝐿‘𝐴) ↔ 𝑁 ∥ (𝐴 − 𝐵))) |
| 54 | 1, 53 | bitrid 283 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ ((𝐿‘𝐴) = (𝐿‘𝐵) ↔ 𝑁 ∥ (𝐴 − 𝐵))) |