| Step | Hyp | Ref
| Expression |
| 1 | | pzriprng.r |
. . 3
⊢ 𝑅 = (ℤring
×s ℤring) |
| 2 | | pzriprng.i |
. . 3
⊢ 𝐼 = (ℤ ×
{0}) |
| 3 | 1, 2 | pzriprnglem3 21494 |
. 2
⊢ (𝑋 ∈ 𝐼 ↔ ∃𝑎 ∈ ℤ 𝑋 = 〈𝑎, 0〉) |
| 4 | 1, 2 | pzriprnglem5 21496 |
. . . . . . . . 9
⊢ 𝐼 ∈ (SubRng‘𝑅) |
| 5 | | pzriprng.j |
. . . . . . . . . . 11
⊢ 𝐽 = (𝑅 ↾s 𝐼) |
| 6 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 7 | 5, 6 | ressmulr 17351 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (SubRng‘𝑅) →
(.r‘𝑅) =
(.r‘𝐽)) |
| 8 | 7 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝐼 ∈ (SubRng‘𝑅) →
(.r‘𝐽) =
(.r‘𝑅)) |
| 9 | 4, 8 | ax-mp 5 |
. . . . . . . 8
⊢
(.r‘𝐽) = (.r‘𝑅) |
| 10 | 9 | oveqi 7444 |
. . . . . . 7
⊢ (〈1,
0〉(.r‘𝐽)〈𝑎, 0〉) = (〈1,
0〉(.r‘𝑅)〈𝑎, 0〉) |
| 11 | 10 | a1i 11 |
. . . . . 6
⊢ (𝑎 ∈ ℤ → (〈1,
0〉(.r‘𝐽)〈𝑎, 0〉) = (〈1,
0〉(.r‘𝑅)〈𝑎, 0〉)) |
| 12 | | zringbas 21464 |
. . . . . . 7
⊢ ℤ =
(Base‘ℤring) |
| 13 | | zringring 21460 |
. . . . . . . 8
⊢
ℤring ∈ Ring |
| 14 | 13 | a1i 11 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ →
ℤring ∈ Ring) |
| 15 | | 1zzd 12648 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → 1 ∈
ℤ) |
| 16 | | 0z 12624 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
| 17 | 16 | a1i 11 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → 0 ∈
ℤ) |
| 18 | | id 22 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℤ) |
| 19 | | zringmulr 21468 |
. . . . . . . . 9
⊢ ·
= (.r‘ℤring) |
| 20 | 19 | oveqi 7444 |
. . . . . . . 8
⊢ (1
· 𝑎) =
(1(.r‘ℤring)𝑎) |
| 21 | 15, 18 | zmulcld 12728 |
. . . . . . . 8
⊢ (𝑎 ∈ ℤ → (1
· 𝑎) ∈
ℤ) |
| 22 | 20, 21 | eqeltrrid 2846 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ →
(1(.r‘ℤring)𝑎) ∈ ℤ) |
| 23 | 19 | eqcomi 2746 |
. . . . . . . . . 10
⊢
(.r‘ℤring) = · |
| 24 | 23 | oveqi 7444 |
. . . . . . . . 9
⊢
(0(.r‘ℤring)0) = (0 ·
0) |
| 25 | | id 22 |
. . . . . . . . . . 11
⊢ (0 ∈
ℤ → 0 ∈ ℤ) |
| 26 | 25, 25 | zmulcld 12728 |
. . . . . . . . . 10
⊢ (0 ∈
ℤ → (0 · 0) ∈ ℤ) |
| 27 | 16, 26 | ax-mp 5 |
. . . . . . . . 9
⊢ (0
· 0) ∈ ℤ |
| 28 | 24, 27 | eqeltri 2837 |
. . . . . . . 8
⊢
(0(.r‘ℤring)0) ∈
ℤ |
| 29 | 28 | a1i 11 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ →
(0(.r‘ℤring)0) ∈
ℤ) |
| 30 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘ℤring) =
(.r‘ℤring) |
| 31 | 1, 12, 12, 14, 14, 15, 17, 18, 17, 22, 29, 30, 30, 6 | xpsmul 17620 |
. . . . . 6
⊢ (𝑎 ∈ ℤ → (〈1,
0〉(.r‘𝑅)〈𝑎, 0〉) =
〈(1(.r‘ℤring)𝑎),
(0(.r‘ℤring)0)〉) |
| 32 | | zcn 12618 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℂ) |
| 33 | 32 | mullidd 11279 |
. . . . . . . 8
⊢ (𝑎 ∈ ℤ → (1
· 𝑎) = 𝑎) |
| 34 | 20, 33 | eqtr3id 2791 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ →
(1(.r‘ℤring)𝑎) = 𝑎) |
| 35 | | 0cn 11253 |
. . . . . . . . . 10
⊢ 0 ∈
ℂ |
| 36 | 35 | mul02i 11450 |
. . . . . . . . 9
⊢ (0
· 0) = 0 |
| 37 | 24, 36 | eqtri 2765 |
. . . . . . . 8
⊢
(0(.r‘ℤring)0) = 0 |
| 38 | 37 | a1i 11 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ →
(0(.r‘ℤring)0) = 0) |
| 39 | 34, 38 | opeq12d 4881 |
. . . . . 6
⊢ (𝑎 ∈ ℤ →
〈(1(.r‘ℤring)𝑎),
(0(.r‘ℤring)0)〉 = 〈𝑎, 0〉) |
| 40 | 11, 31, 39 | 3eqtrd 2781 |
. . . . 5
⊢ (𝑎 ∈ ℤ → (〈1,
0〉(.r‘𝐽)〈𝑎, 0〉) = 〈𝑎, 0〉) |
| 41 | 9 | oveqi 7444 |
. . . . . . 7
⊢
(〈𝑎,
0〉(.r‘𝐽)〈1, 0〉) = (〈𝑎,
0〉(.r‘𝑅)〈1, 0〉) |
| 42 | 41 | a1i 11 |
. . . . . 6
⊢ (𝑎 ∈ ℤ →
(〈𝑎,
0〉(.r‘𝐽)〈1, 0〉) = (〈𝑎,
0〉(.r‘𝑅)〈1, 0〉)) |
| 43 | 19 | oveqi 7444 |
. . . . . . . 8
⊢ (𝑎 · 1) = (𝑎(.r‘ℤring)1) |
| 44 | 18, 15 | zmulcld 12728 |
. . . . . . . 8
⊢ (𝑎 ∈ ℤ → (𝑎 · 1) ∈
ℤ) |
| 45 | 43, 44 | eqeltrrid 2846 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → (𝑎(.r‘ℤring)1)
∈ ℤ) |
| 46 | 1, 12, 12, 14, 14, 18, 17, 15, 17, 45, 29, 30, 30, 6 | xpsmul 17620 |
. . . . . 6
⊢ (𝑎 ∈ ℤ →
(〈𝑎,
0〉(.r‘𝑅)〈1, 0〉) = 〈(𝑎(.r‘ℤring)1),
(0(.r‘ℤring)0)〉) |
| 47 | 23 | oveqi 7444 |
. . . . . . . 8
⊢ (𝑎(.r‘ℤring)1)
= (𝑎 ·
1) |
| 48 | 32 | mulridd 11278 |
. . . . . . . 8
⊢ (𝑎 ∈ ℤ → (𝑎 · 1) = 𝑎) |
| 49 | 47, 48 | eqtrid 2789 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → (𝑎(.r‘ℤring)1)
= 𝑎) |
| 50 | 49, 38 | opeq12d 4881 |
. . . . . 6
⊢ (𝑎 ∈ ℤ →
〈(𝑎(.r‘ℤring)1),
(0(.r‘ℤring)0)〉 = 〈𝑎, 0〉) |
| 51 | 42, 46, 50 | 3eqtrd 2781 |
. . . . 5
⊢ (𝑎 ∈ ℤ →
(〈𝑎,
0〉(.r‘𝐽)〈1, 0〉) = 〈𝑎, 0〉) |
| 52 | 40, 51 | jca 511 |
. . . 4
⊢ (𝑎 ∈ ℤ →
((〈1, 0〉(.r‘𝐽)〈𝑎, 0〉) = 〈𝑎, 0〉 ∧ (〈𝑎, 0〉(.r‘𝐽)〈1, 0〉) = 〈𝑎, 0〉)) |
| 53 | | oveq2 7439 |
. . . . . 6
⊢ (𝑋 = 〈𝑎, 0〉 → (〈1,
0〉(.r‘𝐽)𝑋) = (〈1,
0〉(.r‘𝐽)〈𝑎, 0〉)) |
| 54 | | id 22 |
. . . . . 6
⊢ (𝑋 = 〈𝑎, 0〉 → 𝑋 = 〈𝑎, 0〉) |
| 55 | 53, 54 | eqeq12d 2753 |
. . . . 5
⊢ (𝑋 = 〈𝑎, 0〉 → ((〈1,
0〉(.r‘𝐽)𝑋) = 𝑋 ↔ (〈1,
0〉(.r‘𝐽)〈𝑎, 0〉) = 〈𝑎, 0〉)) |
| 56 | | oveq1 7438 |
. . . . . 6
⊢ (𝑋 = 〈𝑎, 0〉 → (𝑋(.r‘𝐽)〈1, 0〉) = (〈𝑎,
0〉(.r‘𝐽)〈1, 0〉)) |
| 57 | 56, 54 | eqeq12d 2753 |
. . . . 5
⊢ (𝑋 = 〈𝑎, 0〉 → ((𝑋(.r‘𝐽)〈1, 0〉) = 𝑋 ↔ (〈𝑎, 0〉(.r‘𝐽)〈1, 0〉) = 〈𝑎, 0〉)) |
| 58 | 55, 57 | anbi12d 632 |
. . . 4
⊢ (𝑋 = 〈𝑎, 0〉 → (((〈1,
0〉(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)〈1, 0〉) = 𝑋) ↔ ((〈1,
0〉(.r‘𝐽)〈𝑎, 0〉) = 〈𝑎, 0〉 ∧ (〈𝑎, 0〉(.r‘𝐽)〈1, 0〉) = 〈𝑎, 0〉))) |
| 59 | 52, 58 | syl5ibrcom 247 |
. . 3
⊢ (𝑎 ∈ ℤ → (𝑋 = 〈𝑎, 0〉 → ((〈1,
0〉(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)〈1, 0〉) = 𝑋))) |
| 60 | 59 | rexlimiv 3148 |
. 2
⊢
(∃𝑎 ∈
ℤ 𝑋 = 〈𝑎, 0〉 → ((〈1,
0〉(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)〈1, 0〉) = 𝑋)) |
| 61 | 3, 60 | sylbi 217 |
1
⊢ (𝑋 ∈ 𝐼 → ((〈1,
0〉(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)〈1, 0〉) = 𝑋)) |