This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-xps

Description: Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Jim Kingdon, 25-Sep-2023)

Ref Expression
Assertion df-xps ×s = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Base ‘ 𝑠 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑟 ) Xs { ⟨ ∅ , 𝑟 ⟩ , ⟨ 1o , 𝑠 ⟩ } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxps ⊢ ×s
1 vr ⊢ 𝑟
2 cvv ⊢ V
3 vs ⊢ 𝑠
4 vx ⊢ 𝑥
5 cbs ⊢ Base
6 1 cv ⊢ 𝑟
7 6 5 cfv ⊢ ( Base ‘ 𝑟 )
8 vy ⊢ 𝑦
9 3 cv ⊢ 𝑠
10 9 5 cfv ⊢ ( Base ‘ 𝑠 )
11 c0 ⊢ ∅
12 4 cv ⊢ 𝑥
13 11 12 cop ⊢ ⟨ ∅ , 𝑥 ⟩
14 c1o ⊢ 1o
15 8 cv ⊢ 𝑦
16 14 15 cop ⊢ ⟨ 1o , 𝑦 ⟩
17 13 16 cpr ⊢ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ }
18 4 8 7 10 17 cmpo ⊢ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Base ‘ 𝑠 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
19 18 ccnv ⊢ ◡ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Base ‘ 𝑠 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
20 cimas ⊢ “s
21 csca ⊢ Scalar
22 6 21 cfv ⊢ ( Scalar ‘ 𝑟 )
23 cprds ⊢ Xs
24 11 6 cop ⊢ ⟨ ∅ , 𝑟 ⟩
25 14 9 cop ⊢ ⟨ 1o , 𝑠 ⟩
26 24 25 cpr ⊢ { ⟨ ∅ , 𝑟 ⟩ , ⟨ 1o , 𝑠 ⟩ }
27 22 26 23 co ⊢ ( ( Scalar ‘ 𝑟 ) Xs { ⟨ ∅ , 𝑟 ⟩ , ⟨ 1o , 𝑠 ⟩ } )
28 19 27 20 co ⊢ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Base ‘ 𝑠 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑟 ) Xs { ⟨ ∅ , 𝑟 ⟩ , ⟨ 1o , 𝑠 ⟩ } ) )
29 1 3 2 2 28 cmpo ⊢ ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Base ‘ 𝑠 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑟 ) Xs { ⟨ ∅ , 𝑟 ⟩ , ⟨ 1o , 𝑠 ⟩ } ) ) )
30 0 29 wceq ⊢ ×s = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Base ‘ 𝑠 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑟 ) Xs { ⟨ ∅ , 𝑟 ⟩ , ⟨ 1o , 𝑠 ⟩ } ) ) )