Step | Hyp | Ref
| Expression |
1 | | xpsvsca.3 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝐾) |
2 | | df-ov 6552 |
. . . . 5
⊢ (𝐵(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐶) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐵, 𝐶〉) |
3 | | xpsvsca.4 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑋) |
4 | | xpsvsca.5 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑌) |
5 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
6 | 5 | xpsfval 16050 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌) → (𝐵(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐶) = ◡({𝐵} +𝑐 {𝐶})) |
7 | 3, 4, 6 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐵(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐶) = ◡({𝐵} +𝑐 {𝐶})) |
8 | 2, 7 | syl5eqr 2658 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐵, 𝐶〉) = ◡({𝐵} +𝑐 {𝐶})) |
9 | | opelxpi 5072 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌) → 〈𝐵, 𝐶〉 ∈ (𝑋 × 𝑌)) |
10 | 3, 4, 9 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 〈𝐵, 𝐶〉 ∈ (𝑋 × 𝑌)) |
11 | 5 | xpsff1o2 16054 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
12 | | f1of 6050 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
13 | 11, 12 | ax-mp 5 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
14 | 13 | ffvelrni 6266 |
. . . . 5
⊢
(〈𝐵, 𝐶〉 ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐵, 𝐶〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
15 | 10, 14 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐵, 𝐶〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
16 | 8, 15 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → ◡({𝐵} +𝑐 {𝐶}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
17 | | xpssca.t |
. . . . 5
⊢ 𝑇 = (𝑅 ×s 𝑆) |
18 | | xpsvsca.x |
. . . . 5
⊢ 𝑋 = (Base‘𝑅) |
19 | | xpsvsca.y |
. . . . 5
⊢ 𝑌 = (Base‘𝑆) |
20 | | xpssca.1 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
21 | | xpssca.2 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
22 | | xpssca.g |
. . . . 5
⊢ 𝐺 = (Scalar‘𝑅) |
23 | | eqid 2610 |
. . . . 5
⊢ (𝐺Xs◡({𝑅} +𝑐 {𝑆})) = (𝐺Xs◡({𝑅} +𝑐 {𝑆})) |
24 | 17, 18, 19, 20, 21, 5, 22, 23 | xpsval 16055 |
. . . 4
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) “s (𝐺Xs◡({𝑅} +𝑐 {𝑆})))) |
25 | 17, 18, 19, 20, 21, 5, 22, 23 | xpslem 16056 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))) |
26 | | f1ocnv 6062 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
27 | 11, 26 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
28 | | f1ofo 6057 |
. . . . 5
⊢ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌)) |
29 | 27, 28 | syl 17 |
. . . 4
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌)) |
30 | | ovex 6577 |
. . . . 5
⊢ (𝐺Xs◡({𝑅} +𝑐 {𝑆})) ∈ V |
31 | 30 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐺Xs◡({𝑅} +𝑐 {𝑆})) ∈ V) |
32 | | fvex 6113 |
. . . . . . . 8
⊢
(Scalar‘𝑅)
∈ V |
33 | 22, 32 | eqeltri 2684 |
. . . . . . 7
⊢ 𝐺 ∈ V |
34 | 33 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 𝐺 ∈
V) |
35 | | ovex 6577 |
. . . . . . . 8
⊢ ({𝑅} +𝑐 {𝑆}) ∈ V |
36 | 35 | cnvex 7006 |
. . . . . . 7
⊢ ◡({𝑅} +𝑐 {𝑆}) ∈ V |
37 | 36 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ◡({𝑅} +𝑐 {𝑆}) ∈ V) |
38 | 23, 34, 37 | prdssca 15939 |
. . . . 5
⊢ (⊤
→ 𝐺 =
(Scalar‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))) |
39 | 38 | trud 1484 |
. . . 4
⊢ 𝐺 = (Scalar‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))) |
40 | | xpsvsca.k |
. . . 4
⊢ 𝐾 = (Base‘𝐺) |
41 | | eqid 2610 |
. . . 4
⊢ (
·𝑠 ‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))) = ( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))) |
42 | | xpsvsca.p |
. . . 4
⊢ ∙ = (
·𝑠 ‘𝑇) |
43 | 27 | f1ovscpbl 16009 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 𝑐 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑏) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑐) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝑎( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))𝑏)) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝑎( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))𝑐)))) |
44 | 24, 25, 29, 31, 39, 40, 41, 42, 43 | imasvscaval 16021 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐾 ∧ ◡({𝐵} +𝑐 {𝐶}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) → (𝐴 ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶}))) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶})))) |
45 | 1, 16, 44 | mpd3an23 1418 |
. 2
⊢ (𝜑 → (𝐴 ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶}))) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶})))) |
46 | | f1ocnvfv 6434 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 〈𝐵, 𝐶〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐵, 𝐶〉) = ◡({𝐵} +𝑐 {𝐶}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶})) = 〈𝐵, 𝐶〉)) |
47 | 11, 10, 46 | sylancr 694 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐵, 𝐶〉) = ◡({𝐵} +𝑐 {𝐶}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶})) = 〈𝐵, 𝐶〉)) |
48 | 8, 47 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶})) = 〈𝐵, 𝐶〉) |
49 | 48 | oveq2d 6565 |
. 2
⊢ (𝜑 → (𝐴 ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶}))) = (𝐴 ∙ 〈𝐵, 𝐶〉)) |
50 | | iftrue 4042 |
. . . . . . . . . . . 12
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑅) |
51 | 50 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑘 = ∅ → (
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = ( ·𝑠
‘𝑅)) |
52 | | xpsvsca.m |
. . . . . . . . . . 11
⊢ · = (
·𝑠 ‘𝑅) |
53 | 51, 52 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → (
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = · ) |
54 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → 𝐴 = 𝐴) |
55 | | iftrue 4042 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝐵, 𝐶) = 𝐵) |
56 | 53, 54, 55 | oveq123d 6570 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = (𝐴 · 𝐵)) |
57 | | iftrue 4042 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) = (𝐴 · 𝐵)) |
58 | 56, 57 | eqtr4d 2647 |
. . . . . . . 8
⊢ (𝑘 = ∅ → (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))) |
59 | | iffalse 4045 |
. . . . . . . . . . . 12
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑆) |
60 | 59 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (¬
𝑘 = ∅ → (
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = ( ·𝑠
‘𝑆)) |
61 | | xpsvsca.n |
. . . . . . . . . . 11
⊢ × = (
·𝑠 ‘𝑆) |
62 | 60, 61 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → (
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = × ) |
63 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → 𝐴 = 𝐴) |
64 | | iffalse 4045 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, 𝐵, 𝐶) = 𝐶) |
65 | 62, 63, 64 | oveq123d 6570 |
. . . . . . . . 9
⊢ (¬
𝑘 = ∅ → (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = (𝐴 × 𝐶)) |
66 | | iffalse 4045 |
. . . . . . . . 9
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) = (𝐴 × 𝐶)) |
67 | 65, 66 | eqtr4d 2647 |
. . . . . . . 8
⊢ (¬
𝑘 = ∅ → (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))) |
68 | 58, 67 | pm2.61i 175 |
. . . . . . 7
⊢ (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) |
69 | 20 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝑅 ∈ 𝑉) |
70 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝑆 ∈ 𝑊) |
71 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝑘 ∈
2𝑜) |
72 | | xpscfv 16045 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝑘 ∈ 2𝑜) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆)) |
73 | 69, 70, 71, 72 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆)) |
74 | 73 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (
·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = ( ·𝑠
‘if(𝑘 = ∅,
𝑅, 𝑆))) |
75 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐴 = 𝐴) |
76 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐵 ∈ 𝑋) |
77 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐶 ∈ 𝑌) |
78 | | xpscfv 16045 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ 𝑘 ∈ 2𝑜) → (◡({𝐵} +𝑐 {𝐶})‘𝑘) = if(𝑘 = ∅, 𝐵, 𝐶)) |
79 | 76, 77, 71, 78 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({𝐵} +𝑐 {𝐶})‘𝑘) = if(𝑘 = ∅, 𝐵, 𝐶)) |
80 | 74, 75, 79 | oveq123d 6570 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴(
·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐵} +𝑐 {𝐶})‘𝑘)) = (𝐴( ·𝑠
‘if(𝑘 = ∅,
𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶))) |
81 | | xpsvsca.6 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑋) |
82 | 81 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴 · 𝐵) ∈ 𝑋) |
83 | | xpsvsca.7 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 × 𝐶) ∈ 𝑌) |
84 | 83 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴 × 𝐶) ∈ 𝑌) |
85 | | xpscfv 16045 |
. . . . . . . 8
⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌 ∧ 𝑘 ∈ 2𝑜) → (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))) |
86 | 82, 84, 71, 85 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))) |
87 | 68, 80, 86 | 3eqtr4a 2670 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴(
·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐵} +𝑐 {𝐶})‘𝑘)) = (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘)) |
88 | 87 | mpteq2dva 4672 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 2𝑜 ↦ (𝐴(
·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐵} +𝑐 {𝐶})‘𝑘))) = (𝑘 ∈ 2𝑜 ↦ (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘))) |
89 | | eqid 2610 |
. . . . . 6
⊢
(Base‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))) |
90 | 33 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ V) |
91 | | 2on 7455 |
. . . . . . 7
⊢
2𝑜 ∈ On |
92 | 91 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2𝑜
∈ On) |
93 | | xpscfn 16042 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
94 | 20, 21, 93 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
95 | 16, 25 | eleqtrd 2690 |
. . . . . 6
⊢ (𝜑 → ◡({𝐵} +𝑐 {𝐶}) ∈ (Base‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))) |
96 | 23, 89, 41, 40, 90, 92, 94, 1, 95 | prdsvscaval 15962 |
. . . . 5
⊢ (𝜑 → (𝐴( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶})) = (𝑘 ∈ 2𝑜 ↦ (𝐴(
·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐵} +𝑐 {𝐶})‘𝑘)))) |
97 | | xpscfn 16042 |
. . . . . . 7
⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) Fn
2𝑜) |
98 | 81, 83, 97 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) Fn
2𝑜) |
99 | | dffn5 6151 |
. . . . . 6
⊢ (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) Fn 2𝑜 ↔ ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) = (𝑘 ∈ 2𝑜 ↦ (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘))) |
100 | 98, 99 | sylib 207 |
. . . . 5
⊢ (𝜑 → ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) = (𝑘 ∈ 2𝑜 ↦ (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘))) |
101 | 88, 96, 100 | 3eqtr4d 2654 |
. . . 4
⊢ (𝜑 → (𝐴( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶})) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) |
102 | 101 | fveq2d 6107 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶}))) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}))) |
103 | | df-ov 6552 |
. . . . 5
⊢ ((𝐴 · 𝐵)(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))(𝐴 × 𝐶)) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) |
104 | 5 | xpsfval 16050 |
. . . . . 6
⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → ((𝐴 · 𝐵)(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))(𝐴 × 𝐶)) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) |
105 | 81, 83, 104 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝐴 · 𝐵)(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))(𝐴 × 𝐶)) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) |
106 | 103, 105 | syl5eqr 2658 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) |
107 | | opelxpi 5072 |
. . . . . 6
⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉 ∈ (𝑋 × 𝑌)) |
108 | 81, 83, 107 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉 ∈ (𝑋 × 𝑌)) |
109 | | f1ocnvfv 6434 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉)) |
110 | 11, 108, 109 | sylancr 694 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉)) |
111 | 106, 110 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) |
112 | 102, 111 | eqtrd 2644 |
. 2
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶}))) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) |
113 | 45, 49, 112 | 3eqtr3d 2652 |
1
⊢ (𝜑 → (𝐴 ∙ 〈𝐵, 𝐶〉) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) |