| 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 2737 | . 2
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) | 
| 16 |  | eqid 2737 | . 2
⊢
((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) = ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) | 
| 17 | 15 | xpsff1o2 17614 | . . . . 5
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) | 
| 18 |  | f1ocnv 6860 | . . . . 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 6855 | . . . 4
⊢ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})–1-1-onto→(𝑋 × 𝑌) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})–onto→(𝑋 × 𝑌)) | 
| 21 | 19, 20 | syl 17 | . . 3
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})–onto→(𝑋 × 𝑌)) | 
| 22 | 19 | f1ocpbl 17570 | . . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ∧ 𝑏 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})) ∧ (𝑐 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ∧ 𝑑 ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}))) → (((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘𝑎) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘𝑐) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘𝑏) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘𝑑)) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘(𝑎(+g‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))𝑏)) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘(𝑐(+g‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))𝑑)))) | 
| 23 |  | eqid 2737 | . . . 4
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) | 
| 24 | 1, 2, 3, 4, 5, 15,
23, 16 | xpsval 17615 | . . 3
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})
“s ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) | 
| 25 | 1, 2, 3, 4, 5, 15,
23, 16 | xpsrnbas 17616 | . . 3
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) =
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) | 
| 26 |  | ovexd 7466 | . . 3
⊢ (𝜑 → ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) ∈
V) | 
| 27 |  | eqid 2737 | . . 3
⊢
(+g‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) =
(+g‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) | 
| 28 | 21, 22, 24, 25, 26, 27, 14 | imasaddval 17577 | . 2
⊢ ((𝜑 ∧ {〈∅, 𝐴〉, 〈1o,
𝐵〉} ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ∧ {〈∅,
𝐶〉,
〈1o, 𝐷〉} ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})) → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘{〈∅,
𝐴〉,
〈1o, 𝐵〉}) ∙ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘{〈∅,
𝐶〉,
〈1o, 𝐷〉})) = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})‘({〈∅,
𝐴〉,
〈1o, 𝐵〉}
(+g‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})){〈∅, 𝐶〉, 〈1o,
𝐷〉}))) | 
| 29 |  | eqid 2737 | . . 3
⊢
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) =
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) | 
| 30 |  | fvexd 6921 | . . 3
⊢
(({〈∅, 𝑅〉, 〈1o, 𝑆〉} Fn 2o ∧
{〈∅, 𝐴〉,
〈1o, 𝐵〉} ∈
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ∧ {〈∅,
𝐶〉,
〈1o, 𝐷〉} ∈
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) →
(Scalar‘𝑅) ∈
V) | 
| 31 |  | 2on 8520 | . . . 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 1137 | . . 3
⊢
(({〈∅, 𝑅〉, 〈1o, 𝑆〉} Fn 2o ∧
{〈∅, 𝐴〉,
〈1o, 𝐵〉} ∈
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ∧ {〈∅,
𝐶〉,
〈1o, 𝐷〉} ∈
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) →
{〈∅, 𝑅〉,
〈1o, 𝑆〉} Fn 2o) | 
| 34 |  | simp2 1138 | . . 3
⊢
(({〈∅, 𝑅〉, 〈1o, 𝑆〉} Fn 2o ∧
{〈∅, 𝐴〉,
〈1o, 𝐵〉} ∈
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ∧ {〈∅,
𝐶〉,
〈1o, 𝐷〉} ∈
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) →
{〈∅, 𝐴〉,
〈1o, 𝐵〉} ∈
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) | 
| 35 |  | simp3 1139 | . . 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 | prdsplusgval 17518 | . 2
⊢
(({〈∅, 𝑅〉, 〈1o, 𝑆〉} Fn 2o ∧
{〈∅, 𝐴〉,
〈1o, 𝐵〉} ∈
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ∧ {〈∅,
𝐶〉,
〈1o, 𝐷〉} ∈
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) →
({〈∅, 𝐴〉,
〈1o, 𝐵〉}
(+g‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})){〈∅, 𝐶〉, 〈1o,
𝐷〉}) = (𝑘 ∈ 2o ↦
(({〈∅, 𝐴〉,
〈1o, 𝐵〉}‘𝑘)(+g‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘))({〈∅, 𝐶〉, 〈1o,
𝐷〉}‘𝑘)))) | 
| 37 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 28, 36 | xpsaddlem 17618 | 1
⊢ (𝜑 → (〈𝐴, 𝐵〉 ∙ 〈𝐶, 𝐷〉) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) |