This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxps 
 |-  Xs.
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vs 
 |-  s
4 vx 
 |-  x
5 cbs 
 |-  Base
6 1 cv 
 |-  r
7 6 5 cfv 
 |-  ( Base ` r )
8 vy 
 |-  y
9 3 cv 
 |-  s
10 9 5 cfv 
 |-  ( Base ` s )
11 c0 
 |-  (/)
12 4 cv 
 |-  x
13 11 12 cop 
 |-  <. (/) , x >.
14 c1o 
 |-  1o
15 8 cv 
 |-  y
16 14 15 cop 
 |-  <. 1o , y >.
17 13 16 cpr 
 |-  { <. (/) , x >. , <. 1o , y >. }
18 4 8 7 10 17 cmpo 
 |-  ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } )
19 18 ccnv 
 |-  `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } )
20 cimas 
 |-  "s
21 csca 
 |-  Scalar
22 6 21 cfv 
 |-  ( Scalar ` r )
23 cprds 
 |-  Xs_
24 11 6 cop 
 |-  <. (/) , r >.
25 14 9 cop 
 |-  <. 1o , s >.
26 24 25 cpr 
 |-  { <. (/) , r >. , <. 1o , s >. }
27 22 26 23 co 
 |-  ( ( Scalar ` r ) Xs_ { <. (/) , r >. , <. 1o , s >. } )
28 19 27 20 co 
 |-  ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` r ) Xs_ { <. (/) , r >. , <. 1o , s >. } ) )
29 1 3 2 2 28 cmpo 
 |-  ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` r ) Xs_ { <. (/) , r >. , <. 1o , s >. } ) ) )
30 0 29 wceq 
 |-  Xs. = ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` r ) Xs_ { <. (/) , r >. , <. 1o , s >. } ) ) )