Step | Hyp | Ref
| Expression |
1 | | pzriprng.r |
. . . . 5
⊢ 𝑅 = (ℤring
×s ℤring) |
2 | | pzriprng.i |
. . . . 5
⊢ 𝐼 = (ℤ ×
{0}) |
3 | | pzriprng.j |
. . . . 5
⊢ 𝐽 = (𝑅 ↾s 𝐼) |
4 | | pzriprng.1 |
. . . . 5
⊢ 1 =
(1r‘𝐽) |
5 | | pzriprng.g |
. . . . 5
⊢ ∼ =
(𝑅 ~QG
𝐼) |
6 | | pzriprng.q |
. . . . 5
⊢ 𝑄 = (𝑅 /s ∼ ) |
7 | 1, 2, 3, 4, 5, 6 | pzriprnglem11 21264 |
. . . 4
⊢
(Base‘𝑄) =
∪ 𝑦 ∈ ℤ {(ℤ × {𝑦})} |
8 | 7 | eleq2i 2824 |
. . 3
⊢ (𝑋 ∈ (Base‘𝑄) ↔ 𝑋 ∈ ∪
𝑦 ∈ ℤ {(ℤ
× {𝑦})}) |
9 | | eliun 5001 |
. . 3
⊢ (𝑋 ∈ ∪ 𝑦 ∈ ℤ {(ℤ × {𝑦})} ↔ ∃𝑦 ∈ ℤ 𝑋 ∈ {(ℤ × {𝑦})}) |
10 | 8, 9 | bitri 275 |
. 2
⊢ (𝑋 ∈ (Base‘𝑄) ↔ ∃𝑦 ∈ ℤ 𝑋 ∈ {(ℤ × {𝑦})}) |
11 | | elsni 4645 |
. . . 4
⊢ (𝑋 ∈ {(ℤ × {𝑦})} → 𝑋 = (ℤ × {𝑦})) |
12 | | 1z 12599 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
13 | 1, 2, 3, 4, 5 | pzriprnglem10 21263 |
. . . . . . . 8
⊢ ((1
∈ ℤ ∧ 𝑦
∈ ℤ) → [〈1, 𝑦〉] ∼ = (ℤ ×
{𝑦})) |
14 | 12, 13 | mpan 687 |
. . . . . . 7
⊢ (𝑦 ∈ ℤ → [〈1,
𝑦〉] ∼ = (ℤ ×
{𝑦})) |
15 | 14 | eqcomd 2737 |
. . . . . 6
⊢ (𝑦 ∈ ℤ → (ℤ
× {𝑦}) = [〈1,
𝑦〉] ∼ ) |
16 | 15 | eqeq2d 2742 |
. . . . 5
⊢ (𝑦 ∈ ℤ → (𝑋 = (ℤ × {𝑦}) ↔ 𝑋 = [〈1, 𝑦〉] ∼ )) |
17 | 1 | pzriprnglem1 21254 |
. . . . . . . . . 10
⊢ 𝑅 ∈ Rng |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → 𝑅 ∈ Rng) |
19 | 1, 2, 3 | pzriprnglem8 21261 |
. . . . . . . . . 10
⊢ 𝐼 ∈ (2Ideal‘𝑅) |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → 𝐼 ∈ (2Ideal‘𝑅)) |
21 | 1, 2 | pzriprnglem4 21257 |
. . . . . . . . . 10
⊢ 𝐼 ∈ (SubGrp‘𝑅) |
22 | 21 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → 𝐼 ∈ (SubGrp‘𝑅)) |
23 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → 1 ∈
ℤ) |
24 | 23, 23 | opelxpd 5715 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → 〈1,
1〉 ∈ (ℤ × ℤ)) |
25 | | id 22 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℤ) |
26 | 23, 25 | opelxpd 5715 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → 〈1,
𝑦〉 ∈ (ℤ
× ℤ)) |
27 | 1 | pzriprnglem2 21255 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(ℤ × ℤ) |
28 | 27 | eqcomi 2740 |
. . . . . . . . . 10
⊢ (ℤ
× ℤ) = (Base‘𝑅) |
29 | | eqid 2731 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
30 | | eqid 2731 |
. . . . . . . . . 10
⊢
(.r‘𝑄) = (.r‘𝑄) |
31 | 5, 6, 28, 29, 30 | qusmulrng 21032 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Rng ∧ 𝐼 ∈ (2Ideal‘𝑅) ∧ 𝐼 ∈ (SubGrp‘𝑅)) ∧ (〈1, 1〉 ∈ (ℤ
× ℤ) ∧ 〈1, 𝑦〉 ∈ (ℤ × ℤ)))
→ ([〈1, 1〉] ∼
(.r‘𝑄)[〈1, 𝑦〉] ∼ ) = [(〈1,
1〉(.r‘𝑅)〈1, 𝑦〉)] ∼ ) |
32 | 18, 20, 22, 24, 26, 31 | syl32anc 1377 |
. . . . . . . 8
⊢ (𝑦 ∈ ℤ →
([〈1, 1〉] ∼
(.r‘𝑄)[〈1, 𝑦〉] ∼ ) = [(〈1,
1〉(.r‘𝑅)〈1, 𝑦〉)] ∼ ) |
33 | | zringbas 21228 |
. . . . . . . . . . 11
⊢ ℤ =
(Base‘ℤring) |
34 | | zringring 21224 |
. . . . . . . . . . . 12
⊢
ℤring ∈ Ring |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℤ →
ℤring ∈ Ring) |
36 | 23, 23 | zmulcld 12679 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℤ → (1
· 1) ∈ ℤ) |
37 | 23, 25 | zmulcld 12679 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℤ → (1
· 𝑦) ∈
ℤ) |
38 | | zringmulr 21232 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℤring) |
39 | 1, 33, 33, 35, 35, 23, 23, 23, 25, 36, 37, 38, 38, 29 | xpsmul 17528 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → (〈1,
1〉(.r‘𝑅)〈1, 𝑦〉) = 〈(1 · 1), (1 ·
𝑦)〉) |
40 | | 1cnd 11216 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℤ → 1 ∈
ℂ) |
41 | 40 | mulridd 11238 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℤ → (1
· 1) = 1) |
42 | | zcn 12570 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
43 | 42 | mullidd 11239 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℤ → (1
· 𝑦) = 𝑦) |
44 | 41, 43 | opeq12d 4881 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → 〈(1
· 1), (1 · 𝑦)〉 = 〈1, 𝑦〉) |
45 | 39, 44 | eqtrd 2771 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → (〈1,
1〉(.r‘𝑅)〈1, 𝑦〉) = 〈1, 𝑦〉) |
46 | 45 | eceq1d 8748 |
. . . . . . . 8
⊢ (𝑦 ∈ ℤ →
[(〈1, 1〉(.r‘𝑅)〈1, 𝑦〉)] ∼ = [〈1, 𝑦〉] ∼ ) |
47 | 32, 46 | eqtrd 2771 |
. . . . . . 7
⊢ (𝑦 ∈ ℤ →
([〈1, 1〉] ∼
(.r‘𝑄)[〈1, 𝑦〉] ∼ ) = [〈1, 𝑦〉] ∼ ) |
48 | 5, 6, 28, 29, 30 | qusmulrng 21032 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Rng ∧ 𝐼 ∈ (2Ideal‘𝑅) ∧ 𝐼 ∈ (SubGrp‘𝑅)) ∧ (〈1, 𝑦〉 ∈ (ℤ × ℤ) ∧
〈1, 1〉 ∈ (ℤ × ℤ))) → ([〈1, 𝑦〉] ∼
(.r‘𝑄)[〈1, 1〉] ∼ ) = [(〈1,
𝑦〉(.r‘𝑅)〈1, 1〉)] ∼ ) |
49 | 18, 20, 22, 26, 24, 48 | syl32anc 1377 |
. . . . . . . 8
⊢ (𝑦 ∈ ℤ →
([〈1, 𝑦〉] ∼
(.r‘𝑄)[〈1, 1〉] ∼ ) = [(〈1,
𝑦〉(.r‘𝑅)〈1, 1〉)] ∼ ) |
50 | 25, 23 | zmulcld 12679 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℤ → (𝑦 · 1) ∈
ℤ) |
51 | 1, 33, 33, 35, 35, 23, 25, 23, 23, 36, 50, 38, 38, 29 | xpsmul 17528 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → (〈1,
𝑦〉(.r‘𝑅)〈1, 1〉) = 〈(1 · 1),
(𝑦 ·
1)〉) |
52 | 42 | mulridd 11238 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℤ → (𝑦 · 1) = 𝑦) |
53 | 41, 52 | opeq12d 4881 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → 〈(1
· 1), (𝑦 ·
1)〉 = 〈1, 𝑦〉) |
54 | 51, 53 | eqtrd 2771 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → (〈1,
𝑦〉(.r‘𝑅)〈1, 1〉) = 〈1, 𝑦〉) |
55 | 54 | eceq1d 8748 |
. . . . . . . 8
⊢ (𝑦 ∈ ℤ →
[(〈1, 𝑦〉(.r‘𝑅)〈1, 1〉)] ∼ = [〈1, 𝑦〉] ∼ ) |
56 | 49, 55 | eqtrd 2771 |
. . . . . . 7
⊢ (𝑦 ∈ ℤ →
([〈1, 𝑦〉] ∼
(.r‘𝑄)[〈1, 1〉] ∼ ) = [〈1, 𝑦〉] ∼ ) |
57 | 47, 56 | jca 511 |
. . . . . 6
⊢ (𝑦 ∈ ℤ →
(([〈1, 1〉] ∼
(.r‘𝑄)[〈1, 𝑦〉] ∼ ) = [〈1, 𝑦〉] ∼ ∧ ([〈1,
𝑦〉] ∼
(.r‘𝑄)[〈1, 1〉] ∼ ) = [〈1, 𝑦〉] ∼ )) |
58 | 1, 2, 3, 4, 5 | pzriprnglem10 21263 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ 1 ∈ ℤ) → [〈1, 1〉] ∼ =
(ℤ × {1})) |
59 | 12, 12, 58 | mp2an 689 |
. . . . . . . . . . 11
⊢ [〈1,
1〉] ∼ = (ℤ ×
{1}) |
60 | 59 | eqcomi 2740 |
. . . . . . . . . 10
⊢ (ℤ
× {1}) = [〈1, 1〉] ∼ |
61 | 60 | a1i 11 |
. . . . . . . . 9
⊢ (𝑋 = [〈1, 𝑦〉] ∼ → (ℤ
× {1}) = [〈1, 1〉] ∼ ) |
62 | | id 22 |
. . . . . . . . 9
⊢ (𝑋 = [〈1, 𝑦〉] ∼ → 𝑋 = [〈1, 𝑦〉] ∼ ) |
63 | 61, 62 | oveq12d 7430 |
. . . . . . . 8
⊢ (𝑋 = [〈1, 𝑦〉] ∼ → ((ℤ
× {1})(.r‘𝑄)𝑋) = ([〈1, 1〉] ∼
(.r‘𝑄)[〈1, 𝑦〉] ∼ )) |
64 | 63, 62 | eqeq12d 2747 |
. . . . . . 7
⊢ (𝑋 = [〈1, 𝑦〉] ∼ → (((ℤ
× {1})(.r‘𝑄)𝑋) = 𝑋 ↔ ([〈1, 1〉] ∼
(.r‘𝑄)[〈1, 𝑦〉] ∼ ) = [〈1, 𝑦〉] ∼ )) |
65 | 62, 61 | oveq12d 7430 |
. . . . . . . 8
⊢ (𝑋 = [〈1, 𝑦〉] ∼ → (𝑋(.r‘𝑄)(ℤ × {1})) =
([〈1, 𝑦〉] ∼
(.r‘𝑄)[〈1, 1〉] ∼ )) |
66 | 65, 62 | eqeq12d 2747 |
. . . . . . 7
⊢ (𝑋 = [〈1, 𝑦〉] ∼ → ((𝑋(.r‘𝑄)(ℤ × {1})) = 𝑋 ↔ ([〈1, 𝑦〉] ∼
(.r‘𝑄)[〈1, 1〉] ∼ ) = [〈1, 𝑦〉] ∼ )) |
67 | 64, 66 | anbi12d 630 |
. . . . . 6
⊢ (𝑋 = [〈1, 𝑦〉] ∼ → ((((ℤ
× {1})(.r‘𝑄)𝑋) = 𝑋 ∧ (𝑋(.r‘𝑄)(ℤ × {1})) = 𝑋) ↔ (([〈1, 1〉] ∼
(.r‘𝑄)[〈1, 𝑦〉] ∼ ) = [〈1, 𝑦〉] ∼ ∧ ([〈1,
𝑦〉] ∼
(.r‘𝑄)[〈1, 1〉] ∼ ) = [〈1, 𝑦〉] ∼
))) |
68 | 57, 67 | syl5ibrcom 246 |
. . . . 5
⊢ (𝑦 ∈ ℤ → (𝑋 = [〈1, 𝑦〉] ∼ → (((ℤ
× {1})(.r‘𝑄)𝑋) = 𝑋 ∧ (𝑋(.r‘𝑄)(ℤ × {1})) = 𝑋))) |
69 | 16, 68 | sylbid 239 |
. . . 4
⊢ (𝑦 ∈ ℤ → (𝑋 = (ℤ × {𝑦}) → (((ℤ ×
{1})(.r‘𝑄)𝑋) = 𝑋 ∧ (𝑋(.r‘𝑄)(ℤ × {1})) = 𝑋))) |
70 | 11, 69 | syl5 34 |
. . 3
⊢ (𝑦 ∈ ℤ → (𝑋 ∈ {(ℤ × {𝑦})} → (((ℤ ×
{1})(.r‘𝑄)𝑋) = 𝑋 ∧ (𝑋(.r‘𝑄)(ℤ × {1})) = 𝑋))) |
71 | 70 | rexlimiv 3147 |
. 2
⊢
(∃𝑦 ∈
ℤ 𝑋 ∈ {(ℤ
× {𝑦})} →
(((ℤ × {1})(.r‘𝑄)𝑋) = 𝑋 ∧ (𝑋(.r‘𝑄)(ℤ × {1})) = 𝑋)) |
72 | 10, 71 | sylbi 216 |
1
⊢ (𝑋 ∈ (Base‘𝑄) → (((ℤ ×
{1})(.r‘𝑄)𝑋) = 𝑋 ∧ (𝑋(.r‘𝑄)(ℤ × {1})) = 𝑋)) |