Definition df-pprod

Description: Define the parallel product of two classes. Membership in this class is defined by pprodss4v and brpprod . (Contributed by Scott Fenton, 11-Apr-2014)

	Ref	Expression
Assertion	df-pprod	⊢ pprod ( 𝐴 , 𝐵 ) = ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	cpprod	⊢ pprod ( 𝐴 , 𝐵 )
3		c1st	⊢ 1st
4		cvv	⊢ V
5	4 4	cxp	⊢ ( V × V )
6	3 5	cres	⊢ ( 1st ↾ ( V × V ) )
7	0 6	ccom	⊢ ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) )
8		c2nd	⊢ 2nd
9	8 5	cres	⊢ ( 2nd ↾ ( V × V ) )
10	1 9	ccom	⊢ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) )
11	7 10	ctxp	⊢ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) )
12	2 11	wceq	⊢ pprod ( 𝐴 , 𝐵 ) = ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) )