Metamath Proof Explorer


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 ) ) ) )