Theorem dfpprod2

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

	Ref	Expression
Assertion	dfpprod2	⊢ pprod ( 𝐴 , 𝐵 ) = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-pprod	⊢ pprod ( 𝐴 , 𝐵 ) = ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) )
2		df-txp	⊢ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
3	1 2	eqtri	⊢ pprod ( 𝐴 , 𝐵 ) = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) )