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 , 𝑠 ⟩ } ) ) )