Definition df-xps 16170

Description: Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.)

Assertion

Ref	Expression
df-xps	⊢ ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠}))))

Distinct variable group:   𝑠,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-xps

Step	Hyp	Ref	Expression
1		cxps 16166	. 2 class ×s
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3200	. . 3 class V
5		vx	. . . . . 6 setvar 𝑥
6		vy	. . . . . 6 setvar 𝑦
7	2	cv 1482	. . . . . . 7 class 𝑟
8		cbs 15857	. . . . . . 7 class Base
9	7, 8	cfv 5888	. . . . . 6 class (Base‘𝑟)
10	3	cv 1482	. . . . . . 7 class 𝑠
11	10, 8	cfv 5888	. . . . . 6 class (Base‘𝑠)
12	5	cv 1482	. . . . . . . . 9 class 𝑥
13	12	csn 4177	. . . . . . . 8 class {𝑥}
14	6	cv 1482	. . . . . . . . 9 class 𝑦
15	14	csn 4177	. . . . . . . 8 class {𝑦}
16		ccda 8989	. . . . . . . 8 class +𝑐
17	13, 15, 16	co 6650	. . . . . . 7 class ({𝑥} +𝑐 {𝑦})
18	17	ccnv 5113	. . . . . 6 class ◡({𝑥} +𝑐 {𝑦})
19	5, 6, 9, 11, 18	cmpt2 6652	. . . . 5 class (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦}))
20	19	ccnv 5113	. . . 4 class ◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦}))
21		csca 15944	. . . . . 6 class Scalar
22	7, 21	cfv 5888	. . . . 5 class (Scalar‘𝑟)
23	7	csn 4177	. . . . . . 7 class {𝑟}
24	10	csn 4177	. . . . . . 7 class {𝑠}
25	23, 24, 16	co 6650	. . . . . 6 class ({𝑟} +𝑐 {𝑠})
26	25	ccnv 5113	. . . . 5 class ◡({𝑟} +𝑐 {𝑠})
27		cprds 16106	. . . . 5 class Xs
28	22, 26, 27	co 6650	. . . 4 class ((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠}))
29		cimas 16164	. . . 4 class “s
30	20, 28, 29	co 6650	. . 3 class (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠})))
31	2, 3, 4, 4, 30	cmpt2 6652	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠}))))
32	1, 31	wceq 1483	1 wff ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠}))))

This definition is referenced by:  xpsval  16232