| 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 | | xpsmul.m |
. 2
⊢ · =
(.r‘𝑅) |
| 13 | | xpsmul.n |
. 2
⊢ × =
(.r‘𝑆) |
| 14 | | xpsmul.p |
. 2
⊢ ∙ =
(.r‘𝑇) |
| 15 | | eqid 2736 |
. 2
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) |
| 16 | | eqid 2736 |
. 2
⊢
((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) = ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) |
| 17 | 15 | xpsff1o2 17451 |
. . . . 5
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) |
| 18 | | f1ocnv 6796 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})–1-1-onto→(𝑋 × 𝑌)) |
| 19 | 17, 18 | mp1i 13 |
. . . 4
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})–1-1-onto→(𝑋 × 𝑌)) |
| 20 | | f1ofo 6791 |
. . . 4
⊢ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})–1-1-onto→(𝑋 × 𝑌) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})–onto→(𝑋 × 𝑌)) |
| 21 | 19, 20 | syl 17 |
. . 3
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})–onto→(𝑋 × 𝑌)) |
| 22 | 19 | f1ocpbl 17407 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) ∧ 𝑏 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})) ∧ (𝑐 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) ∧ 𝑑 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))) → (((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘𝑎) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘𝑐) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘𝑏) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘𝑑)) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘(𝑎(.r‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))𝑏)) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘(𝑐(.r‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))𝑑)))) |
| 23 | | eqid 2736 |
. . . 4
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
| 24 | 1, 2, 3, 4, 5, 15,
23, 16 | xpsval 17452 |
. . 3
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
“s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) |
| 25 | 1, 2, 3, 4, 5, 15,
23, 16 | xpsrnbas 17453 |
. . 3
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) =
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) |
| 26 | | ovexd 7392 |
. . 3
⊢ (𝜑 → ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) ∈
V) |
| 27 | | eqid 2736 |
. . 3
⊢
(.r‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) =
(.r‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) |
| 28 | 21, 22, 24, 25, 26, 27, 14 | imasmulval 17417 |
. 2
⊢ ((𝜑 ∧ {⟨∅, 𝐴⟩, ⟨1o,
𝐵⟩} ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) ∧ {⟨∅,
𝐶⟩,
⟨1o, 𝐷⟩} ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})) → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅,
𝐴⟩,
⟨1o, 𝐵⟩}) ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅,
𝐶⟩,
⟨1o, 𝐷⟩})) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘({⟨∅,
𝐴⟩,
⟨1o, 𝐵⟩}
(.r‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})){⟨∅, 𝐶⟩, ⟨1o,
𝐷⟩}))) |
| 29 | | eqid 2736 |
. . 3
⊢
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) =
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) |
| 30 | | fvexd 6857 |
. . 3
⊢
(({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o ∧
{⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∧ {⟨∅,
𝐶⟩,
⟨1o, 𝐷⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) →
(Scalar‘𝑅) ∈
V) |
| 31 | | 2on 8426 |
. . . 4
⊢
2o ∈ On |
| 32 | 31 | a1i 11 |
. . 3
⊢
(({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o ∧
{⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∧ {⟨∅,
𝐶⟩,
⟨1o, 𝐷⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) → 2o
∈ On) |
| 33 | | simp1 1136 |
. . 3
⊢
(({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o ∧
{⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∧ {⟨∅,
𝐶⟩,
⟨1o, 𝐷⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) →
{⟨∅, 𝑅⟩,
⟨1o, 𝑆⟩} Fn 2o) |
| 34 | | simp2 1137 |
. . 3
⊢
(({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o ∧
{⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∧ {⟨∅,
𝐶⟩,
⟨1o, 𝐷⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) →
{⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) |
| 35 | | simp3 1138 |
. . 3
⊢
(({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o ∧
{⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∧ {⟨∅,
𝐶⟩,
⟨1o, 𝐷⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) →
{⟨∅, 𝐶⟩,
⟨1o, 𝐷⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) |
| 36 | 16, 29, 30, 32, 33, 34, 35, 27 | prdsmulrval 17357 |
. 2
⊢
(({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o ∧
{⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∧ {⟨∅,
𝐶⟩,
⟨1o, 𝐷⟩} ∈
(Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))) →
({⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩}
(.r‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})){⟨∅, 𝐶⟩, ⟨1o,
𝐷⟩}) = (𝑘 ∈ 2o ↦
(({⟨∅, 𝐴⟩,
⟨1o, 𝐵⟩}‘𝑘)(.r‘({⟨∅, 𝑅⟩, ⟨1o,
𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o,
𝐷⟩}‘𝑘)))) |
| 37 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 28, 36 | xpsaddlem 17455 |
1
⊢ (𝜑 → (⟨𝐴, 𝐵⟩ ∙ ⟨𝐶, 𝐷⟩) = ⟨(𝐴 · 𝐶), (𝐵 × 𝐷)⟩) |
