Proof of Theorem xpsaddlem
Step | Hyp | Ref
| Expression |
1 | | df-ov 6925 |
. . . . 5
⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) |
2 | | xpsadd.3 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
3 | | xpsadd.4 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑌) |
4 | | xpsaddlem.f |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
5 | 4 | xpsfval 16613 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴𝐹𝐵) = ◡({𝐴} +𝑐 {𝐵})) |
6 | 2, 3, 5 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → (𝐴𝐹𝐵) = ◡({𝐴} +𝑐 {𝐵})) |
7 | 1, 6 | syl5eqr 2827 |
. . . 4
⊢ (𝜑 → (𝐹‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵})) |
8 | 2, 3 | opelxpd 5393 |
. . . . 5
⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
9 | 4 | xpsff1o2 16617 |
. . . . . . 7
⊢ 𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 |
10 | | f1of 6391 |
. . . . . . 7
⊢ (𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 → 𝐹:(𝑋 × 𝑌)⟶ran 𝐹) |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
⊢ 𝐹:(𝑋 × 𝑌)⟶ran 𝐹 |
12 | 11 | ffvelrni 6622 |
. . . . 5
⊢
(〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌) → (𝐹‘〈𝐴, 𝐵〉) ∈ ran 𝐹) |
13 | 8, 12 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹‘〈𝐴, 𝐵〉) ∈ ran 𝐹) |
14 | 7, 13 | eqeltrrd 2859 |
. . 3
⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ ran 𝐹) |
15 | | df-ov 6925 |
. . . . 5
⊢ (𝐶𝐹𝐷) = (𝐹‘〈𝐶, 𝐷〉) |
16 | | xpsadd.5 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
17 | | xpsadd.6 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑌) |
18 | 4 | xpsfval 16613 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → (𝐶𝐹𝐷) = ◡({𝐶} +𝑐 {𝐷})) |
19 | 16, 17, 18 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → (𝐶𝐹𝐷) = ◡({𝐶} +𝑐 {𝐷})) |
20 | 15, 19 | syl5eqr 2827 |
. . . 4
⊢ (𝜑 → (𝐹‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷})) |
21 | 16, 17 | opelxpd 5393 |
. . . . 5
⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
22 | 11 | ffvelrni 6622 |
. . . . 5
⊢
(〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌) → (𝐹‘〈𝐶, 𝐷〉) ∈ ran 𝐹) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹‘〈𝐶, 𝐷〉) ∈ ran 𝐹) |
24 | 20, 23 | eqeltrrd 2859 |
. . 3
⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ ran 𝐹) |
25 | | xpsaddlem.1 |
. . 3
⊢ ((𝜑 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ ran 𝐹 ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ ran 𝐹) → ((◡𝐹‘◡({𝐴} +𝑐 {𝐵})) ∙ (◡𝐹‘◡({𝐶} +𝑐 {𝐷}))) = (◡𝐹‘(◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷})))) |
26 | 14, 24, 25 | mpd3an23 1536 |
. 2
⊢ (𝜑 → ((◡𝐹‘◡({𝐴} +𝑐 {𝐵})) ∙ (◡𝐹‘◡({𝐶} +𝑐 {𝐷}))) = (◡𝐹‘(◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷})))) |
27 | | f1ocnvfv 6806 |
. . . . 5
⊢ ((𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 ∧ 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) → ((𝐹‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵}) → (◡𝐹‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉)) |
28 | 9, 8, 27 | sylancr 581 |
. . . 4
⊢ (𝜑 → ((𝐹‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵}) → (◡𝐹‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉)) |
29 | 7, 28 | mpd 15 |
. . 3
⊢ (𝜑 → (◡𝐹‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉) |
30 | | f1ocnvfv 6806 |
. . . . 5
⊢ ((𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 ∧ 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) → ((𝐹‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷}) → (◡𝐹‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉)) |
31 | 9, 21, 30 | sylancr 581 |
. . . 4
⊢ (𝜑 → ((𝐹‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷}) → (◡𝐹‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉)) |
32 | 20, 31 | mpd 15 |
. . 3
⊢ (𝜑 → (◡𝐹‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉) |
33 | 29, 32 | oveq12d 6940 |
. 2
⊢ (𝜑 → ((◡𝐹‘◡({𝐴} +𝑐 {𝐵})) ∙ (◡𝐹‘◡({𝐶} +𝑐 {𝐷}))) = (〈𝐴, 𝐵〉 ∙ 〈𝐶, 𝐷〉)) |
34 | | iftrue 4312 |
. . . . . . . . . . . 12
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑅) |
35 | 34 | fveq2d 6450 |
. . . . . . . . . . 11
⊢ (𝑘 = ∅ → (𝐸‘if(𝑘 = ∅, 𝑅, 𝑆)) = (𝐸‘𝑅)) |
36 | | xpsaddlem.m |
. . . . . . . . . . 11
⊢ · =
(𝐸‘𝑅) |
37 | 35, 36 | syl6eqr 2831 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → (𝐸‘if(𝑘 = ∅, 𝑅, 𝑆)) = · ) |
38 | | iftrue 4312 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐴) |
39 | | iftrue 4312 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝐶, 𝐷) = 𝐶) |
40 | 37, 38, 39 | oveq123d 6943 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → (if(𝑘 = ∅, 𝐴, 𝐵)(𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐶, 𝐷)) = (𝐴 · 𝐶)) |
41 | | iftrue 4312 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷)) = (𝐴 · 𝐶)) |
42 | 40, 41 | eqtr4d 2816 |
. . . . . . . 8
⊢ (𝑘 = ∅ → (if(𝑘 = ∅, 𝐴, 𝐵)(𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐶, 𝐷)) = if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷))) |
43 | | iffalse 4315 |
. . . . . . . . . . . 12
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, 𝑅, 𝑆) = 𝑆) |
44 | 43 | fveq2d 6450 |
. . . . . . . . . . 11
⊢ (¬
𝑘 = ∅ → (𝐸‘if(𝑘 = ∅, 𝑅, 𝑆)) = (𝐸‘𝑆)) |
45 | | xpsaddlem.n |
. . . . . . . . . . 11
⊢ × =
(𝐸‘𝑆) |
46 | 44, 45 | syl6eqr 2831 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → (𝐸‘if(𝑘 = ∅, 𝑅, 𝑆)) = × ) |
47 | | iffalse 4315 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐵) |
48 | | iffalse 4315 |
. . . . . . . . . 10
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, 𝐶, 𝐷) = 𝐷) |
49 | 46, 47, 48 | oveq123d 6943 |
. . . . . . . . 9
⊢ (¬
𝑘 = ∅ →
(if(𝑘 = ∅, 𝐴, 𝐵)(𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐶, 𝐷)) = (𝐵 × 𝐷)) |
50 | | iffalse 4315 |
. . . . . . . . 9
⊢ (¬
𝑘 = ∅ → if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷)) = (𝐵 × 𝐷)) |
51 | 49, 50 | eqtr4d 2816 |
. . . . . . . 8
⊢ (¬
𝑘 = ∅ →
(if(𝑘 = ∅, 𝐴, 𝐵)(𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐶, 𝐷)) = if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷))) |
52 | 42, 51 | pm2.61i 177 |
. . . . . . 7
⊢ (if(𝑘 = ∅, 𝐴, 𝐵)(𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐶, 𝐷)) = if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷)) |
53 | | xpsval.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
54 | 53 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝑅 ∈ 𝑉) |
55 | | xpsval.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
56 | 55 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝑆 ∈ 𝑊) |
57 | | simpr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝑘 ∈
2o) |
58 | | xpscfv 16608 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝑘 ∈ 2o) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆)) |
59 | 54, 56, 57, 58 | syl3anc 1439 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = if(𝑘 = ∅, 𝑅, 𝑆)) |
60 | 59 | fveq2d 6450 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))) |
61 | 2 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝐴 ∈ 𝑋) |
62 | 3 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝐵 ∈ 𝑌) |
63 | | xpscfv 16608 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑘 ∈ 2o) → (◡({𝐴} +𝑐 {𝐵})‘𝑘) = if(𝑘 = ∅, 𝐴, 𝐵)) |
64 | 61, 62, 57, 63 | syl3anc 1439 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (◡({𝐴} +𝑐 {𝐵})‘𝑘) = if(𝑘 = ∅, 𝐴, 𝐵)) |
65 | 16 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝐶 ∈ 𝑋) |
66 | 17 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → 𝐷 ∈ 𝑌) |
67 | | xpscfv 16608 |
. . . . . . . . 9
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ∧ 𝑘 ∈ 2o) → (◡({𝐶} +𝑐 {𝐷})‘𝑘) = if(𝑘 = ∅, 𝐶, 𝐷)) |
68 | 65, 66, 57, 67 | syl3anc 1439 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (◡({𝐶} +𝑐 {𝐷})‘𝑘) = if(𝑘 = ∅, 𝐶, 𝐷)) |
69 | 60, 64, 68 | oveq123d 6943 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) = (if(𝑘 = ∅, 𝐴, 𝐵)(𝐸‘if(𝑘 = ∅, 𝑅, 𝑆))if(𝑘 = ∅, 𝐶, 𝐷))) |
70 | | xpsadd.7 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · 𝐶) ∈ 𝑋) |
71 | 70 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (𝐴 · 𝐶) ∈ 𝑋) |
72 | | xpsadd.8 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 × 𝐷) ∈ 𝑌) |
73 | 72 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (𝐵 × 𝐷) ∈ 𝑌) |
74 | | xpscfv 16608 |
. . . . . . . 8
⊢ (((𝐴 · 𝐶) ∈ 𝑋 ∧ (𝐵 × 𝐷) ∈ 𝑌 ∧ 𝑘 ∈ 2o) → (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷))) |
75 | 71, 73, 57, 74 | syl3anc 1439 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})‘𝑘) = if(𝑘 = ∅, (𝐴 · 𝐶), (𝐵 × 𝐷))) |
76 | 52, 69, 75 | 3eqtr4a 2839 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) = (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})‘𝑘)) |
77 | 76 | mpteq2dva 4979 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) = (𝑘 ∈ 2o ↦ (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})‘𝑘))) |
78 | | xpscfn 16605 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn 2o) |
79 | 53, 55, 78 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn 2o) |
80 | | xpsval.t |
. . . . . . . 8
⊢ 𝑇 = (𝑅 ×s 𝑆) |
81 | | xpsval.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝑅) |
82 | | xpsval.y |
. . . . . . . 8
⊢ 𝑌 = (Base‘𝑆) |
83 | | eqid 2777 |
. . . . . . . 8
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
84 | | xpsaddlem.u |
. . . . . . . 8
⊢ 𝑈 = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) |
85 | 80, 81, 82, 53, 55, 4, 83, 84 | xpslem 16619 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 = (Base‘𝑈)) |
86 | 14, 85 | eleqtrd 2860 |
. . . . . 6
⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘𝑈)) |
87 | 24, 85 | eleqtrd 2860 |
. . . . . 6
⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘𝑈)) |
88 | | xpsaddlem.2 |
. . . . . 6
⊢ ((◡({𝑅} +𝑐 {𝑆}) Fn 2o ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘𝑈) ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘𝑈)) → (◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷})) = (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))) |
89 | 79, 86, 87, 88 | syl3anc 1439 |
. . . . 5
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷})) = (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(𝐸‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))) |
90 | | xpscfn 16605 |
. . . . . . 7
⊢ (((𝐴 · 𝐶) ∈ 𝑋 ∧ (𝐵 × 𝐷) ∈ 𝑌) → ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) Fn 2o) |
91 | 70, 72, 90 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) Fn 2o) |
92 | | dffn5 6501 |
. . . . . 6
⊢ (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) Fn 2o ↔ ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) = (𝑘 ∈ 2o ↦ (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})‘𝑘))) |
93 | 91, 92 | sylib 210 |
. . . . 5
⊢ (𝜑 → ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) = (𝑘 ∈ 2o ↦ (◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})‘𝑘))) |
94 | 77, 89, 93 | 3eqtr4d 2823 |
. . . 4
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷})) = ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) |
95 | 94 | fveq2d 6450 |
. . 3
⊢ (𝜑 → (◡𝐹‘(◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷}))) = (◡𝐹‘◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}))) |
96 | | df-ov 6925 |
. . . . 5
⊢ ((𝐴 · 𝐶)𝐹(𝐵 × 𝐷)) = (𝐹‘〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) |
97 | 4 | xpsfval 16613 |
. . . . . 6
⊢ (((𝐴 · 𝐶) ∈ 𝑋 ∧ (𝐵 × 𝐷) ∈ 𝑌) → ((𝐴 · 𝐶)𝐹(𝐵 × 𝐷)) = ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) |
98 | 70, 72, 97 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → ((𝐴 · 𝐶)𝐹(𝐵 × 𝐷)) = ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) |
99 | 96, 98 | syl5eqr 2827 |
. . . 4
⊢ (𝜑 → (𝐹‘〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) = ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) |
100 | 70, 72 | opelxpd 5393 |
. . . . 5
⊢ (𝜑 → 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉 ∈ (𝑋 × 𝑌)) |
101 | | f1ocnvfv 6806 |
. . . . 5
⊢ ((𝐹:(𝑋 × 𝑌)–1-1-onto→ran
𝐹 ∧ 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉 ∈ (𝑋 × 𝑌)) → ((𝐹‘〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) = ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) → (◡𝐹‘◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉)) |
102 | 9, 100, 101 | sylancr 581 |
. . . 4
⊢ (𝜑 → ((𝐹‘〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) = ◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)}) → (◡𝐹‘◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉)) |
103 | 99, 102 | mpd 15 |
. . 3
⊢ (𝜑 → (◡𝐹‘◡({(𝐴 · 𝐶)} +𝑐 {(𝐵 × 𝐷)})) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) |
104 | 95, 103 | eqtrd 2813 |
. 2
⊢ (𝜑 → (◡𝐹‘(◡({𝐴} +𝑐 {𝐵})(𝐸‘𝑈)◡({𝐶} +𝑐 {𝐷}))) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) |
105 | 26, 33, 104 | 3eqtr3d 2821 |
1
⊢ (𝜑 → (〈𝐴, 𝐵〉 ∙ 〈𝐶, 𝐷〉) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) |