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 33200
Description: Define the parallel product of two classes. Membership in this class is defined by pprodss4v 33229 and brpprod 33230. (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 33176 . 2 class pprod(𝐴, 𝐵)
4 c1st 7678 . . . . 5 class 1st
5 cvv 3500 . . . . . 6 class V
65, 5cxp 5552 . . . . 5 class (V × V)
74, 6cres 5556 . . . 4 class (1st ↾ (V × V))
81, 7ccom 5558 . . 3 class (𝐴 ∘ (1st ↾ (V × V)))
9 c2nd 7679 . . . . 5 class 2nd
109, 6cres 5556 . . . 4 class (2nd ↾ (V × V))
112, 10ccom 5558 . . 3 class (𝐵 ∘ (2nd ↾ (V × V)))
128, 11ctxp 33175 . 2 class ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
133, 12wceq 1530 1 wff pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
Colors of variables: wff setvar class
This definition is referenced by:  dfpprod2  33227  pprodss4v  33229  brpprod  33230
  Copyright terms: Public domain W3C validator