| Step | Hyp | Ref
| Expression |
| 1 | | df-qs 8751 |
. 2
⊢ ((ℤ
× ℤ) / ∼ ) = {𝑒 ∣ ∃𝑝 ∈ (ℤ ×
ℤ)𝑒 = [𝑝] ∼ } |
| 2 | | pzriprng.g |
. . 3
⊢ ∼ =
(𝑅 ~QG
𝐼) |
| 3 | | pzriprng.q |
. . . . 5
⊢ 𝑄 = (𝑅 /s ∼ ) |
| 4 | 3 | a1i 11 |
. . . 4
⊢ ( ∼ =
(𝑅 ~QG
𝐼) → 𝑄 = (𝑅 /s ∼ )) |
| 5 | | pzriprng.r |
. . . . . . 7
⊢ 𝑅 = (ℤring
×s ℤring) |
| 6 | 5 | pzriprnglem2 21493 |
. . . . . 6
⊢
(Base‘𝑅) =
(ℤ × ℤ) |
| 7 | 6 | eqcomi 2746 |
. . . . 5
⊢ (ℤ
× ℤ) = (Base‘𝑅) |
| 8 | 7 | a1i 11 |
. . . 4
⊢ ( ∼ =
(𝑅 ~QG
𝐼) → (ℤ ×
ℤ) = (Base‘𝑅)) |
| 9 | | ovexd 7466 |
. . . . 5
⊢ ( ∼ =
(𝑅 ~QG
𝐼) → (𝑅 ~QG 𝐼) ∈ V) |
| 10 | 2, 9 | eqeltrid 2845 |
. . . 4
⊢ ( ∼ =
(𝑅 ~QG
𝐼) → ∼ ∈
V) |
| 11 | 5 | pzriprnglem1 21492 |
. . . . 5
⊢ 𝑅 ∈ Rng |
| 12 | 11 | a1i 11 |
. . . 4
⊢ ( ∼ =
(𝑅 ~QG
𝐼) → 𝑅 ∈ Rng) |
| 13 | 4, 8, 10, 12 | qusbas 17590 |
. . 3
⊢ ( ∼ =
(𝑅 ~QG
𝐼) → ((ℤ ×
ℤ) / ∼ ) =
(Base‘𝑄)) |
| 14 | 2, 13 | ax-mp 5 |
. 2
⊢ ((ℤ
× ℤ) / ∼ ) =
(Base‘𝑄) |
| 15 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑠{𝑒 ∣ 𝑒 = [𝑝] ∼ } |
| 16 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑟{𝑒 ∣ 𝑒 = [𝑝] ∼ } |
| 17 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑝{𝑒 ∣ 𝑒 = [〈𝑠, 𝑟〉] ∼ } |
| 18 | | eceq1 8784 |
. . . . . 6
⊢ (𝑝 = 〈𝑠, 𝑟〉 → [𝑝] ∼ = [〈𝑠, 𝑟〉] ∼ ) |
| 19 | 18 | eqeq2d 2748 |
. . . . 5
⊢ (𝑝 = 〈𝑠, 𝑟〉 → (𝑒 = [𝑝] ∼ ↔ 𝑒 = [〈𝑠, 𝑟〉] ∼ )) |
| 20 | 19 | abbidv 2808 |
. . . 4
⊢ (𝑝 = 〈𝑠, 𝑟〉 → {𝑒 ∣ 𝑒 = [𝑝] ∼ } = {𝑒 ∣ 𝑒 = [〈𝑠, 𝑟〉] ∼ }) |
| 21 | 15, 16, 17, 20 | iunxpf 5859 |
. . 3
⊢ ∪ 𝑝 ∈ (ℤ × ℤ){𝑒 ∣ 𝑒 = [𝑝] ∼ } = ∪ 𝑠 ∈ ℤ ∪ 𝑟 ∈ ℤ {𝑒 ∣ 𝑒 = [〈𝑠, 𝑟〉] ∼ } |
| 22 | | iunab 5051 |
. . 3
⊢ ∪ 𝑝 ∈ (ℤ × ℤ){𝑒 ∣ 𝑒 = [𝑝] ∼ } = {𝑒 ∣ ∃𝑝 ∈ (ℤ ×
ℤ)𝑒 = [𝑝] ∼ } |
| 23 | | iuncom 4999 |
. . . 4
⊢ ∪ 𝑠 ∈ ℤ ∪ 𝑟 ∈ ℤ {𝑒 ∣ 𝑒 = [〈𝑠, 𝑟〉] ∼ } = ∪ 𝑟 ∈ ℤ ∪ 𝑠 ∈ ℤ {𝑒 ∣ 𝑒 = [〈𝑠, 𝑟〉] ∼ } |
| 24 | | df-sn 4627 |
. . . . . . . . 9
⊢
{[〈𝑠, 𝑟〉] ∼ } = {𝑒 ∣ 𝑒 = [〈𝑠, 𝑟〉] ∼ } |
| 25 | 24 | eqcomi 2746 |
. . . . . . . 8
⊢ {𝑒 ∣ 𝑒 = [〈𝑠, 𝑟〉] ∼ } = {[〈𝑠, 𝑟〉] ∼ } |
| 26 | 25 | a1i 11 |
. . . . . . 7
⊢ (𝑠 ∈ ℤ → {𝑒 ∣ 𝑒 = [〈𝑠, 𝑟〉] ∼ } = {[〈𝑠, 𝑟〉] ∼ }) |
| 27 | 26 | iuneq2i 5013 |
. . . . . 6
⊢ ∪ 𝑠 ∈ ℤ {𝑒 ∣ 𝑒 = [〈𝑠, 𝑟〉] ∼ } = ∪ 𝑠 ∈ ℤ {[〈𝑠, 𝑟〉] ∼ } |
| 28 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) ∧ 𝑝 = [〈𝑠, 𝑟〉] ∼ ) → 𝑝 = [〈𝑠, 𝑟〉] ∼ ) |
| 29 | | pzriprng.i |
. . . . . . . . . . . . . . 15
⊢ 𝐼 = (ℤ ×
{0}) |
| 30 | | pzriprng.j |
. . . . . . . . . . . . . . 15
⊢ 𝐽 = (𝑅 ↾s 𝐼) |
| 31 | | pzriprng.1 |
. . . . . . . . . . . . . . 15
⊢ 1 =
(1r‘𝐽) |
| 32 | 5, 29, 30, 31, 2 | pzriprnglem10 21501 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ ℤ ∧ 𝑟 ∈ ℤ) →
[〈𝑠, 𝑟〉] ∼ = (ℤ ×
{𝑟})) |
| 33 | 32 | ancoms 458 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) →
[〈𝑠, 𝑟〉] ∼ = (ℤ ×
{𝑟})) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) ∧ 𝑝 = [〈𝑠, 𝑟〉] ∼ ) →
[〈𝑠, 𝑟〉] ∼ = (ℤ ×
{𝑟})) |
| 35 | 28, 34 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) ∧ 𝑝 = [〈𝑠, 𝑟〉] ∼ ) → 𝑝 = (ℤ × {𝑟})) |
| 36 | 35 | ex 412 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑝 = [〈𝑠, 𝑟〉] ∼ → 𝑝 = (ℤ × {𝑟}))) |
| 37 | 36 | rexlimdva 3155 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℤ →
(∃𝑠 ∈ ℤ
𝑝 = [〈𝑠, 𝑟〉] ∼ → 𝑝 = (ℤ × {𝑟}))) |
| 38 | | 0zd 12625 |
. . . . . . . . . . 11
⊢ ((𝑟 ∈ ℤ ∧ 𝑝 = (ℤ × {𝑟})) → 0 ∈
ℤ) |
| 39 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ ℤ ∧ 𝑝 = (ℤ × {𝑟})) → 𝑝 = (ℤ × {𝑟})) |
| 40 | | opeq1 4873 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 0 → 〈𝑠, 𝑟〉 = 〈0, 𝑟〉) |
| 41 | 40 | eceq1d 8785 |
. . . . . . . . . . . 12
⊢ (𝑠 = 0 → [〈𝑠, 𝑟〉] ∼ = [〈0, 𝑟〉] ∼ ) |
| 42 | 39, 41 | eqeqan12d 2751 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ ℤ ∧ 𝑝 = (ℤ × {𝑟})) ∧ 𝑠 = 0) → (𝑝 = [〈𝑠, 𝑟〉] ∼ ↔ (ℤ
× {𝑟}) = [〈0,
𝑟〉] ∼ )) |
| 43 | | 0zd 12625 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ ℤ → 0 ∈
ℤ) |
| 44 | 5, 29, 30, 31, 2 | pzriprnglem10 21501 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℤ ∧ 𝑟
∈ ℤ) → [〈0, 𝑟〉] ∼ = (ℤ ×
{𝑟})) |
| 45 | 43, 44 | mpancom 688 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℤ → [〈0,
𝑟〉] ∼ = (ℤ ×
{𝑟})) |
| 46 | 45 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℤ → (ℤ
× {𝑟}) = [〈0,
𝑟〉] ∼ ) |
| 47 | 46 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑟 ∈ ℤ ∧ 𝑝 = (ℤ × {𝑟})) → (ℤ ×
{𝑟}) = [〈0, 𝑟〉] ∼ ) |
| 48 | 38, 42, 47 | rspcedvd 3624 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ ℤ ∧ 𝑝 = (ℤ × {𝑟})) → ∃𝑠 ∈ ℤ 𝑝 = [〈𝑠, 𝑟〉] ∼ ) |
| 49 | 48 | ex 412 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℤ → (𝑝 = (ℤ × {𝑟}) → ∃𝑠 ∈ ℤ 𝑝 = [〈𝑠, 𝑟〉] ∼ )) |
| 50 | 37, 49 | impbid 212 |
. . . . . . . 8
⊢ (𝑟 ∈ ℤ →
(∃𝑠 ∈ ℤ
𝑝 = [〈𝑠, 𝑟〉] ∼ ↔ 𝑝 = (ℤ × {𝑟}))) |
| 51 | 50 | abbidv 2808 |
. . . . . . 7
⊢ (𝑟 ∈ ℤ → {𝑝 ∣ ∃𝑠 ∈ ℤ 𝑝 = [〈𝑠, 𝑟〉] ∼ } = {𝑝 ∣ 𝑝 = (ℤ × {𝑟})}) |
| 52 | | iunsn 5066 |
. . . . . . 7
⊢ ∪ 𝑠 ∈ ℤ {[〈𝑠, 𝑟〉] ∼ } = {𝑝 ∣ ∃𝑠 ∈ ℤ 𝑝 = [〈𝑠, 𝑟〉] ∼ } |
| 53 | | df-sn 4627 |
. . . . . . 7
⊢ {(ℤ
× {𝑟})} = {𝑝 ∣ 𝑝 = (ℤ × {𝑟})} |
| 54 | 51, 52, 53 | 3eqtr4g 2802 |
. . . . . 6
⊢ (𝑟 ∈ ℤ → ∪ 𝑠 ∈ ℤ {[〈𝑠, 𝑟〉] ∼ } = {(ℤ
× {𝑟})}) |
| 55 | 27, 54 | eqtrid 2789 |
. . . . 5
⊢ (𝑟 ∈ ℤ → ∪ 𝑠 ∈ ℤ {𝑒 ∣ 𝑒 = [〈𝑠, 𝑟〉] ∼ } = {(ℤ
× {𝑟})}) |
| 56 | 55 | iuneq2i 5013 |
. . . 4
⊢ ∪ 𝑟 ∈ ℤ ∪ 𝑠 ∈ ℤ {𝑒 ∣ 𝑒 = [〈𝑠, 𝑟〉] ∼ } = ∪ 𝑟 ∈ ℤ {(ℤ × {𝑟})} |
| 57 | 23, 56 | eqtri 2765 |
. . 3
⊢ ∪ 𝑠 ∈ ℤ ∪ 𝑟 ∈ ℤ {𝑒 ∣ 𝑒 = [〈𝑠, 𝑟〉] ∼ } = ∪ 𝑟 ∈ ℤ {(ℤ × {𝑟})} |
| 58 | 21, 22, 57 | 3eqtr3i 2773 |
. 2
⊢ {𝑒 ∣ ∃𝑝 ∈ (ℤ ×
ℤ)𝑒 = [𝑝] ∼ } = ∪ 𝑟 ∈ ℤ {(ℤ × {𝑟})} |
| 59 | 1, 14, 58 | 3eqtr3i 2773 |
1
⊢
(Base‘𝑄) =
∪ 𝑟 ∈ ℤ {(ℤ × {𝑟})} |