Proof of Theorem pzriprng1ALT
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢
(ℤring ×s
ℤring) = (ℤring ×s
ℤring) |
| 2 | 1 | pzriprnglem1 21492 |
. . . 4
⊢
(ℤring ×s
ℤring) ∈ Rng |
| 3 | | eqid 2737 |
. . . . 5
⊢ (ℤ
× {0}) = (ℤ × {0}) |
| 4 | | eqid 2737 |
. . . . 5
⊢
((ℤring ×s
ℤring) ↾s (ℤ × {0})) =
((ℤring ×s ℤring)
↾s (ℤ × {0})) |
| 5 | 1, 3, 4 | pzriprnglem8 21499 |
. . . 4
⊢ (ℤ
× {0}) ∈ (2Ideal‘(ℤring
×s ℤring)) |
| 6 | 2, 5 | pm3.2i 470 |
. . 3
⊢
((ℤring ×s
ℤring) ∈ Rng ∧ (ℤ × {0}) ∈
(2Ideal‘(ℤring ×s
ℤring))) |
| 7 | 1, 3, 4 | pzriprnglem7 21498 |
. . . 4
⊢
((ℤring ×s
ℤring) ↾s (ℤ × {0})) ∈
Ring |
| 8 | | eqid 2737 |
. . . . 5
⊢
(1r‘((ℤring ×s
ℤring) ↾s (ℤ × {0}))) =
(1r‘((ℤring ×s
ℤring) ↾s (ℤ ×
{0}))) |
| 9 | | eqid 2737 |
. . . . 5
⊢
((ℤring ×s
ℤring) ~QG (ℤ × {0})) =
((ℤring ×s ℤring)
~QG (ℤ × {0})) |
| 10 | | eqid 2737 |
. . . . 5
⊢
((ℤring ×s
ℤring) /s ((ℤring
×s ℤring) ~QG
(ℤ × {0}))) = ((ℤring ×s
ℤring) /s ((ℤring
×s ℤring) ~QG
(ℤ × {0}))) |
| 11 | 1, 3, 4, 8, 9, 10 | pzriprnglem13 21504 |
. . . 4
⊢
((ℤring ×s
ℤring) /s ((ℤring
×s ℤring) ~QG
(ℤ × {0}))) ∈ Ring |
| 12 | 7, 11 | pm3.2i 470 |
. . 3
⊢
(((ℤring ×s
ℤring) ↾s (ℤ × {0})) ∈ Ring
∧ ((ℤring ×s
ℤring) /s ((ℤring
×s ℤring) ~QG
(ℤ × {0}))) ∈ Ring) |
| 13 | | 1z 12647 |
. . . . 5
⊢ 1 ∈
ℤ |
| 14 | | 1ex 11257 |
. . . . . 6
⊢ 1 ∈
V |
| 15 | 14 | snid 4662 |
. . . . 5
⊢ 1 ∈
{1} |
| 16 | 13, 15 | opelxpii 5723 |
. . . 4
⊢ 〈1,
1〉 ∈ (ℤ × {1}) |
| 17 | 1, 3, 4, 8, 9, 10 | pzriprnglem14 21505 |
. . . 4
⊢
(1r‘((ℤring ×s
ℤring) /s ((ℤring
×s ℤring) ~QG
(ℤ × {0})))) = (ℤ × {1}) |
| 18 | 16, 17 | eleqtrri 2840 |
. . 3
⊢ 〈1,
1〉 ∈ (1r‘((ℤring
×s ℤring) /s
((ℤring ×s ℤring)
~QG (ℤ × {0})))) |
| 19 | | eqid 2737 |
. . . . 5
⊢
(.r‘(ℤring ×s
ℤring)) = (.r‘(ℤring
×s ℤring)) |
| 20 | | eqid 2737 |
. . . . 5
⊢
(-g‘(ℤring ×s
ℤring)) = (-g‘(ℤring
×s ℤring)) |
| 21 | | eqid 2737 |
. . . . 5
⊢
(+g‘(ℤring ×s
ℤring)) = (+g‘(ℤring
×s ℤring)) |
| 22 | 19, 8, 20, 21 | ring2idlqus1 21329 |
. . . 4
⊢
((((ℤring ×s
ℤring) ∈ Rng ∧ (ℤ × {0}) ∈
(2Ideal‘(ℤring ×s
ℤring))) ∧ (((ℤring
×s ℤring) ↾s (ℤ
× {0})) ∈ Ring ∧ ((ℤring
×s ℤring) /s
((ℤring ×s ℤring)
~QG (ℤ × {0}))) ∈ Ring) ∧ 〈1,
1〉 ∈ (1r‘((ℤring
×s ℤring) /s
((ℤring ×s ℤring)
~QG (ℤ × {0}))))) → ((ℤring
×s ℤring) ∈ Ring ∧
(1r‘(ℤring ×s
ℤring)) = ((〈1,
1〉(-g‘(ℤring ×s
ℤring))((1r‘((ℤring
×s ℤring) ↾s (ℤ
× {0})))(.r‘(ℤring
×s ℤring))〈1,
1〉))(+g‘(ℤring
×s
ℤring))(1r‘((ℤring
×s ℤring) ↾s (ℤ
× {0})))))) |
| 23 | 22 | simprd 495 |
. . 3
⊢
((((ℤring ×s
ℤring) ∈ Rng ∧ (ℤ × {0}) ∈
(2Ideal‘(ℤring ×s
ℤring))) ∧ (((ℤring
×s ℤring) ↾s (ℤ
× {0})) ∈ Ring ∧ ((ℤring
×s ℤring) /s
((ℤring ×s ℤring)
~QG (ℤ × {0}))) ∈ Ring) ∧ 〈1,
1〉 ∈ (1r‘((ℤring
×s ℤring) /s
((ℤring ×s ℤring)
~QG (ℤ × {0}))))) →
(1r‘(ℤring ×s
ℤring)) = ((〈1,
1〉(-g‘(ℤring ×s
ℤring))((1r‘((ℤring
×s ℤring) ↾s (ℤ
× {0})))(.r‘(ℤring
×s ℤring))〈1,
1〉))(+g‘(ℤring
×s
ℤring))(1r‘((ℤring
×s ℤring) ↾s (ℤ
× {0}))))) |
| 24 | 6, 12, 18, 23 | mp3an 1463 |
. 2
⊢
(1r‘(ℤring ×s
ℤring)) = ((〈1,
1〉(-g‘(ℤring ×s
ℤring))((1r‘((ℤring
×s ℤring) ↾s (ℤ
× {0})))(.r‘(ℤring
×s ℤring))〈1,
1〉))(+g‘(ℤring
×s
ℤring))(1r‘((ℤring
×s ℤring) ↾s (ℤ
× {0})))) |
| 25 | 1, 3, 4, 8 | pzriprnglem9 21500 |
. . . . 5
⊢
(1r‘((ℤring ×s
ℤring) ↾s (ℤ × {0}))) = 〈1,
0〉 |
| 26 | 25 | oveq1i 7441 |
. . . 4
⊢
((1r‘((ℤring
×s ℤring) ↾s (ℤ
× {0})))(.r‘(ℤring
×s ℤring))〈1, 1〉) =
(〈1, 0〉(.r‘(ℤring
×s ℤring))〈1,
1〉) |
| 27 | 26 | oveq2i 7442 |
. . 3
⊢ (〈1,
1〉(-g‘(ℤring ×s
ℤring))((1r‘((ℤring
×s ℤring) ↾s (ℤ
× {0})))(.r‘(ℤring
×s ℤring))〈1, 1〉)) =
(〈1, 1〉(-g‘(ℤring
×s ℤring))(〈1,
0〉(.r‘(ℤring ×s
ℤring))〈1, 1〉)) |
| 28 | 27, 25 | oveq12i 7443 |
. 2
⊢
((〈1, 1〉(-g‘(ℤring
×s
ℤring))((1r‘((ℤring
×s ℤring) ↾s (ℤ
× {0})))(.r‘(ℤring
×s ℤring))〈1,
1〉))(+g‘(ℤring
×s
ℤring))(1r‘((ℤring
×s ℤring) ↾s (ℤ
× {0})))) = ((〈1,
1〉(-g‘(ℤring ×s
ℤring))(〈1,
0〉(.r‘(ℤring ×s
ℤring))〈1,
1〉))(+g‘(ℤring
×s ℤring))〈1,
0〉) |
| 29 | | zringring 21460 |
. . . . . . 7
⊢
ℤring ∈ Ring |
| 30 | | zringbas 21464 |
. . . . . . . 8
⊢ ℤ =
(Base‘ℤring) |
| 31 | | id 22 |
. . . . . . . 8
⊢
(ℤring ∈ Ring → ℤring ∈
Ring) |
| 32 | 13 | a1i 11 |
. . . . . . . 8
⊢
(ℤring ∈ Ring → 1 ∈
ℤ) |
| 33 | | 0zd 12625 |
. . . . . . . 8
⊢
(ℤring ∈ Ring → 0 ∈
ℤ) |
| 34 | | zmulcl 12666 |
. . . . . . . . . 10
⊢ ((1
∈ ℤ ∧ 1 ∈ ℤ) → (1 · 1) ∈
ℤ) |
| 35 | 13, 13, 34 | mp2an 692 |
. . . . . . . . 9
⊢ (1
· 1) ∈ ℤ |
| 36 | 35 | a1i 11 |
. . . . . . . 8
⊢
(ℤring ∈ Ring → (1 · 1) ∈
ℤ) |
| 37 | | zringmulr 21468 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘ℤring) |
| 38 | 37 | eqcomi 2746 |
. . . . . . . . . . 11
⊢
(.r‘ℤring) = · |
| 39 | 38 | oveqi 7444 |
. . . . . . . . . 10
⊢
(0(.r‘ℤring)1) = (0 ·
1) |
| 40 | | 0z 12624 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
| 41 | | zmulcl 12666 |
. . . . . . . . . . 11
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) → (0 · 1) ∈
ℤ) |
| 42 | 40, 13, 41 | mp2an 692 |
. . . . . . . . . 10
⊢ (0
· 1) ∈ ℤ |
| 43 | 39, 42 | eqeltri 2837 |
. . . . . . . . 9
⊢
(0(.r‘ℤring)1) ∈
ℤ |
| 44 | 43 | a1i 11 |
. . . . . . . 8
⊢
(ℤring ∈ Ring →
(0(.r‘ℤring)1) ∈
ℤ) |
| 45 | | eqid 2737 |
. . . . . . . 8
⊢
(.r‘ℤring) =
(.r‘ℤring) |
| 46 | 1, 30, 30, 31, 31, 32, 33, 32, 32, 36, 44, 37, 45, 19 | xpsmul 17620 |
. . . . . . 7
⊢
(ℤring ∈ Ring → (〈1,
0〉(.r‘(ℤring ×s
ℤring))〈1, 1〉) = 〈(1 · 1),
(0(.r‘ℤring)1)〉) |
| 47 | 29, 46 | ax-mp 5 |
. . . . . 6
⊢ (〈1,
0〉(.r‘(ℤring ×s
ℤring))〈1, 1〉) = 〈(1 · 1),
(0(.r‘ℤring)1)〉 |
| 48 | 47 | oveq2i 7442 |
. . . . 5
⊢ (〈1,
1〉(-g‘(ℤring ×s
ℤring))(〈1,
0〉(.r‘(ℤring ×s
ℤring))〈1, 1〉)) = (〈1,
1〉(-g‘(ℤring ×s
ℤring))〈(1 · 1),
(0(.r‘ℤring)1)〉) |
| 49 | | 1t1e1 12428 |
. . . . . . 7
⊢ (1
· 1) = 1 |
| 50 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 51 | 50 | mul02i 11450 |
. . . . . . . 8
⊢ (0
· 1) = 0 |
| 52 | 39, 51 | eqtri 2765 |
. . . . . . 7
⊢
(0(.r‘ℤring)1) = 0 |
| 53 | 49, 52 | opeq12i 4878 |
. . . . . 6
⊢ 〈(1
· 1), (0(.r‘ℤring)1)〉 = 〈1,
0〉 |
| 54 | 53 | oveq2i 7442 |
. . . . 5
⊢ (〈1,
1〉(-g‘(ℤring ×s
ℤring))〈(1 · 1),
(0(.r‘ℤring)1)〉) = (〈1,
1〉(-g‘(ℤring ×s
ℤring))〈1, 0〉) |
| 55 | | zringgrp 21463 |
. . . . . . . 8
⊢
ℤring ∈ Grp |
| 56 | 55 | a1i 11 |
. . . . . . 7
⊢ (1 ∈
ℤ → ℤring ∈ Grp) |
| 57 | | id 22 |
. . . . . . 7
⊢ (1 ∈
ℤ → 1 ∈ ℤ) |
| 58 | | 0zd 12625 |
. . . . . . 7
⊢ (1 ∈
ℤ → 0 ∈ ℤ) |
| 59 | | eqid 2737 |
. . . . . . 7
⊢
(-g‘ℤring) =
(-g‘ℤring) |
| 60 | 1, 30, 30, 56, 56, 57, 57, 57, 58, 59, 59, 20 | xpsgrpsub 19079 |
. . . . . 6
⊢ (1 ∈
ℤ → (〈1, 1〉(-g‘(ℤring
×s ℤring))〈1, 0〉) =
〈(1(-g‘ℤring)1),
(1(-g‘ℤring)0)〉) |
| 61 | 13, 60 | ax-mp 5 |
. . . . 5
⊢ (〈1,
1〉(-g‘(ℤring ×s
ℤring))〈1, 0〉) =
〈(1(-g‘ℤring)1),
(1(-g‘ℤring)0)〉 |
| 62 | 48, 54, 61 | 3eqtri 2769 |
. . . 4
⊢ (〈1,
1〉(-g‘(ℤring ×s
ℤring))(〈1,
0〉(.r‘(ℤring ×s
ℤring))〈1, 1〉)) =
〈(1(-g‘ℤring)1),
(1(-g‘ℤring)0)〉 |
| 63 | 62 | oveq1i 7441 |
. . 3
⊢
((〈1, 1〉(-g‘(ℤring
×s ℤring))(〈1,
0〉(.r‘(ℤring ×s
ℤring))〈1,
1〉))(+g‘(ℤring
×s ℤring))〈1, 0〉) =
(〈(1(-g‘ℤring)1),
(1(-g‘ℤring)0)〉(+g‘(ℤring
×s ℤring))〈1, 0〉) |
| 64 | 59 | zringsub 21466 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ 1 ∈ ℤ) →
(1(-g‘ℤring)1) = (1 −
1)) |
| 65 | 13, 13, 64 | mp2an 692 |
. . . . . 6
⊢
(1(-g‘ℤring)1) = (1 −
1) |
| 66 | | 1m1e0 12338 |
. . . . . 6
⊢ (1
− 1) = 0 |
| 67 | 65, 66 | eqtri 2765 |
. . . . 5
⊢
(1(-g‘ℤring)1) = 0 |
| 68 | 59 | zringsub 21466 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ 0 ∈ ℤ) →
(1(-g‘ℤring)0) = (1 −
0)) |
| 69 | 13, 40, 68 | mp2an 692 |
. . . . 5
⊢
(1(-g‘ℤring)0) = (1 −
0) |
| 70 | 67, 69 | opeq12i 4878 |
. . . 4
⊢
〈(1(-g‘ℤring)1),
(1(-g‘ℤring)0)〉 = 〈0, (1 −
0)〉 |
| 71 | 70 | oveq1i 7441 |
. . 3
⊢
(〈(1(-g‘ℤring)1),
(1(-g‘ℤring)0)〉(+g‘(ℤring
×s ℤring))〈1, 0〉) = (〈0, (1 −
0)〉(+g‘(ℤring ×s
ℤring))〈1, 0〉) |
| 72 | | 1m0e1 12387 |
. . . . . 6
⊢ (1
− 0) = 1 |
| 73 | 72 | opeq2i 4877 |
. . . . 5
⊢ 〈0,
(1 − 0)〉 = 〈0, 1〉 |
| 74 | 73 | oveq1i 7441 |
. . . 4
⊢ (〈0,
(1 − 0)〉(+g‘(ℤring
×s ℤring))〈1, 0〉) =
(〈0, 1〉(+g‘(ℤring
×s ℤring))〈1,
0〉) |
| 75 | 29 | a1i 11 |
. . . . . 6
⊢ (1 ∈
ℤ → ℤring ∈ Ring) |
| 76 | 58, 57 | zaddcld 12726 |
. . . . . 6
⊢ (1 ∈
ℤ → (0 + 1) ∈ ℤ) |
| 77 | 57, 58 | zaddcld 12726 |
. . . . . 6
⊢ (1 ∈
ℤ → (1 + 0) ∈ ℤ) |
| 78 | | zringplusg 21465 |
. . . . . 6
⊢ + =
(+g‘ℤring) |
| 79 | 1, 30, 30, 75, 75, 58, 57, 57, 58, 76, 77, 78, 78, 21 | xpsadd 17619 |
. . . . 5
⊢ (1 ∈
ℤ → (〈0, 1〉(+g‘(ℤring
×s ℤring))〈1, 0〉) = 〈(0
+ 1), (1 + 0)〉) |
| 80 | 13, 79 | ax-mp 5 |
. . . 4
⊢ (〈0,
1〉(+g‘(ℤring ×s
ℤring))〈1, 0〉) = 〈(0 + 1), (1 +
0)〉 |
| 81 | | 0p1e1 12388 |
. . . . 5
⊢ (0 + 1) =
1 |
| 82 | | 1p0e1 12390 |
. . . . 5
⊢ (1 + 0) =
1 |
| 83 | 81, 82 | opeq12i 4878 |
. . . 4
⊢ 〈(0
+ 1), (1 + 0)〉 = 〈1, 1〉 |
| 84 | 74, 80, 83 | 3eqtri 2769 |
. . 3
⊢ (〈0,
(1 − 0)〉(+g‘(ℤring
×s ℤring))〈1, 0〉) = 〈1,
1〉 |
| 85 | 63, 71, 84 | 3eqtri 2769 |
. 2
⊢
((〈1, 1〉(-g‘(ℤring
×s ℤring))(〈1,
0〉(.r‘(ℤring ×s
ℤring))〈1,
1〉))(+g‘(ℤring
×s ℤring))〈1, 0〉) = 〈1,
1〉 |
| 86 | 24, 28, 85 | 3eqtri 2769 |
1
⊢
(1r‘(ℤring ×s
ℤring)) = 〈1, 1〉 |