MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xps Unicode version

Definition df-xps 13408
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
StepHypRef Expression
1 cxps 13404 . 2  class  X.s
2 vr . . 3  set  r
3 vs . . 3  set  s
4 cvv 2790 . . 3  class  _V
5 vx . . . . . 6  set  x
6 vy . . . . . 6  set  y
72cv 1623 . . . . . . 7  class  r
8 cbs 13143 . . . . . . 7  class  Base
97, 8cfv 5222 . . . . . 6  class  ( Base `  r )
103cv 1623 . . . . . . 7  class  s
1110, 8cfv 5222 . . . . . 6  class  ( Base `  s )
125cv 1623 . . . . . . . . 9  class  x
1312csn 3642 . . . . . . . 8  class  { x }
146cv 1623 . . . . . . . . 9  class  y
1514csn 3642 . . . . . . . 8  class  { y }
16 ccda 7789 . . . . . . . 8  class  +c
1713, 15, 16co 5820 . . . . . . 7  class  ( { x }  +c  {
y } )
1817ccnv 4688 . . . . . 6  class  `' ( { x }  +c  { y } )
195, 6, 9, 11, 18cmpt2 5822 . . . . 5  class  ( x  e.  ( Base `  r
) ,  y  e.  ( Base `  s
)  |->  `' ( { x }  +c  {
y } ) )
2019ccnv 4688 . . . 4  class  `' ( x  e.  ( Base `  r ) ,  y  e.  ( Base `  s
)  |->  `' ( { x }  +c  {
y } ) )
21 csca 13206 . . . . . 6  class Scalar
227, 21cfv 5222 . . . . 5  class  (Scalar `  r )
237csn 3642 . . . . . . 7  class  { r }
2410csn 3642 . . . . . . 7  class  { s }
2523, 24, 16co 5820 . . . . . 6  class  ( { r }  +c  {
s } )
2625ccnv 4688 . . . . 5  class  `' ( { r }  +c  { s } )
27 cprds 13341 . . . . 5  class  X_s
2822, 26, 27co 5820 . . . 4  class  ( (Scalar `  r ) X_s `' ( { r }  +c  { s } ) )
29 cimas 13402 . . . 4  class  "s
3020, 28, 29co 5820 . . 3  class  ( `' ( x  e.  (
Base `  r ) ,  y  e.  ( Base `  s )  |->  `' ( { x }  +c  { y } ) )  "s  ( (Scalar `  r
) X_s `' ( { r }  +c  { s } ) ) )
312, 3, 4, 4, 30cmpt2 5822 . 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 } ) ) ) )
321, 31wceq 1624 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 } ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  xpsval  13469
  Copyright terms: Public domain W3C validator