Step | Hyp | Ref
| Expression |
1 | | prex 5300 |
. . . 4
⊢ {0, 1}
∈ V |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → {0, 1}
∈ V) |
3 | | fnconstg 6567 |
. . . 4
⊢ (𝐴 ∈ ℤ → ({0, 1}
× {𝐴}) Fn {0,
1}) |
4 | 3 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ({0, 1}
× {𝐴}) Fn {0,
1}) |
5 | | c0ex 10714 |
. . . . . 6
⊢ 0 ∈
V |
6 | | 1ex 10716 |
. . . . . 6
⊢ 1 ∈
V |
7 | 5, 6 | pm3.2i 474 |
. . . . 5
⊢ (0 ∈
V ∧ 1 ∈ V) |
8 | 7 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (0
∈ V ∧ 1 ∈ V)) |
9 | | 3simpc 1151 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 ∈ ℤ ∧ 𝐶 ∈
ℤ)) |
10 | | 0ne1 11788 |
. . . . 5
⊢ 0 ≠
1 |
11 | 10 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 0 ≠
1) |
12 | | fnprg 6399 |
. . . 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 45204 |
. 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 2738 |
. . 3
⊢
(Base‘𝑍) =
(Base‘𝑍) |
17 | | eqid 2738 |
. . 3
⊢
(Base‘ℤring) =
(Base‘ℤring) |
18 | | simp1 1137 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∈
ℤ) |
19 | | zringbas 20296 |
. . . 4
⊢ ℤ =
(Base‘ℤring) |
20 | 18, 19 | eleqtrdi 2843 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∈
(Base‘ℤring)) |
21 | 15 | zlmodzxzel 45217 |
. . . 4
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
{〈0, 𝐵〉, 〈1,
𝐶〉} ∈
(Base‘𝑍)) |
22 | 21 | 3adant1 1131 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
{〈0, 𝐵〉, 〈1,
𝐶〉} ∈
(Base‘𝑍)) |
23 | | zlmodzxzscm.t |
. . 3
⊢ ∙ = (
·𝑠 ‘𝑍) |
24 | | eqid 2738 |
. . 3
⊢
(.r‘ℤring) =
(.r‘ℤring) |
25 | 15, 16, 17, 2, 20, 22, 23, 24 | frlmvscafval 20583 |
. 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 7206 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐵) ∈ V) |
29 | | ovexd 7206 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐶) ∈ V) |
30 | | fveq2 6675 |
. . . . 5
⊢ (𝑥 = 0 → (({0, 1} ×
{𝐴})‘𝑥) = (({0, 1} × {𝐴})‘0)) |
31 | | fveq2 6675 |
. . . . 5
⊢ (𝑥 = 0 → ({〈0, 𝐵〉, 〈1, 𝐶〉}‘𝑥) = ({〈0, 𝐵〉, 〈1, 𝐶〉}‘0)) |
32 | 30, 31 | oveq12d 7189 |
. . . 4
⊢ (𝑥 = 0 → ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘𝑥)) = ((({0, 1} × {𝐴})‘0)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘0))) |
33 | | zringmulr 20299 |
. . . . . . 7
⊢ ·
= (.r‘ℤring) |
34 | 33 | eqcomi 2747 |
. . . . . 6
⊢
(.r‘ℤring) = · |
35 | 34 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
(.r‘ℤring) = · ) |
36 | 5 | prid1 4654 |
. . . . . 6
⊢ 0 ∈
{0, 1} |
37 | | fvconst2g 6975 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 0 ∈
{0, 1}) → (({0, 1} × {𝐴})‘0) = 𝐴) |
38 | 18, 36, 37 | sylancl 589 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (({0, 1}
× {𝐴})‘0) =
𝐴) |
39 | | simp2 1138 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐵 ∈
ℤ) |
40 | | fvpr1g 6965 |
. . . . . 6
⊢ ((0
∈ V ∧ 𝐵 ∈
ℤ ∧ 0 ≠ 1) → ({〈0, 𝐵〉, 〈1, 𝐶〉}‘0) = 𝐵) |
41 | 26, 39, 11, 40 | syl3anc 1372 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
({〈0, 𝐵〉,
〈1, 𝐶〉}‘0)
= 𝐵) |
42 | 35, 38, 41 | oveq123d 7192 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((({0,
1} × {𝐴})‘0)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘0)) = (𝐴 · 𝐵)) |
43 | 32, 42 | sylan9eqr 2795 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝑥 = 0) → ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘𝑥)) = (𝐴 · 𝐵)) |
44 | | fveq2 6675 |
. . . . 5
⊢ (𝑥 = 1 → (({0, 1} ×
{𝐴})‘𝑥) = (({0, 1} × {𝐴})‘1)) |
45 | | fveq2 6675 |
. . . . 5
⊢ (𝑥 = 1 → ({〈0, 𝐵〉, 〈1, 𝐶〉}‘𝑥) = ({〈0, 𝐵〉, 〈1, 𝐶〉}‘1)) |
46 | 44, 45 | oveq12d 7189 |
. . . 4
⊢ (𝑥 = 1 → ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘𝑥)) = ((({0, 1} × {𝐴})‘1)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘1))) |
47 | 6 | prid2 4655 |
. . . . . 6
⊢ 1 ∈
{0, 1} |
48 | | fvconst2g 6975 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 1 ∈
{0, 1}) → (({0, 1} × {𝐴})‘1) = 𝐴) |
49 | 18, 47, 48 | sylancl 589 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (({0, 1}
× {𝐴})‘1) =
𝐴) |
50 | | simp3 1139 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐶 ∈
ℤ) |
51 | | fvpr2g 6966 |
. . . . . 6
⊢ ((1
∈ V ∧ 𝐶 ∈
ℤ ∧ 0 ≠ 1) → ({〈0, 𝐵〉, 〈1, 𝐶〉}‘1) = 𝐶) |
52 | 27, 50, 11, 51 | syl3anc 1372 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
({〈0, 𝐵〉,
〈1, 𝐶〉}‘1)
= 𝐶) |
53 | 35, 49, 52 | oveq123d 7192 |
. . . 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 6945 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
{〈0, (𝐴 · 𝐵)〉, 〈1, (𝐴 · 𝐶)〉} = (𝑥 ∈ {0, 1} ↦ ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘𝑥)))) |
56 | 14, 25, 55 | 3eqtr4d 2783 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∙ {〈0, 𝐵〉, 〈1, 𝐶〉}) = {〈0, (𝐴 · 𝐵)〉, 〈1, (𝐴 · 𝐶)〉}) |