Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Quantifier-free definitions
dfpprod2
Next ⟩
pprodcnveq
Metamath Proof Explorer
Ascii
Unicode
Theorem
dfpprod2
Description:
Expanded definition of parallel product.
(Contributed by
Scott Fenton
, 3-May-2014)
Ref
Expression
Assertion
dfpprod2
⊢
pprod
A
B
=
1
st
↾
V
×
V
-1
∘
A
∘
1
st
↾
V
×
V
∩
2
nd
↾
V
×
V
-1
∘
B
∘
2
nd
↾
V
×
V
Proof
Step
Hyp
Ref
Expression
1
df-pprod
⊢
pprod
A
B
=
A
∘
1
st
↾
V
×
V
⊗
B
∘
2
nd
↾
V
×
V
2
df-txp
⊢
A
∘
1
st
↾
V
×
V
⊗
B
∘
2
nd
↾
V
×
V
=
1
st
↾
V
×
V
-1
∘
A
∘
1
st
↾
V
×
V
∩
2
nd
↾
V
×
V
-1
∘
B
∘
2
nd
↾
V
×
V
3
1
2
eqtri
⊢
pprod
A
B
=
1
st
↾
V
×
V
-1
∘
A
∘
1
st
↾
V
×
V
∩
2
nd
↾
V
×
V
-1
∘
B
∘
2
nd
↾
V
×
V