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

Definition df-xps 16378
Description: Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
df-xps ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑟)Xs({𝑟} +𝑐 {𝑠}))))
Distinct variable group:   𝑠,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-xps
StepHypRef Expression
1 cxps 16374 . 2 class ×s
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 cvv 3398 . . 3 class V
5 vx . . . . . 6 setvar 𝑥
6 vy . . . . . 6 setvar 𝑦
72cv 1636 . . . . . . 7 class 𝑟
8 cbs 16071 . . . . . . 7 class Base
97, 8cfv 6104 . . . . . 6 class (Base‘𝑟)
103cv 1636 . . . . . . 7 class 𝑠
1110, 8cfv 6104 . . . . . 6 class (Base‘𝑠)
125cv 1636 . . . . . . . . 9 class 𝑥
1312csn 4377 . . . . . . . 8 class {𝑥}
146cv 1636 . . . . . . . . 9 class 𝑦
1514csn 4377 . . . . . . . 8 class {𝑦}
16 ccda 9277 . . . . . . . 8 class +𝑐
1713, 15, 16co 6877 . . . . . . 7 class ({𝑥} +𝑐 {𝑦})
1817ccnv 5317 . . . . . 6 class ({𝑥} +𝑐 {𝑦})
195, 6, 9, 11, 18cmpt2 6879 . . . . 5 class (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ({𝑥} +𝑐 {𝑦}))
2019ccnv 5317 . . . 4 class (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ({𝑥} +𝑐 {𝑦}))
21 csca 16159 . . . . . 6 class Scalar
227, 21cfv 6104 . . . . 5 class (Scalar‘𝑟)
237csn 4377 . . . . . . 7 class {𝑟}
2410csn 4377 . . . . . . 7 class {𝑠}
2523, 24, 16co 6877 . . . . . 6 class ({𝑟} +𝑐 {𝑠})
2625ccnv 5317 . . . . 5 class ({𝑟} +𝑐 {𝑠})
27 cprds 16314 . . . . 5 class Xs
2822, 26, 27co 6877 . . . 4 class ((Scalar‘𝑟)Xs({𝑟} +𝑐 {𝑠}))
29 cimas 16372 . . . 4 class s
3020, 28, 29co 6877 . . 3 class ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑟)Xs({𝑟} +𝑐 {𝑠})))
312, 3, 4, 4, 30cmpt2 6879 . 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑟)Xs({𝑟} +𝑐 {𝑠}))))
321, 31wceq 1637 1 wff ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑟)Xs({𝑟} +𝑐 {𝑠}))))
Colors of variables: wff setvar class
This definition is referenced by:  xpsval  16440
  Copyright terms: Public domain W3C validator