Metamath Proof Explorer

Definition df-xps

Description: Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Jim Kingdon, 25-Sep-2023)

Ref Expression
Assertion df-xps ⊢ × 𝑠 = r ∈ V , s ∈ V ⟼ x ∈ Base r , y ∈ Base s ⟼ ∅ x 1 𝑜 y -1 “ 𝑠 Scalar ⁡ r ⨉ 𝑠 ∅ r 1 𝑜 s

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxps class × 𝑠
1 vr setvar r
2 cvv class V
3 vs setvar s
4 vx setvar x
5 cbs class Base
6 1 cv setvar r
7 6 5 cfv class Base r
8 vy setvar y
9 3 cv setvar s
10 9 5 cfv class Base s
11 c0 class ∅
12 4 cv setvar x
13 11 12 cop class ∅ x
14 c1o class 1 𝑜
15 8 cv setvar y
16 14 15 cop class 1 𝑜 y
17 13 16 cpr class ∅ x 1 𝑜 y
18 4 8 7 10 17 cmpo class x ∈ Base r , y ∈ Base s ⟼ ∅ x 1 𝑜 y
19 18 ccnv class x ∈ Base r , y ∈ Base s ⟼ ∅ x 1 𝑜 y -1
20 cimas class “ 𝑠
21 csca class Scalar
22 6 21 cfv class Scalar ⁡ r
23 cprds class ⨉ 𝑠
24 11 6 cop class ∅ r
25 14 9 cop class 1 𝑜 s
26 24 25 cpr class ∅ r 1 𝑜 s
27 22 26 23 co class Scalar ⁡ r ⨉ 𝑠 ∅ r 1 𝑜 s
28 19 27 20 co class x ∈ Base r , y ∈ Base s ⟼ ∅ x 1 𝑜 y -1 “ 𝑠 Scalar ⁡ r ⨉ 𝑠 ∅ r 1 𝑜 s
29 1 3 2 2 28 cmpo class r ∈ V , s ∈ V ⟼ x ∈ Base r , y ∈ Base s ⟼ ∅ x 1 𝑜 y -1 “ 𝑠 Scalar ⁡ r ⨉ 𝑠 ∅ r 1 𝑜 s
30 0 29 wceq wff × 𝑠 = r ∈ V , s ∈ V ⟼ x ∈ Base r , y ∈ Base s ⟼ ∅ x 1 𝑜 y -1 “ 𝑠 Scalar ⁡ r ⨉ 𝑠 ∅ r 1 𝑜 s