Step | Hyp | Ref
| Expression |
1 | | xpsval.t |
. 2
⊢ 𝑇 = (𝑅 ×s 𝑆) |
2 | | xpsval.x |
. 2
⊢ 𝑋 = (Base‘𝑅) |
3 | | xpsval.y |
. 2
⊢ 𝑌 = (Base‘𝑆) |
4 | | xpsval.1 |
. 2
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
5 | | xpsval.2 |
. 2
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
6 | | xpsadd.3 |
. 2
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
7 | | xpsadd.4 |
. 2
⊢ (𝜑 → 𝐵 ∈ 𝑌) |
8 | | xpsadd.5 |
. 2
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
9 | | xpsadd.6 |
. 2
⊢ (𝜑 → 𝐷 ∈ 𝑌) |
10 | | xpsadd.7 |
. 2
⊢ (𝜑 → (𝐴 · 𝐶) ∈ 𝑋) |
11 | | xpsadd.8 |
. 2
⊢ (𝜑 → (𝐵 × 𝐷) ∈ 𝑌) |
12 | | xpsadd.m |
. 2
⊢ · =
(+g‘𝑅) |
13 | | xpsadd.n |
. 2
⊢ × =
(+g‘𝑆) |
14 | | xpsadd.p |
. 2
⊢ ∙ =
(+g‘𝑇) |
15 | | eqid 2622 |
. 2
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
16 | | eqid 2622 |
. 2
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) |
17 | 15 | xpsff1o2 16231 |
. . . . 5
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
18 | | f1ocnv 6149 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
19 | 17, 18 | mp1i 13 |
. . . 4
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
20 | | f1ofo 6144 |
. . . 4
⊢ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌)) |
21 | 19, 20 | syl 17 |
. . 3
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–onto→(𝑋 × 𝑌)) |
22 | 19 | f1ocpbl 16185 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 𝑏 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) ∧ (𝑐 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 𝑑 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) → (((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑎) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑐) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑏) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘𝑑)) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝑎(+g‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))𝑏)) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(𝑐(+g‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))𝑑)))) |
23 | | eqid 2622 |
. . . 4
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
24 | 1, 2, 3, 4, 5, 15,
23, 16 | xpsval 16232 |
. . 3
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
25 | 1, 2, 3, 4, 5, 15,
23, 16 | xpslem 16233 |
. . 3
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
26 | | ovexd 6680 |
. . 3
⊢ (𝜑 → ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V) |
27 | | eqid 2622 |
. . 3
⊢
(+g‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) =
(+g‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
28 | 21, 22, 24, 25, 26, 27, 14 | imasaddval 16192 |
. 2
⊢ ((𝜑 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘(◡({𝐴} +𝑐 {𝐵})(+g‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})))) |
29 | | eqid 2622 |
. . 3
⊢
(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
30 | | fvexd 6203 |
. . 3
⊢ ((◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) → (Scalar‘𝑅) ∈ V) |
31 | | 2on 7568 |
. . . 4
⊢
2𝑜 ∈ On |
32 | 31 | a1i 11 |
. . 3
⊢ ((◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) → 2𝑜 ∈
On) |
33 | | simp1 1061 |
. . 3
⊢ ((◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
34 | | simp2 1062 |
. . 3
⊢ ((◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) → ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
35 | | simp3 1063 |
. . 3
⊢ ((◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) → ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
36 | 16, 29, 30, 32, 33, 34, 35, 27 | prdsplusgval 16133 |
. 2
⊢ ((◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ∧ ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∧ ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) → (◡({𝐴} +𝑐 {𝐵})(+g‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})) = (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(+g‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))) |
37 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 28, 36 | xpsaddlem 16235 |
1
⊢ (𝜑 → (〈𝐴, 𝐵〉 ∙ 〈𝐶, 𝐷〉) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) |