| Step | Hyp | Ref
| Expression |
| 1 | | prex 5437 |
. . . 4
⊢ {0, 1}
∈ V |
| 2 | 1 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → {0, 1}
∈ V) |
| 3 | | fnconstg 6796 |
. . . 4
⊢ (𝐴 ∈ ℤ → ({0, 1}
× {𝐴}) Fn {0,
1}) |
| 4 | 3 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ({0, 1}
× {𝐴}) Fn {0,
1}) |
| 5 | | c0ex 11255 |
. . . . . 6
⊢ 0 ∈
V |
| 6 | | 1ex 11257 |
. . . . . 6
⊢ 1 ∈
V |
| 7 | 5, 6 | pm3.2i 470 |
. . . . 5
⊢ (0 ∈
V ∧ 1 ∈ V) |
| 8 | 7 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (0
∈ V ∧ 1 ∈ V)) |
| 9 | | 3simpc 1151 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵 ∈ ℤ ∧ 𝐶 ∈
ℤ)) |
| 10 | | 0ne1 12337 |
. . . . 5
⊢ 0 ≠
1 |
| 11 | 10 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 0 ≠
1) |
| 12 | | fnprg 6625 |
. . . 4
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 0 ≠ 1) →
{〈0, 𝐵〉, 〈1,
𝐶〉} Fn {0,
1}) |
| 13 | 8, 9, 11, 12 | syl3anc 1373 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
{〈0, 𝐵〉, 〈1,
𝐶〉} Fn {0,
1}) |
| 14 | 2, 4, 13 | offvalfv 7719 |
. 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 2737 |
. . 3
⊢
(Base‘𝑍) =
(Base‘𝑍) |
| 17 | | eqid 2737 |
. . 3
⊢
(Base‘ℤring) =
(Base‘ℤring) |
| 18 | | simp1 1137 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∈
ℤ) |
| 19 | | zringbas 21464 |
. . . 4
⊢ ℤ =
(Base‘ℤring) |
| 20 | 18, 19 | eleqtrdi 2851 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∈
(Base‘ℤring)) |
| 21 | 15 | zlmodzxzel 48271 |
. . . 4
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
{〈0, 𝐵〉, 〈1,
𝐶〉} ∈
(Base‘𝑍)) |
| 22 | 21 | 3adant1 1131 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
{〈0, 𝐵〉, 〈1,
𝐶〉} ∈
(Base‘𝑍)) |
| 23 | | zlmodzxzscm.t |
. . 3
⊢ ∙ = (
·𝑠 ‘𝑍) |
| 24 | | eqid 2737 |
. . 3
⊢
(.r‘ℤring) =
(.r‘ℤring) |
| 25 | 15, 16, 17, 2, 20, 22, 23, 24 | frlmvscafval 21786 |
. 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 7466 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐵) ∈ V) |
| 29 | | ovexd 7466 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 · 𝐶) ∈ V) |
| 30 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 0 → (({0, 1} ×
{𝐴})‘𝑥) = (({0, 1} × {𝐴})‘0)) |
| 31 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 0 → ({〈0, 𝐵〉, 〈1, 𝐶〉}‘𝑥) = ({〈0, 𝐵〉, 〈1, 𝐶〉}‘0)) |
| 32 | 30, 31 | oveq12d 7449 |
. . . 4
⊢ (𝑥 = 0 → ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘𝑥)) = ((({0, 1} × {𝐴})‘0)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘0))) |
| 33 | | zringmulr 21468 |
. . . . . . 7
⊢ ·
= (.r‘ℤring) |
| 34 | 33 | eqcomi 2746 |
. . . . . 6
⊢
(.r‘ℤring) = · |
| 35 | 34 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
(.r‘ℤring) = · ) |
| 36 | 5 | prid1 4762 |
. . . . . 6
⊢ 0 ∈
{0, 1} |
| 37 | | fvconst2g 7222 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 0 ∈
{0, 1}) → (({0, 1} × {𝐴})‘0) = 𝐴) |
| 38 | 18, 36, 37 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (({0, 1}
× {𝐴})‘0) =
𝐴) |
| 39 | | simp2 1138 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐵 ∈
ℤ) |
| 40 | | fvpr1g 7210 |
. . . . . 6
⊢ ((0
∈ V ∧ 𝐵 ∈
ℤ ∧ 0 ≠ 1) → ({〈0, 𝐵〉, 〈1, 𝐶〉}‘0) = 𝐵) |
| 41 | 26, 39, 11, 40 | syl3anc 1373 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
({〈0, 𝐵〉,
〈1, 𝐶〉}‘0)
= 𝐵) |
| 42 | 35, 38, 41 | oveq123d 7452 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((({0,
1} × {𝐴})‘0)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘0)) = (𝐴 · 𝐵)) |
| 43 | 32, 42 | sylan9eqr 2799 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝑥 = 0) → ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘𝑥)) = (𝐴 · 𝐵)) |
| 44 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 1 → (({0, 1} ×
{𝐴})‘𝑥) = (({0, 1} × {𝐴})‘1)) |
| 45 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 1 → ({〈0, 𝐵〉, 〈1, 𝐶〉}‘𝑥) = ({〈0, 𝐵〉, 〈1, 𝐶〉}‘1)) |
| 46 | 44, 45 | oveq12d 7449 |
. . . 4
⊢ (𝑥 = 1 → ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘𝑥)) = ((({0, 1} × {𝐴})‘1)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘1))) |
| 47 | 6 | prid2 4763 |
. . . . . 6
⊢ 1 ∈
{0, 1} |
| 48 | | fvconst2g 7222 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 1 ∈
{0, 1}) → (({0, 1} × {𝐴})‘1) = 𝐴) |
| 49 | 18, 47, 48 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (({0, 1}
× {𝐴})‘1) =
𝐴) |
| 50 | | simp3 1139 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐶 ∈
ℤ) |
| 51 | | fvpr2g 7211 |
. . . . . 6
⊢ ((1
∈ V ∧ 𝐶 ∈
ℤ ∧ 0 ≠ 1) → ({〈0, 𝐵〉, 〈1, 𝐶〉}‘1) = 𝐶) |
| 52 | 27, 50, 11, 51 | syl3anc 1373 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
({〈0, 𝐵〉,
〈1, 𝐶〉}‘1)
= 𝐶) |
| 53 | 35, 49, 52 | oveq123d 7452 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((({0,
1} × {𝐴})‘1)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘1)) = (𝐴 · 𝐶)) |
| 54 | 46, 53 | sylan9eqr 2799 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝑥 = 1) → ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘𝑥)) = (𝐴 · 𝐶)) |
| 55 | 26, 27, 28, 29, 43, 54 | fmptpr 7192 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) →
{〈0, (𝐴 · 𝐵)〉, 〈1, (𝐴 · 𝐶)〉} = (𝑥 ∈ {0, 1} ↦ ((({0, 1} ×
{𝐴})‘𝑥)(.r‘ℤring)({〈0,
𝐵〉, 〈1, 𝐶〉}‘𝑥)))) |
| 56 | 14, 25, 55 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∙ {〈0, 𝐵〉, 〈1, 𝐶〉}) = {〈0, (𝐴 · 𝐵)〉, 〈1, (𝐴 · 𝐶)〉}) |