Definition df-pprod 34641

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

Assertion

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

Detailed syntax breakdown of Definition df-pprod

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cpprod 34617	. 2 class pprod(𝐴, 𝐵)
4		c1st 7952	. . . . 5 class 1st
5		cvv 3470	. . . . . 6 class V
6	5, 5	cxp 5664	. . . . 5 class (V × V)
7	4, 6	cres 5668	. . . 4 class (1st ↾ (V × V))
8	1, 7	ccom 5670	. . 3 class (𝐴 ∘ (1st ↾ (V × V)))
9		c2nd 7953	. . . . 5 class 2nd
10	9, 6	cres 5668	. . . 4 class (2nd ↾ (V × V))
11	2, 10	ccom 5670	. . 3 class (𝐵 ∘ (2nd ↾ (V × V)))
12	8, 11	ctxp 34616	. 2 class ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
13	3, 12	wceq 1541	1 wff pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))

This definition is referenced by:  dfpprod2  34668  pprodss4v  34670  brpprod  34671