Definition df-xps 12724

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 12721	. 2 class ×s
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 2737	. . 3 class V
5		vx	. . . . . 6 setvar 𝑥
6		vy	. . . . . 6 setvar 𝑦
7	2	cv 1352	. . . . . . 7 class 𝑟
8		cbs 12461	. . . . . . 7 class Base
9	7, 8	cfv 5216	. . . . . 6 class (Base‘𝑟)
10	3	cv 1352	. . . . . . 7 class 𝑠
11	10, 8	cfv 5216	. . . . . 6 class (Base‘𝑠)
12		c0 3422	. . . . . . . 8 class ∅
13	5	cv 1352	. . . . . . . 8 class 𝑥
14	12, 13	cop 3595	. . . . . . 7 class ⟨∅, 𝑥⟩
15		c1o 6409	. . . . . . . 8 class 1o
16	6	cv 1352	. . . . . . . 8 class 𝑦
17	15, 16	cop 3595	. . . . . . 7 class ⟨1o, 𝑦⟩
18	14, 17	cpr 3593	. . . . . 6 class {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}
19	5, 6, 9, 11, 18	cmpo 5876	. . . . 5 class (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
20	19	ccnv 4625	. . . 4 class ◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
21		csca 12538	. . . . . 6 class Scalar
22	7, 21	cfv 5216	. . . . 5 class (Scalar‘𝑟)
23	12, 7	cop 3595	. . . . . 6 class ⟨∅, 𝑟⟩
24	15, 10	cop 3595	. . . . . 6 class ⟨1o, 𝑠⟩
25	23, 24	cpr 3593	. . . . 5 class {⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}
26		cprds 12713	. . . . 5 class Xs
27	22, 25, 26	co 5874	. . . 4 class ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})
28		cimas 12719	. . . 4 class “s
29	20, 27, 28	co 5874	. . 3 class (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}))
30	2, 3, 4, 4, 29	cmpo 5876	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
31	1, 30	wceq 1353	1 wff ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))

This definition is referenced by:  xpsval  12770