Step | Hyp | Ref
| Expression |
1 | | pzriprng.r |
. . 3
⊢ 𝑅 = (ℤring
×s ℤring) |
2 | | pzriprng.i |
. . 3
⊢ 𝐼 = (ℤ ×
{0}) |
3 | 1, 2 | pzriprnglem3 21403 |
. 2
⊢ (𝑋 ∈ 𝐼 ↔ ∃𝑎 ∈ ℤ 𝑋 = 〈𝑎, 0〉) |
4 | 1, 2 | pzriprnglem5 21405 |
. . . . . . . . 9
⊢ 𝐼 ∈ (SubRng‘𝑅) |
5 | | pzriprng.j |
. . . . . . . . . . 11
⊢ 𝐽 = (𝑅 ↾s 𝐼) |
6 | | eqid 2728 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
7 | 5, 6 | ressmulr 17282 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (SubRng‘𝑅) →
(.r‘𝑅) =
(.r‘𝐽)) |
8 | 7 | eqcomd 2734 |
. . . . . . . . 9
⊢ (𝐼 ∈ (SubRng‘𝑅) →
(.r‘𝐽) =
(.r‘𝑅)) |
9 | 4, 8 | ax-mp 5 |
. . . . . . . 8
⊢
(.r‘𝐽) = (.r‘𝑅) |
10 | 9 | oveqi 7428 |
. . . . . . 7
⊢ (〈1,
0〉(.r‘𝐽)〈𝑎, 0〉) = (〈1,
0〉(.r‘𝑅)〈𝑎, 0〉) |
11 | 10 | a1i 11 |
. . . . . 6
⊢ (𝑎 ∈ ℤ → (〈1,
0〉(.r‘𝐽)〈𝑎, 0〉) = (〈1,
0〉(.r‘𝑅)〈𝑎, 0〉)) |
12 | | zringbas 21373 |
. . . . . . 7
⊢ ℤ =
(Base‘ℤring) |
13 | | zringring 21369 |
. . . . . . . 8
⊢
ℤring ∈ Ring |
14 | 13 | a1i 11 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ →
ℤring ∈ Ring) |
15 | | 1zzd 12618 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → 1 ∈
ℤ) |
16 | | 0z 12594 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → 0 ∈
ℤ) |
18 | | id 22 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℤ) |
19 | | zringmulr 21377 |
. . . . . . . . 9
⊢ ·
= (.r‘ℤring) |
20 | 19 | oveqi 7428 |
. . . . . . . 8
⊢ (1
· 𝑎) =
(1(.r‘ℤring)𝑎) |
21 | 15, 18 | zmulcld 12697 |
. . . . . . . 8
⊢ (𝑎 ∈ ℤ → (1
· 𝑎) ∈
ℤ) |
22 | 20, 21 | eqeltrrid 2834 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ →
(1(.r‘ℤring)𝑎) ∈ ℤ) |
23 | 19 | eqcomi 2737 |
. . . . . . . . . 10
⊢
(.r‘ℤring) = · |
24 | 23 | oveqi 7428 |
. . . . . . . . 9
⊢
(0(.r‘ℤring)0) = (0 ·
0) |
25 | | id 22 |
. . . . . . . . . . 11
⊢ (0 ∈
ℤ → 0 ∈ ℤ) |
26 | 25, 25 | zmulcld 12697 |
. . . . . . . . . 10
⊢ (0 ∈
ℤ → (0 · 0) ∈ ℤ) |
27 | 16, 26 | ax-mp 5 |
. . . . . . . . 9
⊢ (0
· 0) ∈ ℤ |
28 | 24, 27 | eqeltri 2825 |
. . . . . . . 8
⊢
(0(.r‘ℤring)0) ∈
ℤ |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ →
(0(.r‘ℤring)0) ∈
ℤ) |
30 | | eqid 2728 |
. . . . . . 7
⊢
(.r‘ℤring) =
(.r‘ℤring) |
31 | 1, 12, 12, 14, 14, 15, 17, 18, 17, 22, 29, 30, 30, 6 | xpsmul 17551 |
. . . . . 6
⊢ (𝑎 ∈ ℤ → (〈1,
0〉(.r‘𝑅)〈𝑎, 0〉) =
〈(1(.r‘ℤring)𝑎),
(0(.r‘ℤring)0)〉) |
32 | | zcn 12588 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℂ) |
33 | 32 | mullidd 11257 |
. . . . . . . 8
⊢ (𝑎 ∈ ℤ → (1
· 𝑎) = 𝑎) |
34 | 20, 33 | eqtr3id 2782 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ →
(1(.r‘ℤring)𝑎) = 𝑎) |
35 | | 0cn 11231 |
. . . . . . . . . 10
⊢ 0 ∈
ℂ |
36 | 35 | mul02i 11428 |
. . . . . . . . 9
⊢ (0
· 0) = 0 |
37 | 24, 36 | eqtri 2756 |
. . . . . . . 8
⊢
(0(.r‘ℤring)0) = 0 |
38 | 37 | a1i 11 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ →
(0(.r‘ℤring)0) = 0) |
39 | 34, 38 | opeq12d 4878 |
. . . . . 6
⊢ (𝑎 ∈ ℤ →
〈(1(.r‘ℤring)𝑎),
(0(.r‘ℤring)0)〉 = 〈𝑎, 0〉) |
40 | 11, 31, 39 | 3eqtrd 2772 |
. . . . 5
⊢ (𝑎 ∈ ℤ → (〈1,
0〉(.r‘𝐽)〈𝑎, 0〉) = 〈𝑎, 0〉) |
41 | 9 | oveqi 7428 |
. . . . . . 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 7428 |
. . . . . . . 8
⊢ (𝑎 · 1) = (𝑎(.r‘ℤring)1) |
44 | 18, 15 | zmulcld 12697 |
. . . . . . . 8
⊢ (𝑎 ∈ ℤ → (𝑎 · 1) ∈
ℤ) |
45 | 43, 44 | eqeltrrid 2834 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → (𝑎(.r‘ℤring)1)
∈ ℤ) |
46 | 1, 12, 12, 14, 14, 18, 17, 15, 17, 45, 29, 30, 30, 6 | xpsmul 17551 |
. . . . . 6
⊢ (𝑎 ∈ ℤ →
(〈𝑎,
0〉(.r‘𝑅)〈1, 0〉) = 〈(𝑎(.r‘ℤring)1),
(0(.r‘ℤring)0)〉) |
47 | 23 | oveqi 7428 |
. . . . . . . 8
⊢ (𝑎(.r‘ℤring)1)
= (𝑎 ·
1) |
48 | 32 | mulridd 11256 |
. . . . . . . 8
⊢ (𝑎 ∈ ℤ → (𝑎 · 1) = 𝑎) |
49 | 47, 48 | eqtrid 2780 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → (𝑎(.r‘ℤring)1)
= 𝑎) |
50 | 49, 38 | opeq12d 4878 |
. . . . . 6
⊢ (𝑎 ∈ ℤ →
〈(𝑎(.r‘ℤring)1),
(0(.r‘ℤring)0)〉 = 〈𝑎, 0〉) |
51 | 42, 46, 50 | 3eqtrd 2772 |
. . . . 5
⊢ (𝑎 ∈ ℤ →
(〈𝑎,
0〉(.r‘𝐽)〈1, 0〉) = 〈𝑎, 0〉) |
52 | 40, 51 | jca 511 |
. . . 4
⊢ (𝑎 ∈ ℤ →
((〈1, 0〉(.r‘𝐽)〈𝑎, 0〉) = 〈𝑎, 0〉 ∧ (〈𝑎, 0〉(.r‘𝐽)〈1, 0〉) = 〈𝑎, 0〉)) |
53 | | oveq2 7423 |
. . . . . 6
⊢ (𝑋 = 〈𝑎, 0〉 → (〈1,
0〉(.r‘𝐽)𝑋) = (〈1,
0〉(.r‘𝐽)〈𝑎, 0〉)) |
54 | | id 22 |
. . . . . 6
⊢ (𝑋 = 〈𝑎, 0〉 → 𝑋 = 〈𝑎, 0〉) |
55 | 53, 54 | eqeq12d 2744 |
. . . . 5
⊢ (𝑋 = 〈𝑎, 0〉 → ((〈1,
0〉(.r‘𝐽)𝑋) = 𝑋 ↔ (〈1,
0〉(.r‘𝐽)〈𝑎, 0〉) = 〈𝑎, 0〉)) |
56 | | oveq1 7422 |
. . . . . 6
⊢ (𝑋 = 〈𝑎, 0〉 → (𝑋(.r‘𝐽)〈1, 0〉) = (〈𝑎,
0〉(.r‘𝐽)〈1, 0〉)) |
57 | 56, 54 | eqeq12d 2744 |
. . . . 5
⊢ (𝑋 = 〈𝑎, 0〉 → ((𝑋(.r‘𝐽)〈1, 0〉) = 𝑋 ↔ (〈𝑎, 0〉(.r‘𝐽)〈1, 0〉) = 〈𝑎, 0〉)) |
58 | 55, 57 | anbi12d 631 |
. . . 4
⊢ (𝑋 = 〈𝑎, 0〉 → (((〈1,
0〉(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)〈1, 0〉) = 𝑋) ↔ ((〈1,
0〉(.r‘𝐽)〈𝑎, 0〉) = 〈𝑎, 0〉 ∧ (〈𝑎, 0〉(.r‘𝐽)〈1, 0〉) = 〈𝑎, 0〉))) |
59 | 52, 58 | syl5ibrcom 246 |
. . 3
⊢ (𝑎 ∈ ℤ → (𝑋 = 〈𝑎, 0〉 → ((〈1,
0〉(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)〈1, 0〉) = 𝑋))) |
60 | 59 | rexlimiv 3144 |
. 2
⊢
(∃𝑎 ∈
ℤ 𝑋 = 〈𝑎, 0〉 → ((〈1,
0〉(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)〈1, 0〉) = 𝑋)) |
61 | 3, 60 | sylbi 216 |
1
⊢ (𝑋 ∈ 𝐼 → ((〈1,
0〉(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)〈1, 0〉) = 𝑋)) |