Step | Hyp | Ref
| Expression |
1 | | prex 5433 |
. . . 4
⊢ {0, 1}
∈ V |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → {0, 1}
∈ V) |
3 | | fnconstg 6780 |
. . . 4
⊢ (𝐴 ∈ ℤ → ({0, 1}
× {𝐴}) Fn {0,
1}) |
4 | 3 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ({0, 1}
× {𝐴}) Fn {0,
1}) |
5 | | c0ex 11208 |
. . . . . 6
⊢ 0 ∈
V |
6 | | 1ex 11210 |
. . . . . 6
⊢ 1 ∈
V |
7 | 5, 6 | pm3.2i 472 |
. . . . 5
⊢ (0 ∈
V ∧ 1 ∈ V) |
8 | 7 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (0
∈ V ∧ 1 ∈ V)) |
9 | | 3simpc 1151 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 ∈ ℤ ∧ 𝐶 ∈
ℤ)) |
10 | | 0ne1 12283 |
. . . . 5
⊢ 0 ≠
1 |
11 | 10 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 0 ≠
1) |
12 | | fnprg 6608 |
. . . 4
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 0 ≠ 1) →
{⟨0, 𝐵⟩, ⟨1,
𝐶⟩} Fn {0,
1}) |
13 | 8, 9, 11, 12 | syl3anc 1372 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
{⟨0, 𝐵⟩, ⟨1,
𝐶⟩} Fn {0,
1}) |
14 | 2, 4, 13 | offvalfv 47018 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (({0, 1}
× {𝐴})
∘f (.r‘ℤring){⟨0, 𝐵⟩, ⟨1, 𝐶⟩}) = (𝑥 ∈ {0, 1} ↦ ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({⟨0,
𝐵⟩, ⟨1, 𝐶⟩}‘𝑥)))) |
15 | | zlmodzxz.z |
. . 3
⊢ 𝑍 = (ℤring
freeLMod {0, 1}) |
16 | | eqid 2733 |
. . 3
⊢
(Base‘𝑍) =
(Base‘𝑍) |
17 | | eqid 2733 |
. . 3
⊢
(Base‘ℤring) =
(Base‘ℤring) |
18 | | simp1 1137 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∈
ℤ) |
19 | | zringbas 21023 |
. . . 4
⊢ ℤ =
(Base‘ℤring) |
20 | 18, 19 | eleqtrdi 2844 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∈
(Base‘ℤring)) |
21 | 15 | zlmodzxzel 47031 |
. . . 4
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
{⟨0, 𝐵⟩, ⟨1,
𝐶⟩} ∈
(Base‘𝑍)) |
22 | 21 | 3adant1 1131 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
{⟨0, 𝐵⟩, ⟨1,
𝐶⟩} ∈
(Base‘𝑍)) |
23 | | zlmodzxzscm.t |
. . 3
⊢ ∙ = (
·𝑠 ‘𝑍) |
24 | | eqid 2733 |
. . 3
⊢
(.r‘ℤring) =
(.r‘ℤring) |
25 | 15, 16, 17, 2, 20, 22, 23, 24 | frlmvscafval 21321 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∙ {⟨0, 𝐵⟩, ⟨1, 𝐶⟩}) = (({0, 1} ×
{𝐴}) ∘f
(.r‘ℤring){⟨0, 𝐵⟩, ⟨1, 𝐶⟩})) |
26 | 5 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 0 ∈
V) |
27 | 6 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 1 ∈
V) |
28 | | ovexd 7444 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐵) ∈ V) |
29 | | ovexd 7444 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐶) ∈ V) |
30 | | fveq2 6892 |
. . . . 5
⊢ (𝑥 = 0 → (({0, 1} ×
{𝐴})‘𝑥) = (({0, 1} × {𝐴})‘0)) |
31 | | fveq2 6892 |
. . . . 5
⊢ (𝑥 = 0 → ({⟨0, 𝐵⟩, ⟨1, 𝐶⟩}‘𝑥) = ({⟨0, 𝐵⟩, ⟨1, 𝐶⟩}‘0)) |
32 | 30, 31 | oveq12d 7427 |
. . . 4
⊢ (𝑥 = 0 → ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({⟨0,
𝐵⟩, ⟨1, 𝐶⟩}‘𝑥)) = ((({0, 1} × {𝐴})‘0)(.r‘ℤring)({⟨0,
𝐵⟩, ⟨1, 𝐶⟩}‘0))) |
33 | | zringmulr 21027 |
. . . . . . 7
⊢ ·
= (.r‘ℤring) |
34 | 33 | eqcomi 2742 |
. . . . . 6
⊢
(.r‘ℤring) = · |
35 | 34 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
(.r‘ℤring) = · ) |
36 | 5 | prid1 4767 |
. . . . . 6
⊢ 0 ∈
{0, 1} |
37 | | fvconst2g 7203 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 0 ∈
{0, 1}) → (({0, 1} × {𝐴})‘0) = 𝐴) |
38 | 18, 36, 37 | sylancl 587 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (({0, 1}
× {𝐴})‘0) =
𝐴) |
39 | | simp2 1138 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐵 ∈
ℤ) |
40 | | fvpr1g 7188 |
. . . . . 6
⊢ ((0
∈ V ∧ 𝐵 ∈
ℤ ∧ 0 ≠ 1) → ({⟨0, 𝐵⟩, ⟨1, 𝐶⟩}‘0) = 𝐵) |
41 | 26, 39, 11, 40 | syl3anc 1372 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
({⟨0, 𝐵⟩,
⟨1, 𝐶⟩}‘0)
= 𝐵) |
42 | 35, 38, 41 | oveq123d 7430 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((({0,
1} × {𝐴})‘0)(.r‘ℤring)({⟨0,
𝐵⟩, ⟨1, 𝐶⟩}‘0)) = (𝐴 · 𝐵)) |
43 | 32, 42 | sylan9eqr 2795 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝑥 = 0) → ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({⟨0,
𝐵⟩, ⟨1, 𝐶⟩}‘𝑥)) = (𝐴 · 𝐵)) |
44 | | fveq2 6892 |
. . . . 5
⊢ (𝑥 = 1 → (({0, 1} ×
{𝐴})‘𝑥) = (({0, 1} × {𝐴})‘1)) |
45 | | fveq2 6892 |
. . . . 5
⊢ (𝑥 = 1 → ({⟨0, 𝐵⟩, ⟨1, 𝐶⟩}‘𝑥) = ({⟨0, 𝐵⟩, ⟨1, 𝐶⟩}‘1)) |
46 | 44, 45 | oveq12d 7427 |
. . . 4
⊢ (𝑥 = 1 → ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({⟨0,
𝐵⟩, ⟨1, 𝐶⟩}‘𝑥)) = ((({0, 1} × {𝐴})‘1)(.r‘ℤring)({⟨0,
𝐵⟩, ⟨1, 𝐶⟩}‘1))) |
47 | 6 | prid2 4768 |
. . . . . 6
⊢ 1 ∈
{0, 1} |
48 | | fvconst2g 7203 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 1 ∈
{0, 1}) → (({0, 1} × {𝐴})‘1) = 𝐴) |
49 | 18, 47, 48 | sylancl 587 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (({0, 1}
× {𝐴})‘1) =
𝐴) |
50 | | simp3 1139 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐶 ∈
ℤ) |
51 | | fvpr2g 7189 |
. . . . . 6
⊢ ((1
∈ V ∧ 𝐶 ∈
ℤ ∧ 0 ≠ 1) → ({⟨0, 𝐵⟩, ⟨1, 𝐶⟩}‘1) = 𝐶) |
52 | 27, 50, 11, 51 | syl3anc 1372 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
({⟨0, 𝐵⟩,
⟨1, 𝐶⟩}‘1)
= 𝐶) |
53 | 35, 49, 52 | oveq123d 7430 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((({0,
1} × {𝐴})‘1)(.r‘ℤring)({⟨0,
𝐵⟩, ⟨1, 𝐶⟩}‘1)) = (𝐴 · 𝐶)) |
54 | 46, 53 | sylan9eqr 2795 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝑥 = 1) → ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({⟨0,
𝐵⟩, ⟨1, 𝐶⟩}‘𝑥)) = (𝐴 · 𝐶)) |
55 | 26, 27, 28, 29, 43, 54 | fmptpr 7170 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
{⟨0, (𝐴 · 𝐵)⟩, ⟨1, (𝐴 · 𝐶)⟩} = (𝑥 ∈ {0, 1} ↦ ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({⟨0,
𝐵⟩, ⟨1, 𝐶⟩}‘𝑥)))) |
56 | 14, 25, 55 | 3eqtr4d 2783 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∙ {⟨0, 𝐵⟩, ⟨1, 𝐶⟩}) = {⟨0, (𝐴 · 𝐵)⟩, ⟨1, (𝐴 · 𝐶)⟩}) |