Step | Hyp | Ref
| Expression |
1 | | xpsvsca.3 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝐾) |
2 | | df-ov 7263 |
. . . . 5
⊢ (𝐵(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})𝐶) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘〈𝐵, 𝐶〉) |
3 | | xpsvsca.4 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑋) |
4 | | xpsvsca.5 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑌) |
5 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) |
6 | 5 | xpsfval 17221 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌) → (𝐵(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})𝐶) = {〈∅, 𝐵〉, 〈1o, 𝐶〉}) |
7 | 3, 4, 6 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → (𝐵(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})𝐶) = {〈∅, 𝐵〉, 〈1o, 𝐶〉}) |
8 | 2, 7 | eqtr3id 2791 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘〈𝐵, 𝐶〉) = {〈∅, 𝐵〉, 〈1o, 𝐶〉}) |
9 | 3, 4 | opelxpd 5623 |
. . . . 5
⊢ (𝜑 → 〈𝐵, 𝐶〉 ∈ (𝑋 × 𝑌)) |
10 | 5 | xpsff1o2 17224 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) |
11 | | f1of 6705 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) |
13 | 12 | ffvelrni 6947 |
. . . . 5
⊢
(〈𝐵, 𝐶〉 ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘〈𝐵, 𝐶〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})) |
14 | 9, 13 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘〈𝐵, 𝐶〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})) |
15 | 8, 14 | eqeltrrd 2838 |
. . 3
⊢ (𝜑 → {〈∅, 𝐵〉, 〈1o,
𝐶〉} ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})) |
16 | | xpssca.t |
. . . . 5
⊢ 𝑇 = (𝑅 ×s 𝑆) |
17 | | xpsvsca.x |
. . . . 5
⊢ 𝑋 = (Base‘𝑅) |
18 | | xpsvsca.y |
. . . . 5
⊢ 𝑌 = (Base‘𝑆) |
19 | | xpssca.1 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
20 | | xpssca.2 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
21 | | xpssca.g |
. . . . 5
⊢ 𝐺 = (Scalar‘𝑅) |
22 | | eqid 2737 |
. . . . 5
⊢ (𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) = (𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) |
23 | 16, 17, 18, 19, 20, 5, 21, 22 | xpsval 17225 |
. . . 4
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})
“s (𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) |
24 | 16, 17, 18, 19, 20, 5, 21, 22 | xpsrnbas 17226 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) = (Base‘(𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) |
25 | | f1ocnv 6717 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})–1-1-onto→(𝑋 × 𝑌)) |
26 | 10, 25 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})–1-1-onto→(𝑋 × 𝑌)) |
27 | | f1ofo 6712 |
. . . . 5
⊢ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})–1-1-onto→(𝑋 × 𝑌) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})–onto→(𝑋 × 𝑌)) |
28 | 26, 27 | syl 17 |
. . . 4
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})–onto→(𝑋 × 𝑌)) |
29 | | ovexd 7295 |
. . . 4
⊢ (𝜑 → (𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) ∈
V) |
30 | 21 | fvexi 6775 |
. . . . . . 7
⊢ 𝐺 ∈ V |
31 | 30 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 𝐺 ∈
V) |
32 | | prex 5355 |
. . . . . . 7
⊢
{〈∅, 𝑅〉, 〈1o, 𝑆〉} ∈
V |
33 | 32 | a1i 11 |
. . . . . 6
⊢ (⊤
→ {〈∅, 𝑅〉, 〈1o, 𝑆〉} ∈
V) |
34 | 22, 31, 33 | prdssca 17111 |
. . . . 5
⊢ (⊤
→ 𝐺 =
(Scalar‘(𝐺Xs{〈∅, 𝑅〉, 〈1o,
𝑆〉}))) |
35 | 34 | mptru 1546 |
. . . 4
⊢ 𝐺 = (Scalar‘(𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) |
36 | | xpsvsca.k |
. . . 4
⊢ 𝐾 = (Base‘𝐺) |
37 | | eqid 2737 |
. . . 4
⊢ (
·𝑠 ‘(𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) = (
·𝑠 ‘(𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) |
38 | | xpsvsca.p |
. . . 4
⊢ ∙ = (
·𝑠 ‘𝑇) |
39 | 26 | f1ovscpbl 17181 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ∧ 𝑐 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}))) → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘𝑏) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘𝑐) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘(𝑎(
·𝑠 ‘(𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))𝑏)) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘(𝑎(
·𝑠 ‘(𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))𝑐)))) |
40 | 23, 24, 28, 29, 35, 36, 37, 38, 39 | imasvscaval 17193 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐾 ∧ {〈∅, 𝐵〉, 〈1o, 𝐶〉} ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})) → (𝐴 ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘{〈∅,
𝐵〉,
〈1o, 𝐶〉})) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘(𝐴(
·𝑠 ‘(𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})){〈∅, 𝐵〉, 〈1o,
𝐶〉}))) |
41 | 1, 15, 40 | mpd3an23 1461 |
. 2
⊢ (𝜑 → (𝐴 ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘{〈∅,
𝐵〉,
〈1o, 𝐶〉})) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘(𝐴(
·𝑠 ‘(𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})){〈∅, 𝐵〉, 〈1o,
𝐶〉}))) |
42 | | f1ocnvfv 7136 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ∧ 〈𝐵, 𝐶〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘〈𝐵, 𝐶〉) = {〈∅, 𝐵〉, 〈1o, 𝐶〉} → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘{〈∅,
𝐵〉,
〈1o, 𝐶〉}) = 〈𝐵, 𝐶〉)) |
43 | 10, 9, 42 | sylancr 586 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘〈𝐵, 𝐶〉) = {〈∅, 𝐵〉, 〈1o, 𝐶〉} → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘{〈∅,
𝐵〉,
〈1o, 𝐶〉}) = 〈𝐵, 𝐶〉)) |
44 | 8, 43 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘{〈∅,
𝐵〉,
〈1o, 𝐶〉}) = 〈𝐵, 𝐶〉) |
45 | 44 | oveq2d 7276 |
. 2
⊢ (𝜑 → (𝐴 ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘{〈∅,
𝐵〉,
〈1o, 𝐶〉})) = (𝐴 ∙ 〈𝐵, 𝐶〉)) |
46 | | iftrue 4467 |
. . . . . . . . . . . 12
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑅) |
47 | 46 | fveq2d 6765 |
. . . . . . . . . . 11
⊢ (𝑘 = ∅ → (
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = ( ·𝑠
‘𝑅)) |
48 | | xpsvsca.m |
. . . . . . . . . . 11
⊢ · = (
·𝑠 ‘𝑅) |
49 | 47, 48 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → (
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = · ) |
50 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → 𝐴 = 𝐴) |
51 | | iftrue 4467 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝐵, 𝐶) = 𝐵) |
52 | 49, 50, 51 | oveq123d 7281 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = (𝐴 · 𝐵)) |
53 | | iftrue 4467 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) = (𝐴 · 𝐵)) |
54 | 52, 53 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝑘 = ∅ → (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))) |
55 | | iffalse 4470 |
. . . . . . . . . . . 12
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑆) |
56 | 55 | fveq2d 6765 |
. . . . . . . . . . 11
⊢ (¬
𝑘 = ∅ → (
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = ( ·𝑠
‘𝑆)) |
57 | | xpsvsca.n |
. . . . . . . . . . 11
⊢ × = (
·𝑠 ‘𝑆) |
58 | 56, 57 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → (
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = × ) |
59 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → 𝐴 = 𝐴) |
60 | | iffalse 4470 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, 𝐵, 𝐶) = 𝐶) |
61 | 58, 59, 60 | oveq123d 7281 |
. . . . . . . . 9
⊢ (¬
𝑘 = ∅ → (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = (𝐴 × 𝐶)) |
62 | | iffalse 4470 |
. . . . . . . . 9
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) = (𝐴 × 𝐶)) |
63 | 61, 62 | eqtr4d 2780 |
. . . . . . . 8
⊢ (¬
𝑘 = ∅ → (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))) |
64 | 54, 63 | pm2.61i 182 |
. . . . . . 7
⊢ (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) |
65 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝑅 ∈ 𝑉) |
66 | 20 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝑆 ∈ 𝑊) |
67 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝑘 ∈
2o) |
68 | | fvprif 17216 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝑘 ∈ 2o) →
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆)) |
69 | 65, 66, 67, 68 | syl3anc 1369 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) →
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆)) |
70 | 69 | fveq2d 6765 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (
·𝑠 ‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) = ( ·𝑠
‘if(𝑘 = ∅,
𝑅, 𝑆))) |
71 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝐴 = 𝐴) |
72 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝐵 ∈ 𝑋) |
73 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝐶 ∈ 𝑌) |
74 | | fvprif 17216 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ 𝑘 ∈ 2o) →
({〈∅, 𝐵〉,
〈1o, 𝐶〉}‘𝑘) = if(𝑘 = ∅, 𝐵, 𝐶)) |
75 | 72, 73, 67, 74 | syl3anc 1369 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) →
({〈∅, 𝐵〉,
〈1o, 𝐶〉}‘𝑘) = if(𝑘 = ∅, 𝐵, 𝐶)) |
76 | 70, 71, 75 | oveq123d 7281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (𝐴(
·𝑠 ‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘))({〈∅, 𝐵〉, 〈1o, 𝐶〉}‘𝑘)) = (𝐴( ·𝑠
‘if(𝑘 = ∅,
𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶))) |
77 | | xpsvsca.6 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑋) |
78 | 77 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (𝐴 · 𝐵) ∈ 𝑋) |
79 | | xpsvsca.7 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 × 𝐶) ∈ 𝑌) |
80 | 79 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (𝐴 × 𝐶) ∈ 𝑌) |
81 | | fvprif 17216 |
. . . . . . . 8
⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌 ∧ 𝑘 ∈ 2o) →
({〈∅, (𝐴 · 𝐵)〉, 〈1o,
(𝐴 × 𝐶)〉}‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))) |
82 | 78, 80, 67, 81 | syl3anc 1369 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) →
({〈∅, (𝐴 · 𝐵)〉, 〈1o,
(𝐴 × 𝐶)〉}‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))) |
83 | 64, 76, 82 | 3eqtr4a 2803 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (𝐴(
·𝑠 ‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘))({〈∅, 𝐵〉, 〈1o, 𝐶〉}‘𝑘)) = ({〈∅, (𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉}‘𝑘)) |
84 | 83 | mpteq2dva 5175 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 2o ↦ (𝐴(
·𝑠 ‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘))({〈∅, 𝐵〉, 〈1o, 𝐶〉}‘𝑘))) = (𝑘 ∈ 2o ↦
({〈∅, (𝐴 · 𝐵)〉, 〈1o,
(𝐴 × 𝐶)〉}‘𝑘))) |
85 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(𝐺Xs{〈∅, 𝑅〉, 〈1o,
𝑆〉})) =
(Base‘(𝐺Xs{〈∅, 𝑅〉, 〈1o,
𝑆〉})) |
86 | 30 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ V) |
87 | | 2on 8280 |
. . . . . . 7
⊢
2o ∈ On |
88 | 87 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2o ∈
On) |
89 | | fnpr2o 17212 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → {〈∅, 𝑅〉, 〈1o, 𝑆〉} Fn
2o) |
90 | 19, 20, 89 | syl2anc 583 |
. . . . . 6
⊢ (𝜑 → {〈∅, 𝑅〉, 〈1o,
𝑆〉} Fn
2o) |
91 | 15, 24 | eleqtrd 2839 |
. . . . . 6
⊢ (𝜑 → {〈∅, 𝐵〉, 〈1o,
𝐶〉} ∈
(Base‘(𝐺Xs{〈∅, 𝑅〉, 〈1o,
𝑆〉}))) |
92 | 22, 85, 37, 36, 86, 88, 90, 1, 91 | prdsvscaval 17134 |
. . . . 5
⊢ (𝜑 → (𝐴( ·𝑠
‘(𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})){〈∅, 𝐵〉, 〈1o,
𝐶〉}) = (𝑘 ∈ 2o ↦
(𝐴(
·𝑠 ‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘))({〈∅, 𝐵〉, 〈1o, 𝐶〉}‘𝑘)))) |
93 | | fnpr2o 17212 |
. . . . . . 7
⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → {〈∅, (𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉} Fn 2o) |
94 | 77, 79, 93 | syl2anc 583 |
. . . . . 6
⊢ (𝜑 → {〈∅, (𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉} Fn 2o) |
95 | | dffn5 6815 |
. . . . . 6
⊢
({〈∅, (𝐴
·
𝐵)〉,
〈1o, (𝐴
×
𝐶)〉} Fn 2o
↔ {〈∅, (𝐴
·
𝐵)〉,
〈1o, (𝐴
×
𝐶)〉} = (𝑘 ∈ 2o ↦
({〈∅, (𝐴 · 𝐵)〉, 〈1o,
(𝐴 × 𝐶)〉}‘𝑘))) |
96 | 94, 95 | sylib 217 |
. . . . 5
⊢ (𝜑 → {〈∅, (𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉} = (𝑘 ∈ 2o ↦
({〈∅, (𝐴 · 𝐵)〉, 〈1o,
(𝐴 × 𝐶)〉}‘𝑘))) |
97 | 84, 92, 96 | 3eqtr4d 2787 |
. . . 4
⊢ (𝜑 → (𝐴( ·𝑠
‘(𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})){〈∅, 𝐵〉, 〈1o,
𝐶〉}) = {〈∅,
(𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉}) |
98 | 97 | fveq2d 6765 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘(𝐴(
·𝑠 ‘(𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})){〈∅, 𝐵〉, 〈1o,
𝐶〉})) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘{〈∅,
(𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉})) |
99 | | df-ov 7263 |
. . . . 5
⊢ ((𝐴 · 𝐵)(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})(𝐴 × 𝐶)) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) |
100 | 5 | xpsfval 17221 |
. . . . . 6
⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → ((𝐴 · 𝐵)(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})(𝐴 × 𝐶)) = {〈∅, (𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉}) |
101 | 77, 79, 100 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → ((𝐴 · 𝐵)(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})(𝐴 × 𝐶)) = {〈∅, (𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉}) |
102 | 99, 101 | eqtr3id 2791 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) = {〈∅, (𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉}) |
103 | 77, 79 | opelxpd 5623 |
. . . . 5
⊢ (𝜑 → 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉 ∈ (𝑋 × 𝑌)) |
104 | | f1ocnvfv 7136 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ∧ 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) = {〈∅, (𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉} → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘{〈∅,
(𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉}) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉)) |
105 | 10, 103, 104 | sylancr 586 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) = {〈∅, (𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉} → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘{〈∅,
(𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉}) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉)) |
106 | 102, 105 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘{〈∅,
(𝐴 · 𝐵)〉, 〈1o, (𝐴 × 𝐶)〉}) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) |
107 | 98, 106 | eqtrd 2777 |
. 2
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘(𝐴(
·𝑠 ‘(𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})){〈∅, 𝐵〉, 〈1o,
𝐶〉})) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) |
108 | 41, 45, 107 | 3eqtr3d 2785 |
1
⊢ (𝜑 → (𝐴 ∙ 〈𝐵, 𝐶〉) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) |