Step | Hyp | Ref
| Expression |
1 | | xpsvsca.3 |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝐾) |
2 | | df-ov 6653 |
. . . . 5
⊢ (𝐵(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐶) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐵, 𝐶〉) |
3 | | xpsvsca.4 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑋) |
4 | | xpsvsca.5 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑌) |
5 | | eqid 2622 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
6 | 5 | xpsfval 16227 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌) → (𝐵(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐶) = ◡({𝐵} +𝑐 {𝐶})) |
7 | 3, 4, 6 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐵(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐶) = ◡({𝐵} +𝑐 {𝐶})) |
8 | 2, 7 | syl5eqr 2670 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐵, 𝐶〉) = ◡({𝐵} +𝑐 {𝐶})) |
9 | | opelxpi 5148 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌) → 〈𝐵, 𝐶〉 ∈ (𝑋 × 𝑌)) |
10 | 3, 4, 9 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 〈𝐵, 𝐶〉 ∈ (𝑋 × 𝑌)) |
11 | 5 | xpsff1o2 16231 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
12 | | f1of 6137 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
13 | 11, 12 | ax-mp 5 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
14 | 13 | ffvelrni 6358 |
. . . . 5
⊢
(〈𝐵, 𝐶〉 ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐵, 𝐶〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
15 | 10, 14 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐵, 𝐶〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
16 | 8, 15 | eqeltrrd 2702 |
. . 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 2622 |
. . . . 5
⊢ (𝐺Xs◡({𝑅} +𝑐 {𝑆})) = (𝐺Xs◡({𝑅} +𝑐 {𝑆})) |
24 | 17, 18, 19, 20, 21, 5, 22, 23 | xpsval 16232 |
. . . 4
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) “s (𝐺Xs◡({𝑅} +𝑐 {𝑆})))) |
25 | 17, 18, 19, 20, 21, 5, 22, 23 | xpslem 16233 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))) |
26 | | f1ocnv 6149 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
27 | 11, 26 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
28 | | f1ofo 6144 |
. . . . 5
⊢ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌)) |
29 | 27, 28 | syl 17 |
. . . 4
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌)) |
30 | | ovexd 6680 |
. . . 4
⊢ (𝜑 → (𝐺Xs◡({𝑅} +𝑐 {𝑆})) ∈ V) |
31 | | fvex 6201 |
. . . . . . . 8
⊢
(Scalar‘𝑅)
∈ V |
32 | 22, 31 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐺 ∈ V |
33 | 32 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 𝐺 ∈
V) |
34 | | ovex 6678 |
. . . . . . . 8
⊢ ({𝑅} +𝑐 {𝑆}) ∈ V |
35 | 34 | cnvex 7113 |
. . . . . . 7
⊢ ◡({𝑅} +𝑐 {𝑆}) ∈ V |
36 | 35 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ◡({𝑅} +𝑐 {𝑆}) ∈ V) |
37 | 23, 33, 36 | prdssca 16116 |
. . . . 5
⊢ (⊤
→ 𝐺 =
(Scalar‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))) |
38 | 37 | trud 1493 |
. . . 4
⊢ 𝐺 = (Scalar‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))) |
39 | | xpsvsca.k |
. . . 4
⊢ 𝐾 = (Base‘𝐺) |
40 | | eqid 2622 |
. . . 4
⊢ (
·𝑠 ‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))) = ( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))) |
41 | | xpsvsca.p |
. . . 4
⊢ ∙ = (
·𝑠 ‘𝑇) |
42 | 27 | f1ovscpbl 16186 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 𝑐 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑏) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑐) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝑎( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))𝑏)) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝑎( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))𝑐)))) |
43 | 24, 25, 29, 30, 38, 39, 40, 41, 42 | imasvscaval 16198 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐾 ∧ ◡({𝐵} +𝑐 {𝐶}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) → (𝐴 ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶}))) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶})))) |
44 | 1, 16, 43 | mpd3an23 1426 |
. 2
⊢ (𝜑 → (𝐴 ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶}))) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶})))) |
45 | | f1ocnvfv 6534 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 〈𝐵, 𝐶〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐵, 𝐶〉) = ◡({𝐵} +𝑐 {𝐶}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶})) = 〈𝐵, 𝐶〉)) |
46 | 11, 10, 45 | sylancr 695 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐵, 𝐶〉) = ◡({𝐵} +𝑐 {𝐶}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶})) = 〈𝐵, 𝐶〉)) |
47 | 8, 46 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶})) = 〈𝐵, 𝐶〉) |
48 | 47 | oveq2d 6666 |
. 2
⊢ (𝜑 → (𝐴 ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐵} +𝑐 {𝐶}))) = (𝐴 ∙ 〈𝐵, 𝐶〉)) |
49 | | iftrue 4092 |
. . . . . . . . . . . 12
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑅) |
50 | 49 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑘 = ∅ → (
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = ( ·𝑠
‘𝑅)) |
51 | | xpsvsca.m |
. . . . . . . . . . 11
⊢ · = (
·𝑠 ‘𝑅) |
52 | 50, 51 | syl6eqr 2674 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → (
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = · ) |
53 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → 𝐴 = 𝐴) |
54 | | iftrue 4092 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝐵, 𝐶) = 𝐵) |
55 | 52, 53, 54 | oveq123d 6671 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = (𝐴 · 𝐵)) |
56 | | iftrue 4092 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) = (𝐴 · 𝐵)) |
57 | 55, 56 | eqtr4d 2659 |
. . . . . . . 8
⊢ (𝑘 = ∅ → (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))) |
58 | | iffalse 4095 |
. . . . . . . . . . . 12
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑆) |
59 | 58 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (¬
𝑘 = ∅ → (
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = ( ·𝑠
‘𝑆)) |
60 | | xpsvsca.n |
. . . . . . . . . . 11
⊢ × = (
·𝑠 ‘𝑆) |
61 | 59, 60 | syl6eqr 2674 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → (
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆)) = × ) |
62 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → 𝐴 = 𝐴) |
63 | | iffalse 4095 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, 𝐵, 𝐶) = 𝐶) |
64 | 61, 62, 63 | oveq123d 6671 |
. . . . . . . . 9
⊢ (¬
𝑘 = ∅ → (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = (𝐴 × 𝐶)) |
65 | | iffalse 4095 |
. . . . . . . . 9
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) = (𝐴 × 𝐶)) |
66 | 64, 65 | eqtr4d 2659 |
. . . . . . . 8
⊢ (¬
𝑘 = ∅ → (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))) |
67 | 57, 66 | pm2.61i 176 |
. . . . . . 7
⊢ (𝐴(
·𝑠 ‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶)) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶)) |
68 | 20 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝑅 ∈ 𝑉) |
69 | 21 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝑆 ∈ 𝑊) |
70 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝑘 ∈
2𝑜) |
71 | | xpscfv 16222 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝑘 ∈ 2𝑜) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆)) |
72 | 68, 69, 70, 71 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆)) |
73 | 72 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (
·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = ( ·𝑠
‘if(𝑘 = ∅,
𝑅, 𝑆))) |
74 | | eqidd 2623 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐴 = 𝐴) |
75 | 3 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐵 ∈ 𝑋) |
76 | 4 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐶 ∈ 𝑌) |
77 | | xpscfv 16222 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ 𝑘 ∈ 2𝑜) → (◡({𝐵} +𝑐 {𝐶})‘𝑘) = if(𝑘 = ∅, 𝐵, 𝐶)) |
78 | 75, 76, 70, 77 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({𝐵} +𝑐 {𝐶})‘𝑘) = if(𝑘 = ∅, 𝐵, 𝐶)) |
79 | 73, 74, 78 | oveq123d 6671 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴(
·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐵} +𝑐 {𝐶})‘𝑘)) = (𝐴( ·𝑠
‘if(𝑘 = ∅,
𝑅, 𝑆))if(𝑘 = ∅, 𝐵, 𝐶))) |
80 | | xpsvsca.6 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑋) |
81 | 80 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴 · 𝐵) ∈ 𝑋) |
82 | | xpsvsca.7 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 × 𝐶) ∈ 𝑌) |
83 | 82 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴 × 𝐶) ∈ 𝑌) |
84 | | xpscfv 16222 |
. . . . . . . 8
⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌 ∧ 𝑘 ∈ 2𝑜) → (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))) |
85 | 81, 83, 70, 84 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐵), (𝐴 × 𝐶))) |
86 | 67, 79, 85 | 3eqtr4a 2682 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴(
·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐵} +𝑐 {𝐶})‘𝑘)) = (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘)) |
87 | 86 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 2𝑜 ↦ (𝐴(
·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐵} +𝑐 {𝐶})‘𝑘))) = (𝑘 ∈ 2𝑜 ↦ (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘))) |
88 | | eqid 2622 |
. . . . . 6
⊢
(Base‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘(𝐺Xs◡({𝑅} +𝑐 {𝑆}))) |
89 | 32 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ V) |
90 | | 2on 7568 |
. . . . . . 7
⊢
2𝑜 ∈ On |
91 | 90 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2𝑜
∈ On) |
92 | | xpscfn 16219 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
93 | 20, 21, 92 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
94 | 16, 25 | eleqtrd 2703 |
. . . . . 6
⊢ (𝜑 → ◡({𝐵} +𝑐 {𝐶}) ∈ (Base‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))) |
95 | 23, 88, 40, 39, 89, 91, 93, 1, 94 | prdsvscaval 16139 |
. . . . 5
⊢ (𝜑 → (𝐴( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶})) = (𝑘 ∈ 2𝑜 ↦ (𝐴(
·𝑠 ‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐵} +𝑐 {𝐶})‘𝑘)))) |
96 | | xpscfn 16219 |
. . . . . . 7
⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) Fn
2𝑜) |
97 | 80, 82, 96 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) Fn
2𝑜) |
98 | | dffn5 6241 |
. . . . . 6
⊢ (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) Fn 2𝑜 ↔ ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) = (𝑘 ∈ 2𝑜 ↦ (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘))) |
99 | 97, 98 | sylib 208 |
. . . . 5
⊢ (𝜑 → ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) = (𝑘 ∈ 2𝑜 ↦ (◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})‘𝑘))) |
100 | 87, 95, 99 | 3eqtr4d 2666 |
. . . 4
⊢ (𝜑 → (𝐴( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶})) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) |
101 | 100 | fveq2d 6195 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶}))) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}))) |
102 | | df-ov 6653 |
. . . . 5
⊢ ((𝐴 · 𝐵)(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))(𝐴 × 𝐶)) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) |
103 | 5 | xpsfval 16227 |
. . . . . 6
⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → ((𝐴 · 𝐵)(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))(𝐴 × 𝐶)) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) |
104 | 80, 82, 103 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((𝐴 · 𝐵)(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))(𝐴 × 𝐶)) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) |
105 | 102, 104 | syl5eqr 2670 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) |
106 | | opelxpi 5148 |
. . . . . 6
⊢ (((𝐴 · 𝐵) ∈ 𝑋 ∧ (𝐴 × 𝐶) ∈ 𝑌) → 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉 ∈ (𝑋 × 𝑌)) |
107 | 80, 82, 106 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉 ∈ (𝑋 × 𝑌)) |
108 | | f1ocnvfv 6534 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉)) |
109 | 11, 107, 108 | sylancr 695 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) = ◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉)) |
110 | 105, 109 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({(𝐴 · 𝐵)} +𝑐 {(𝐴 × 𝐶)})) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) |
111 | 101, 110 | eqtrd 2656 |
. 2
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝐴( ·𝑠
‘(𝐺Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐵} +𝑐 {𝐶}))) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) |
112 | 44, 48, 111 | 3eqtr3d 2664 |
1
⊢ (𝜑 → (𝐴 ∙ 〈𝐵, 𝐶〉) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) |