Proof of Theorem pzriprng1ALT
Step | Hyp | Ref
| Expression |
1 | | eqid 2731 |
. . . . 5
⊢
(ℤring ×s
ℤring) = (ℤring ×s
ℤring) |
2 | 1 | pzriprnglem1 21254 |
. . . 4
⊢
(ℤring ×s
ℤring) ∈ Rng |
3 | | eqid 2731 |
. . . . 5
⊢ (ℤ
× {0}) = (ℤ × {0}) |
4 | | eqid 2731 |
. . . . 5
⊢
((ℤring ×s
ℤring) ↾s (ℤ × {0})) =
((ℤring ×s ℤring)
↾s (ℤ × {0})) |
5 | 1, 3, 4 | pzriprnglem8 21261 |
. . . 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 21260 |
. . . 4
⊢
((ℤring ×s
ℤring) ↾s (ℤ × {0})) ∈
Ring |
8 | | eqid 2731 |
. . . . 5
⊢
(1r‘((ℤring ×s
ℤring) ↾s (ℤ × {0}))) =
(1r‘((ℤring ×s
ℤring) ↾s (ℤ ×
{0}))) |
9 | | eqid 2731 |
. . . . 5
⊢
((ℤring ×s
ℤring) ~QG (ℤ × {0})) =
((ℤring ×s ℤring)
~QG (ℤ × {0})) |
10 | | eqid 2731 |
. . . . 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 21266 |
. . . 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 12599 |
. . . . 5
⊢ 1 ∈
ℤ |
14 | | 1ex 11217 |
. . . . . 6
⊢ 1 ∈
V |
15 | 14 | snid 4664 |
. . . . 5
⊢ 1 ∈
{1} |
16 | 13, 15 | opelxpii 5714 |
. . . 4
⊢ 〈1,
1〉 ∈ (ℤ × {1}) |
17 | 1, 3, 4, 8, 9, 10 | pzriprnglem14 21267 |
. . . 4
⊢
(1r‘((ℤring ×s
ℤring) /s ((ℤring
×s ℤring) ~QG
(ℤ × {0})))) = (ℤ × {1}) |
18 | 16, 17 | eleqtrri 2831 |
. . 3
⊢ 〈1,
1〉 ∈ (1r‘((ℤring
×s ℤring) /s
((ℤring ×s ℤring)
~QG (ℤ × {0})))) |
19 | | eqid 2731 |
. . . . 5
⊢
(.r‘(ℤring ×s
ℤring)) = (.r‘(ℤring
×s ℤring)) |
20 | | eqid 2731 |
. . . . 5
⊢
(-g‘(ℤring ×s
ℤring)) = (-g‘(ℤring
×s ℤring)) |
21 | | eqid 2731 |
. . . . 5
⊢
(+g‘(ℤring ×s
ℤring)) = (+g‘(ℤring
×s ℤring)) |
22 | 19, 8, 20, 21 | ring2idlqus1 21082 |
. . . 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 1460 |
. 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 21262 |
. . . . 5
⊢
(1r‘((ℤring ×s
ℤring) ↾s (ℤ × {0}))) = 〈1,
0〉 |
26 | 25 | oveq1i 7422 |
. . . 4
⊢
((1r‘((ℤring
×s ℤring) ↾s (ℤ
× {0})))(.r‘(ℤring
×s ℤring))〈1, 1〉) =
(〈1, 0〉(.r‘(ℤring
×s ℤring))〈1,
1〉) |
27 | 26 | oveq2i 7423 |
. . 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 7424 |
. 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 21224 |
. . . . . . 7
⊢
ℤring ∈ Ring |
30 | | zringbas 21228 |
. . . . . . . 8
⊢ ℤ =
(Base‘ℤring) |
31 | | id 22 |
. . . . . . . 8
⊢
(ℤring ∈ Ring → ℤring ∈
Ring) |
32 | 13 | a1i 11 |
. . . . . . . 8
⊢
(ℤring ∈ Ring → 1 ∈
ℤ) |
33 | | 0zd 12577 |
. . . . . . . 8
⊢
(ℤring ∈ Ring → 0 ∈
ℤ) |
34 | | zmulcl 12618 |
. . . . . . . . . 10
⊢ ((1
∈ ℤ ∧ 1 ∈ ℤ) → (1 · 1) ∈
ℤ) |
35 | 13, 13, 34 | mp2an 689 |
. . . . . . . . 9
⊢ (1
· 1) ∈ ℤ |
36 | 35 | a1i 11 |
. . . . . . . 8
⊢
(ℤring ∈ Ring → (1 · 1) ∈
ℤ) |
37 | | zringmulr 21232 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘ℤring) |
38 | 37 | eqcomi 2740 |
. . . . . . . . . . 11
⊢
(.r‘ℤring) = · |
39 | 38 | oveqi 7425 |
. . . . . . . . . 10
⊢
(0(.r‘ℤring)1) = (0 ·
1) |
40 | | 0z 12576 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
41 | | zmulcl 12618 |
. . . . . . . . . . 11
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) → (0 · 1) ∈
ℤ) |
42 | 40, 13, 41 | mp2an 689 |
. . . . . . . . . 10
⊢ (0
· 1) ∈ ℤ |
43 | 39, 42 | eqeltri 2828 |
. . . . . . . . 9
⊢
(0(.r‘ℤring)1) ∈
ℤ |
44 | 43 | a1i 11 |
. . . . . . . 8
⊢
(ℤring ∈ Ring →
(0(.r‘ℤring)1) ∈
ℤ) |
45 | | eqid 2731 |
. . . . . . . 8
⊢
(.r‘ℤring) =
(.r‘ℤring) |
46 | 1, 30, 30, 31, 31, 32, 33, 32, 32, 36, 44, 37, 45, 19 | xpsmul 17528 |
. . . . . . 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 7423 |
. . . . 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 12381 |
. . . . . . 7
⊢ (1
· 1) = 1 |
50 | | ax-1cn 11174 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
51 | 50 | mul02i 11410 |
. . . . . . . 8
⊢ (0
· 1) = 0 |
52 | 39, 51 | eqtri 2759 |
. . . . . . 7
⊢
(0(.r‘ℤring)1) = 0 |
53 | 49, 52 | opeq12i 4878 |
. . . . . 6
⊢ 〈(1
· 1), (0(.r‘ℤring)1)〉 = 〈1,
0〉 |
54 | 53 | oveq2i 7423 |
. . . . 5
⊢ (〈1,
1〉(-g‘(ℤring ×s
ℤring))〈(1 · 1),
(0(.r‘ℤring)1)〉) = (〈1,
1〉(-g‘(ℤring ×s
ℤring))〈1, 0〉) |
55 | | zringgrp 21227 |
. . . . . . . 8
⊢
ℤring ∈ Grp |
56 | 55 | a1i 11 |
. . . . . . 7
⊢ (1 ∈
ℤ → ℤring ∈ Grp) |
57 | | id 22 |
. . . . . . 7
⊢ (1 ∈
ℤ → 1 ∈ ℤ) |
58 | | 0zd 12577 |
. . . . . . 7
⊢ (1 ∈
ℤ → 0 ∈ ℤ) |
59 | | eqid 2731 |
. . . . . . 7
⊢
(-g‘ℤring) =
(-g‘ℤring) |
60 | 1, 30, 30, 56, 56, 57, 57, 57, 58, 59, 59, 20 | xpsgrpsub 18984 |
. . . . . 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 2763 |
. . . 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 7422 |
. . 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 21230 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ 1 ∈ ℤ) →
(1(-g‘ℤring)1) = (1 −
1)) |
65 | 13, 13, 64 | mp2an 689 |
. . . . . 6
⊢
(1(-g‘ℤring)1) = (1 −
1) |
66 | | 1m1e0 12291 |
. . . . . 6
⊢ (1
− 1) = 0 |
67 | 65, 66 | eqtri 2759 |
. . . . 5
⊢
(1(-g‘ℤring)1) = 0 |
68 | 59 | zringsub 21230 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ 0 ∈ ℤ) →
(1(-g‘ℤring)0) = (1 −
0)) |
69 | 13, 40, 68 | mp2an 689 |
. . . . 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 7422 |
. . 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 12340 |
. . . . . 6
⊢ (1
− 0) = 1 |
73 | 72 | opeq2i 4877 |
. . . . 5
⊢ 〈0,
(1 − 0)〉 = 〈0, 1〉 |
74 | 73 | oveq1i 7422 |
. . . 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 12677 |
. . . . . 6
⊢ (1 ∈
ℤ → (0 + 1) ∈ ℤ) |
77 | 57, 58 | zaddcld 12677 |
. . . . . 6
⊢ (1 ∈
ℤ → (1 + 0) ∈ ℤ) |
78 | | zringplusg 21229 |
. . . . . 6
⊢ + =
(+g‘ℤring) |
79 | 1, 30, 30, 75, 75, 58, 57, 57, 58, 76, 77, 78, 78, 21 | xpsadd 17527 |
. . . . 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 12341 |
. . . . 5
⊢ (0 + 1) =
1 |
82 | | 1p0e1 12343 |
. . . . 5
⊢ (1 + 0) =
1 |
83 | 81, 82 | opeq12i 4878 |
. . . 4
⊢ 〈(0
+ 1), (1 + 0)〉 = 〈1, 1〉 |
84 | 74, 80, 83 | 3eqtri 2763 |
. . 3
⊢ (〈0,
(1 − 0)〉(+g‘(ℤring
×s ℤring))〈1, 0〉) = 〈1,
1〉 |
85 | 63, 71, 84 | 3eqtri 2763 |
. 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 2763 |
1
⊢
(1r‘(ℤring ×s
ℤring)) = 〈1, 1〉 |