Definition df-xps 17555

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

Assertion

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

Distinct variable group:   𝑠,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-xps

Step	Hyp	Ref	Expression
1		cxps 17551	. 2 class ×s
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3480	. . 3 class V
5		vx	. . . . . 6 setvar 𝑥
6		vy	. . . . . 6 setvar 𝑦
7	2	cv 1539	. . . . . . 7 class 𝑟
8		cbs 17247	. . . . . . 7 class Base
9	7, 8	cfv 6561	. . . . . 6 class (Base‘𝑟)
10	3	cv 1539	. . . . . . 7 class 𝑠
11	10, 8	cfv 6561	. . . . . 6 class (Base‘𝑠)
12		c0 4333	. . . . . . . 8 class ∅
13	5	cv 1539	. . . . . . . 8 class 𝑥
14	12, 13	cop 4632	. . . . . . 7 class ⟨∅, 𝑥⟩
15		c1o 8499	. . . . . . . 8 class 1o
16	6	cv 1539	. . . . . . . 8 class 𝑦
17	15, 16	cop 4632	. . . . . . 7 class ⟨1o, 𝑦⟩
18	14, 17	cpr 4628	. . . . . 6 class {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}
19	5, 6, 9, 11, 18	cmpo 7433	. . . . 5 class (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
20	19	ccnv 5684	. . . 4 class ◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
21		csca 17300	. . . . . 6 class Scalar
22	7, 21	cfv 6561	. . . . 5 class (Scalar‘𝑟)
23	12, 7	cop 4632	. . . . . 6 class ⟨∅, 𝑟⟩
24	15, 10	cop 4632	. . . . . 6 class ⟨1o, 𝑠⟩
25	23, 24	cpr 4628	. . . . 5 class {⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}
26		cprds 17490	. . . . 5 class Xs
27	22, 25, 26	co 7431	. . . 4 class ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})
28		cimas 17549	. . . 4 class “s
29	20, 27, 28	co 7431	. . 3 class (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}))
30	2, 3, 4, 4, 29	cmpo 7433	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
31	1, 30	wceq 1540	1 wff ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))

This definition is referenced by:  xpsval  17615