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 16773
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 16769 . 2 class ×s
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 cvv 3495 . . 3 class V
5 vx . . . . . 6 setvar 𝑥
6 vy . . . . . 6 setvar 𝑦
72cv 1527 . . . . . . 7 class 𝑟
8 cbs 16473 . . . . . . 7 class Base
97, 8cfv 6349 . . . . . 6 class (Base‘𝑟)
103cv 1527 . . . . . . 7 class 𝑠
1110, 8cfv 6349 . . . . . 6 class (Base‘𝑠)
12 c0 4290 . . . . . . . 8 class
135cv 1527 . . . . . . . 8 class 𝑥
1412, 13cop 4565 . . . . . . 7 class ⟨∅, 𝑥
15 c1o 8086 . . . . . . . 8 class 1o
166cv 1527 . . . . . . . 8 class 𝑦
1715, 16cop 4565 . . . . . . 7 class ⟨1o, 𝑦
1814, 17cpr 4561 . . . . . 6 class {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}
195, 6, 9, 11, 18cmpo 7147 . . . . 5 class (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
2019ccnv 5548 . . . 4 class (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
21 csca 16558 . . . . . 6 class Scalar
227, 21cfv 6349 . . . . 5 class (Scalar‘𝑟)
2312, 7cop 4565 . . . . . 6 class ⟨∅, 𝑟
2415, 10cop 4565 . . . . . 6 class ⟨1o, 𝑠
2523, 24cpr 4561 . . . . 5 class {⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}
26 cprds 16709 . . . . 5 class Xs
2722, 25, 26co 7145 . . . 4 class ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})
28 cimas 16767 . . . 4 class s
2920, 27, 28co 7145 . . 3 class ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩}))
302, 3, 4, 4, 29cmpo 7147 . 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
311, 30wceq 1528 1 wff ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
Colors of variables: wff setvar class
This definition is referenced by:  xpsval  16833
  Copyright terms: Public domain W3C validator