Metamath Proof Explorer


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