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

Definition df-xps 15410
 Description: Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
df-xps s s Scalars
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-xps
StepHypRef Expression
1 cxps 15405 . 2 s
2 vr . . 3
3 vs . . 3
4 cvv 3045 . . 3
5 vx . . . . . 6
6 vy . . . . . 6
72cv 1443 . . . . . . 7
8 cbs 15121 . . . . . . 7
97, 8cfv 5582 . . . . . 6
103cv 1443 . . . . . . 7
1110, 8cfv 5582 . . . . . 6
125cv 1443 . . . . . . . . 9
1312csn 3968 . . . . . . . 8
146cv 1443 . . . . . . . . 9
1514csn 3968 . . . . . . . 8
16 ccda 8597 . . . . . . . 8
1713, 15, 16co 6290 . . . . . . 7
1817ccnv 4833 . . . . . 6
195, 6, 9, 11, 18cmpt2 6292 . . . . 5
2019ccnv 4833 . . . 4
21 csca 15193 . . . . . 6 Scalar
227, 21cfv 5582 . . . . 5 Scalar
237csn 3968 . . . . . . 7
2410csn 3968 . . . . . . 7
2523, 24, 16co 6290 . . . . . 6
2625ccnv 4833 . . . . 5
27 cprds 15344 . . . . 5 s
2822, 26, 27co 6290 . . . 4 Scalars
29 cimas 15402 . . . 4 s
3020, 28, 29co 6290 . . 3 s Scalars
312, 3, 4, 4, 30cmpt2 6292 . 2 s Scalars
321, 31wceq 1444 1 s s Scalars
 Colors of variables: wff setvar class This definition is referenced by:  xpsval  15478
 Copyright terms: Public domain W3C validator