Definition df-pprod 5739

Description: Define the parallel product operation. (Contributed by SF, 9-Feb-2015.)

Assertion

Ref	Expression
df-pprod	⊢ PProd (A, B) = ((A ∘ 1st ) ⊗ (B ∘ 2nd ))

Detailed syntax breakdown of Definition df-pprod

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cpprod 5738	. 2 class PProd (A, B)
4		c1st 4718	. . . 4 class 1st
5	1, 4	ccom 4722	. . 3 class (A ∘ 1st )
6		c2nd 4784	. . . 4 class 2nd
7	2, 6	ccom 4722	. . 3 class (B ∘ 2nd )
8	5, 7	ctxp 5736	. 2 class ((A ∘ 1st ) ⊗ (B ∘ 2nd ))
9	3, 8	wceq 1642	1 wff PProd (A, B) = ((A ∘ 1st ) ⊗ (B ∘ 2nd ))

This definition is referenced by:  pprodeq1  5835  pprodeq2  5836  qrpprod  5837  pprodexg  5838  brpprod  5840  cnvpprod  5842