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	$⊢ \times_{𝑠} = (r \in V, s \in V ⟼ {(x \in {Base}_{r}, y \in {Base}_{s} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (Scalar (r) ⨉_{𝑠} \{⟨\emptyset, r⟩, ⟨1_{𝑜}, s⟩\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxps	$class \times_{𝑠}$
1		vr	$setvar r$
2		cvv	$class V$
3		vs	$setvar s$
4		vx	$setvar x$
5		cbs	$class Base$
6	1	cv	$setvar r$
7	6 5	cfv	$class {Base}_{r}$
8		vy	$setvar y$
9	3	cv	$setvar s$
10	9 5	cfv	$class {Base}_{s}$
11		c0	$class \emptyset$
12	4	cv	$setvar x$
13	11 12	cop	$class ⟨\emptyset, x⟩$
14		c1o	$class 1_{𝑜}$
15	8	cv	$setvar y$
16	14 15	cop	$class ⟨1_{𝑜}, y⟩$
17	13 16	cpr	$class \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}$
18	4 8 7 10 17	cmpo	$class (x \in {Base}_{r}, y \in {Base}_{s} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
19	18	ccnv	$class {(x \in {Base}_{r}, y \in {Base}_{s} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1}$
20		cimas	$class “_{𝑠}$
21		csca	$class Scalar$
22	6 21	cfv	$class Scalar (r)$
23		cprds	$class ⨉_{𝑠}$
24	11 6	cop	$class ⟨\emptyset, r⟩$
25	14 9	cop	$class ⟨1_{𝑜}, s⟩$
26	24 25	cpr	$class \{⟨\emptyset, r⟩, ⟨1_{𝑜}, s⟩\}$
27	22 26 23	co	$class (Scalar (r) ⨉_{𝑠} \{⟨\emptyset, r⟩, ⟨1_{𝑜}, s⟩\})$
28	19 27 20	co	$class ({(x \in {Base}_{r}, y \in {Base}_{s} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (Scalar (r) ⨉_{𝑠} \{⟨\emptyset, r⟩, ⟨1_{𝑜}, s⟩\}))$
29	1 3 2 2 28	cmpo	$class (r \in V, s \in V ⟼ {(x \in {Base}_{r}, y \in {Base}_{s} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (Scalar (r) ⨉_{𝑠} \{⟨\emptyset, r⟩, ⟨1_{𝑜}, s⟩\}))$
30	0 29	wceq	$wff \times_{𝑠} = (r \in V, s \in V ⟼ {(x \in {Base}_{r}, y \in {Base}_{s} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (Scalar (r) ⨉_{𝑠} \{⟨\emptyset, r⟩, ⟨1_{𝑜}, s⟩\}))$

Metamath Proof Explorer

Definition df-xps

Detailed syntax breakdown