Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pprod Structured version   Visualization version   GIF version

Definition df-pprod 32299
Description: Define the parallel product of two classes. Membership in this class is defined by pprodss4v 32328 and brpprod 32329. (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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cpprod 32275 . 2 class pprod(𝐴, 𝐵)
4 c1st 7313 . . . . 5 class 1st
5 cvv 3351 . . . . . 6 class V
65, 5cxp 5247 . . . . 5 class (V × V)
74, 6cres 5251 . . . 4 class (1st ↾ (V × V))
81, 7ccom 5253 . . 3 class (𝐴 ∘ (1st ↾ (V × V)))
9 c2nd 7314 . . . . 5 class 2nd
109, 6cres 5251 . . . 4 class (2nd ↾ (V × V))
112, 10ccom 5253 . . 3 class (𝐵 ∘ (2nd ↾ (V × V)))
128, 11ctxp 32274 . 2 class ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
133, 12wceq 1631 1 wff pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
Colors of variables: wff setvar class
This definition is referenced by:  dfpprod2  32326  pprodss4v  32328  brpprod  32329
  Copyright terms: Public domain W3C validator