Definition df-xps 12725

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	|- X.s = ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( (Scalar ` r ) X_s { <. (/) , r >. , <. 1o , s >. } ) ) )

Distinct variable group:   s, r, x, y

Detailed syntax breakdown of Definition df-xps

Step	Hyp	Ref	Expression
1		cxps 12722	. 2 class X.s
2		vr	. . 3 setvar r
3		vs	. . 3 setvar s
4		cvv 2738	. . 3 class _V
5		vx	. . . . . 6 setvar x
6		vy	. . . . . 6 setvar y
7	2	cv 1352	. . . . . . 7 class r
8		cbs 12462	. . . . . . 7 class Base
9	7, 8	cfv 5217	. . . . . 6 class ( Base ` r )
10	3	cv 1352	. . . . . . 7 class s
11	10, 8	cfv 5217	. . . . . 6 class ( Base ` s )
12		c0 3423	. . . . . . . 8 class (/)
13	5	cv 1352	. . . . . . . 8 class x
14	12, 13	cop 3596	. . . . . . 7 class <. (/) , x >.
15		c1o 6410	. . . . . . . 8 class 1o
16	6	cv 1352	. . . . . . . 8 class y
17	15, 16	cop 3596	. . . . . . 7 class <. 1o , y >.
18	14, 17	cpr 3594	. . . . . 6 class { <. (/) , x >. , <. 1o , y >. }
19	5, 6, 9, 11, 18	cmpo 5877	. . . . 5 class ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } )
20	19	ccnv 4626	. . . 4 class `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } )
21		csca 12539	. . . . . 6 class Scalar
22	7, 21	cfv 5217	. . . . 5 class (Scalar ` r )
23	12, 7	cop 3596	. . . . . 6 class <. (/) , r >.
24	15, 10	cop 3596	. . . . . 6 class <. 1o , s >.
25	23, 24	cpr 3594	. . . . 5 class { <. (/) , r >. , <. 1o , s >. }
26		cprds 12714	. . . . 5 class X_s
27	22, 25, 26	co 5875	. . . 4 class ( (Scalar ` r ) X_s { <. (/) , r >. , <. 1o , s >. } )
28		cimas 12720	. . . 4 class "s
29	20, 27, 28	co 5875	. . 3 class ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( (Scalar ` r ) X_s { <. (/) , r >. , <. 1o , s >. } ) )
30	2, 3, 4, 4, 29	cmpo 5877	. 2 class ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( (Scalar ` r ) X_s { <. (/) , r >. , <. 1o , s >. } ) ) )
31	1, 30	wceq 1353	1 wff X.s = ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( (Scalar ` r ) X_s { <. (/) , r >. , <. 1o , s >. } ) ) )

This definition is referenced by:  xpsval  12771