Definition df-xps 17456

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 17452	. 2 class ×s
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3475	. . 3 class V
5		vx	. . . . . 6 setvar 𝑥
6		vy	. . . . . 6 setvar 𝑦
7	2	cv 1541	. . . . . . 7 class 𝑟
8		cbs 17144	. . . . . . 7 class Base
9	7, 8	cfv 6544	. . . . . 6 class (Base‘𝑟)
10	3	cv 1541	. . . . . . 7 class 𝑠
11	10, 8	cfv 6544	. . . . . 6 class (Base‘𝑠)
12		c0 4323	. . . . . . . 8 class ∅
13	5	cv 1541	. . . . . . . 8 class 𝑥
14	12, 13	cop 4635	. . . . . . 7 class ⟨∅, 𝑥⟩
15		c1o 8459	. . . . . . . 8 class 1o
16	6	cv 1541	. . . . . . . 8 class 𝑦
17	15, 16	cop 4635	. . . . . . 7 class ⟨1o, 𝑦⟩
18	14, 17	cpr 4631	. . . . . 6 class {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}
19	5, 6, 9, 11, 18	cmpo 7411	. . . . 5 class (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
20	19	ccnv 5676	. . . 4 class ◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
21		csca 17200	. . . . . 6 class Scalar
22	7, 21	cfv 6544	. . . . 5 class (Scalar‘𝑟)
23	12, 7	cop 4635	. . . . . 6 class ⟨∅, 𝑟⟩
24	15, 10	cop 4635	. . . . . 6 class ⟨1o, 𝑠⟩
25	23, 24	cpr 4631	. . . . 5 class {⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}
26		cprds 17391	. . . . 5 class Xs
27	22, 25, 26	co 7409	. . . 4 class ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})
28		cimas 17450	. . . 4 class “s
29	20, 27, 28	co 7409	. . 3 class (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}))
30	2, 3, 4, 4, 29	cmpo 7411	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
31	1, 30	wceq 1542	1 wff ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))

This definition is referenced by:  xpsval  17516