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

Definition df-xps 16775
 Description: Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)
Assertion
Ref Expression
df-xps ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
Distinct variable group:   𝑠,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-xps
StepHypRef Expression
1 cxps 16771 . 2 class ×s
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 cvv 3441 . . 3 class V
5 vx . . . . . 6 setvar 𝑥
6 vy . . . . . 6 setvar 𝑦
72cv 1537 . . . . . . 7 class 𝑟
8 cbs 16475 . . . . . . 7 class Base
97, 8cfv 6324 . . . . . 6 class (Base‘𝑟)
103cv 1537 . . . . . . 7 class 𝑠
1110, 8cfv 6324 . . . . . 6 class (Base‘𝑠)
12 c0 4243 . . . . . . . 8 class
135cv 1537 . . . . . . . 8 class 𝑥
1412, 13cop 4531 . . . . . . 7 class ⟨∅, 𝑥
15 c1o 8078 . . . . . . . 8 class 1o
166cv 1537 . . . . . . . 8 class 𝑦
1715, 16cop 4531 . . . . . . 7 class ⟨1o, 𝑦
1814, 17cpr 4527 . . . . . 6 class {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}
195, 6, 9, 11, 18cmpo 7137 . . . . 5 class (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
2019ccnv 5518 . . . 4 class (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
21 csca 16560 . . . . . 6 class Scalar
227, 21cfv 6324 . . . . 5 class (Scalar‘𝑟)
2312, 7cop 4531 . . . . . 6 class ⟨∅, 𝑟
2415, 10cop 4531 . . . . . 6 class ⟨1o, 𝑠
2523, 24cpr 4527 . . . . 5 class {⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}
26 cprds 16711 . . . . 5 class Xs
2722, 25, 26co 7135 . . . 4 class ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})
28 cimas 16769 . . . 4 class s
2920, 27, 28co 7135 . . 3 class ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}))
302, 3, 4, 4, 29cmpo 7137 . 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
311, 30wceq 1538 1 wff ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
 Colors of variables: wff setvar class This definition is referenced by:  xpsval  16835
 Copyright terms: Public domain W3C validator