Proof of Theorem xpsaddlem
Step | Hyp | Ref
| Expression |
1 | | df-ov 6653 |
. . . . 5
⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) |
2 | | xpsadd.3 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
3 | | xpsadd.4 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑌) |
4 | | xpsaddlem.f |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
5 | 4 | xpsfval 16227 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴𝐹𝐵) = ◡({𝐴} +𝑐 {𝐵})) |
6 | 2, 3, 5 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐴𝐹𝐵) = ◡({𝐴} +𝑐 {𝐵})) |
7 | 1, 6 | syl5eqr 2670 |
. . . 4
⊢ (𝜑 → (𝐹‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵})) |
8 | | opelxpi 5148 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
9 | 2, 3, 8 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
10 | 4 | xpsff1o2 16231 |
. . . . . . 7
⊢ 𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 |
11 | | f1of 6137 |
. . . . . . 7
⊢ (𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 → 𝐹:(𝑋 × 𝑌)⟶ran 𝐹) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢ 𝐹:(𝑋 × 𝑌)⟶ran 𝐹 |
13 | 12 | ffvelrni 6358 |
. . . . 5
⊢
(〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌) → (𝐹‘〈𝐴, 𝐵〉) ∈ ran 𝐹) |
14 | 9, 13 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹‘〈𝐴, 𝐵〉) ∈ ran 𝐹) |
15 | 7, 14 | eqeltrrd 2702 |
. . 3
⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ ran 𝐹) |
16 | | df-ov 6653 |
. . . . 5
⊢ (𝐶𝐹𝐷) = (𝐹‘〈𝐶, 𝐷〉) |
17 | | xpsadd.5 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
18 | | xpsadd.6 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑌) |
19 | 4 | xpsfval 16227 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → (𝐶𝐹𝐷) = ◡({𝐶} +𝑐 {𝐷})) |
20 | 17, 18, 19 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐶𝐹𝐷) = ◡({𝐶} +𝑐 {𝐷})) |
21 | 16, 20 | syl5eqr 2670 |
. . . 4
⊢ (𝜑 → (𝐹‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷})) |
22 | | opelxpi 5148 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
23 | 17, 18, 22 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
24 | 12 | ffvelrni 6358 |
. . . . 5
⊢
(〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌) → (𝐹‘〈𝐶, 𝐷〉) ∈ ran 𝐹) |
25 | 23, 24 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹‘〈𝐶, 𝐷〉) ∈ ran 𝐹) |
26 | 21, 25 | eqeltrrd 2702 |
. . 3
⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ ran 𝐹) |
27 | | xpsaddlem.1 |
. . 3
⊢ ((𝜑 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ ran 𝐹 ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ ran 𝐹) → ((◡𝐹‘◡({𝐴} +𝑐 {𝐵})) ∙ (◡𝐹‘◡({𝐶} +𝑐 {𝐷}))) = (◡𝐹‘(◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷})))) |
28 | 15, 26, 27 | mpd3an23 1426 |
. 2
⊢ (𝜑 → ((◡𝐹‘◡({𝐴} +𝑐 {𝐵})) ∙ (◡𝐹‘◡({𝐶} +𝑐 {𝐷}))) = (◡𝐹‘(◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷})))) |
29 | | f1ocnvfv 6534 |
. . . . 5
⊢ ((𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 ∧ 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) → ((𝐹‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵}) → (◡𝐹‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉)) |
30 | 10, 9, 29 | sylancr 695 |
. . . 4
⊢ (𝜑 → ((𝐹‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵}) → (◡𝐹‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉)) |
31 | 7, 30 | mpd 15 |
. . 3
⊢ (𝜑 → (◡𝐹‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉) |
32 | | f1ocnvfv 6534 |
. . . . 5
⊢ ((𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 ∧ 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) → ((𝐹‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷}) → (◡𝐹‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉)) |
33 | 10, 23, 32 | sylancr 695 |
. . . 4
⊢ (𝜑 → ((𝐹‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷}) → (◡𝐹‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉)) |
34 | 21, 33 | mpd 15 |
. . 3
⊢ (𝜑 → (◡𝐹‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉) |
35 | 31, 34 | oveq12d 6668 |
. 2
⊢ (𝜑 → ((◡𝐹‘◡({𝐴} +𝑐 {𝐵})) ∙ (◡𝐹‘◡({𝐶} +𝑐 {𝐷}))) = (〈𝐴, 𝐵〉 ∙ 〈𝐶, 𝐷〉)) |
36 | | xpsval.1 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
37 | | xpsval.2 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
38 | | xpscfn 16219 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
39 | 36, 37, 38 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
40 | | xpsval.t |
. . . . . . . 8
⊢ 𝑇 = (𝑅 ×s 𝑆) |
41 | | xpsval.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝑅) |
42 | | xpsval.y |
. . . . . . . 8
⊢ 𝑌 = (Base‘𝑆) |
43 | | eqid 2622 |
. . . . . . . 8
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
44 | | xpsaddlem.u |
. . . . . . . 8
⊢ 𝑈 = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) |
45 | 40, 41, 42, 36, 37, 4, 43, 44 | xpslem 16233 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 = (Base‘𝑈)) |
46 | 15, 45 | eleqtrd 2703 |
. . . . . 6
⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘𝑈)) |
47 | 26, 45 | eleqtrd 2703 |
. . . . . 6
⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘𝑈)) |
48 | | xpsaddlem.2 |
. . . . . 6
⊢ ((◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘𝑈) ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘𝑈)) → (◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷})) = (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))) |
49 | 39, 46, 47, 48 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷})) = (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))) |
50 | | xpsadd.7 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 · 𝐶) ∈ 𝑋) |
51 | | xpsadd.8 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 × 𝐷) ∈ 𝑌) |
52 | | xpscfn 16219 |
. . . . . . . 8
⊢ (((𝐴 · 𝐶) ∈ 𝑋 ∧ (𝐵 × 𝐷) ∈ 𝑌) → ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) Fn
2𝑜) |
53 | 50, 51, 52 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) Fn
2𝑜) |
54 | | dffn5 6241 |
. . . . . . 7
⊢ (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) Fn 2𝑜 ↔ ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) = (𝑘 ∈ 2𝑜 ↦ (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})‘𝑘))) |
55 | 53, 54 | sylib 208 |
. . . . . 6
⊢ (𝜑 → ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) = (𝑘 ∈ 2𝑜 ↦ (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})‘𝑘))) |
56 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑅) |
57 | 56 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑘 = ∅ → (𝐸‘if(𝑘 = ∅, 𝑅, 𝑆)) = (𝐸‘𝑅)) |
58 | | xpsaddlem.m |
. . . . . . . . . . . 12
⊢ · =
(𝐸‘𝑅) |
59 | 57, 58 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (𝑘 = ∅ → (𝐸‘if(𝑘 = ∅, 𝑅, 𝑆)) = · ) |
60 | | iftrue 4092 |
. . . . . . . . . . 11
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐴) |
61 | | iftrue 4092 |
. . . . . . . . . . 11
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝐶, 𝐷) = 𝐶) |
62 | 59, 60, 61 | oveq123d 6671 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → (if(𝑘 = ∅, 𝐴, 𝐵)(𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐶, 𝐷)) = (𝐴 · 𝐶)) |
63 | | iftrue 4092 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷)) = (𝐴 · 𝐶)) |
64 | 62, 63 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → (if(𝑘 = ∅, 𝐴, 𝐵)(𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐶, 𝐷)) = if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷))) |
65 | | iffalse 4095 |
. . . . . . . . . . . . 13
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑆) |
66 | 65 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (¬
𝑘 = ∅ → (𝐸‘if(𝑘 = ∅, 𝑅, 𝑆)) = (𝐸‘𝑆)) |
67 | | xpsaddlem.n |
. . . . . . . . . . . 12
⊢ × =
(𝐸‘𝑆) |
68 | 66, 67 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (¬
𝑘 = ∅ → (𝐸‘if(𝑘 = ∅, 𝑅, 𝑆)) = × ) |
69 | | iffalse 4095 |
. . . . . . . . . . 11
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐵) |
70 | | iffalse 4095 |
. . . . . . . . . . 11
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, 𝐶, 𝐷) = 𝐷) |
71 | 68, 69, 70 | oveq123d 6671 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ →
(if(𝑘 = ∅, 𝐴, 𝐵)(𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐶, 𝐷)) = (𝐵 × 𝐷)) |
72 | | iffalse 4095 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷)) = (𝐵 × 𝐷)) |
73 | 71, 72 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (¬
𝑘 = ∅ →
(if(𝑘 = ∅, 𝐴, 𝐵)(𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐶, 𝐷)) = if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷))) |
74 | 64, 73 | pm2.61i 176 |
. . . . . . . 8
⊢ (if(𝑘 = ∅, 𝐴, 𝐵)(𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐶, 𝐷)) = if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷)) |
75 | 36 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝑅 ∈ 𝑉) |
76 | 37 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝑆 ∈ 𝑊) |
77 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝑘 ∈
2𝑜) |
78 | | xpscfv 16222 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝑘 ∈ 2𝑜) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆)) |
79 | 75, 76, 77, 78 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆)) |
80 | 79 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))) |
81 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐴 ∈ 𝑋) |
82 | 3 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐵 ∈ 𝑌) |
83 | | xpscfv 16222 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑘 ∈ 2𝑜) → (◡({𝐴} +𝑐 {𝐵})‘𝑘) = if(𝑘 = ∅, 𝐴, 𝐵)) |
84 | 81, 82, 77, 83 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({𝐴} +𝑐 {𝐵})‘𝑘) = if(𝑘 = ∅, 𝐴, 𝐵)) |
85 | 17 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐶 ∈ 𝑋) |
86 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → 𝐷 ∈ 𝑌) |
87 | | xpscfv 16222 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ∧ 𝑘 ∈ 2𝑜) → (◡({𝐶} +𝑐 {𝐷})‘𝑘) = if(𝑘 = ∅, 𝐶, 𝐷)) |
88 | 85, 86, 77, 87 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({𝐶} +𝑐 {𝐷})‘𝑘) = if(𝑘 = ∅, 𝐶, 𝐷)) |
89 | 80, 84, 88 | oveq123d 6671 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) = (if(𝑘 = ∅, 𝐴, 𝐵)(𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐶, 𝐷))) |
90 | 50 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐴 · 𝐶) ∈ 𝑋) |
91 | 51 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (𝐵 × 𝐷) ∈ 𝑌) |
92 | | xpscfv 16222 |
. . . . . . . . 9
⊢ (((𝐴 · 𝐶) ∈ 𝑋 ∧ (𝐵 × 𝐷) ∈ 𝑌 ∧ 𝑘 ∈ 2𝑜) → (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷))) |
93 | 90, 91, 77, 92 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷))) |
94 | 74, 89, 93 | 3eqtr4a 2682 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) = (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})‘𝑘)) |
95 | 94 | mpteq2dva 4744 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) = (𝑘 ∈ 2𝑜 ↦ (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})‘𝑘))) |
96 | 55, 95 | eqtr4d 2659 |
. . . . 5
⊢ (𝜑 → ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) = (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))) |
97 | 49, 96 | eqtr4d 2659 |
. . . 4
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷})) = ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) |
98 | 97 | fveq2d 6195 |
. . 3
⊢ (𝜑 → (◡𝐹‘(◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷}))) = (◡𝐹‘◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}))) |
99 | | df-ov 6653 |
. . . . 5
⊢ ((𝐴 · 𝐶)𝐹(𝐵 × 𝐷)) = (𝐹‘〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) |
100 | 4 | xpsfval 16227 |
. . . . . 6
⊢ (((𝐴 · 𝐶) ∈ 𝑋 ∧ (𝐵 × 𝐷) ∈ 𝑌) → ((𝐴 · 𝐶)𝐹(𝐵 × 𝐷)) = ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) |
101 | 50, 51, 100 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((𝐴 · 𝐶)𝐹(𝐵 × 𝐷)) = ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) |
102 | 99, 101 | syl5eqr 2670 |
. . . 4
⊢ (𝜑 → (𝐹‘〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) = ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) |
103 | | opelxpi 5148 |
. . . . . 6
⊢ (((𝐴 · 𝐶) ∈ 𝑋 ∧ (𝐵 × 𝐷) ∈ 𝑌) → 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉 ∈ (𝑋 × 𝑌)) |
104 | 50, 51, 103 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉 ∈ (𝑋 × 𝑌)) |
105 | | f1ocnvfv 6534 |
. . . . 5
⊢ ((𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 ∧ 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉 ∈ (𝑋 × 𝑌)) → ((𝐹‘〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) = ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) → (◡𝐹‘◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉)) |
106 | 10, 104, 105 | sylancr 695 |
. . . 4
⊢ (𝜑 → ((𝐹‘〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) = ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) → (◡𝐹‘◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉)) |
107 | 102, 106 | mpd 15 |
. . 3
⊢ (𝜑 → (◡𝐹‘◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) |
108 | 98, 107 | eqtrd 2656 |
. 2
⊢ (𝜑 → (◡𝐹‘(◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷}))) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) |
109 | 28, 35, 108 | 3eqtr3d 2664 |
1
⊢ (𝜑 → (〈𝐴, 𝐵〉 ∙ 〈𝐶, 𝐷〉) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) |