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