dfpprod2

Description: Expanded definition of parallel product. (Contributed by Scott Fenton, 3-May-2014)

		Ref	Expression
	Assertion	dfpprod2	$⊢ pprod (A, B) = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ (A \circ ({1^{st} ↾}_{(V \times V)}))) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ (B \circ ({2^{nd} ↾}_{(V \times V)})))$

Step	Hyp	Ref	Expression
1		df-pprod	$⊢ pprod (A, B) = ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)})))$
2		df-txp	$⊢ ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ (A \circ ({1^{st} ↾}_{(V \times V)}))) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ (B \circ ({2^{nd} ↾}_{(V \times V)})))$
3	1 2	eqtri	$⊢ pprod (A, B) = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ (A \circ ({1^{st} ↾}_{(V \times V)}))) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ (B \circ ({2^{nd} ↾}_{(V \times V)})))$

Metamath Proof Explorer