Definition df-xps 13691

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

Assertion

Ref	Expression
df-xps	|- X.s = ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> `' ( { x } +c { y } ) ) "s ( (Scalar ` r ) X_s `' ( { r } +c { s } ) ) ) )

Distinct variable group:   s, r, x, y

Detailed syntax breakdown of Definition df-xps

Step	Hyp	Ref	Expression
1		cxps 13687	. 2 class X.s
2		vr	. . 3 set r
3		vs	. . 3 set s
4		cvv 2916	. . 3 class _V
5		vx	. . . . . 6 set x
6		vy	. . . . . 6 set y
7	2	cv 1648	. . . . . . 7 class r
8		cbs 13424	. . . . . . 7 class Base
9	7, 8	cfv 5413	. . . . . 6 class ( Base ` r )
10	3	cv 1648	. . . . . . 7 class s
11	10, 8	cfv 5413	. . . . . 6 class ( Base ` s )
12	5	cv 1648	. . . . . . . . 9 class x
13	12	csn 3774	. . . . . . . 8 class { x }
14	6	cv 1648	. . . . . . . . 9 class y
15	14	csn 3774	. . . . . . . 8 class { y }
16		ccda 8003	. . . . . . . 8 class +c
17	13, 15, 16	co 6040	. . . . . . 7 class ( { x } +c { y } )
18	17	ccnv 4836	. . . . . 6 class `' ( { x } +c { y } )
19	5, 6, 9, 11, 18	cmpt2 6042	. . . . 5 class ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> `' ( { x } +c { y } ) )
20	19	ccnv 4836	. . . 4 class `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> `' ( { x } +c { y } ) )
21		csca 13487	. . . . . 6 class Scalar
22	7, 21	cfv 5413	. . . . 5 class (Scalar ` r )
23	7	csn 3774	. . . . . . 7 class { r }
24	10	csn 3774	. . . . . . 7 class { s }
25	23, 24, 16	co 6040	. . . . . 6 class ( { r } +c { s } )
26	25	ccnv 4836	. . . . 5 class `' ( { r } +c { s } )
27		cprds 13624	. . . . 5 class X_s
28	22, 26, 27	co 6040	. . . 4 class ( (Scalar ` r ) X_s `' ( { r } +c { s } ) )
29		cimas 13685	. . . 4 class "s
30	20, 28, 29	co 6040	. . 3 class ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> `' ( { x } +c { y } ) ) "s ( (Scalar ` r ) X_s `' ( { r } +c { s } ) ) )
31	2, 3, 4, 4, 30	cmpt2 6042	. 2 class ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> `' ( { x } +c { y } ) ) "s ( (Scalar ` r ) X_s `' ( { r } +c { s } ) ) ) )
32	1, 31	wceq 1649	1 wff X.s = ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> `' ( { x } +c { y } ) ) "s ( (Scalar ` r ) X_s `' ( { r } +c { s } ) ) ) )

This definition is referenced by:  xpsval  13752