Theorem dfpprod2 36393

Description: Expanded definition of parallel product. (Contributed by Scott Fenton, 3-May-2014.)

Assertion

Ref	Expression
dfpprod2	⊢ pprod(𝐴, 𝐵) = ((◡(1st ↾ (V × V)) ∘ (𝐴 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐵 ∘ (2nd ↾ (V × V)))))

Proof of Theorem dfpprod2

Step	Hyp	Ref	Expression
1		df-pprod 36366	. 2 ⊢ pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
2		df-txp 36365	. 2 ⊢ ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V)))) = ((◡(1st ↾ (V × V)) ∘ (𝐴 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐵 ∘ (2nd ↾ (V × V)))))
3	1, 2	eqtri 2789	1 ⊢ pprod(𝐴, 𝐵) = ((◡(1st ↾ (V × V)) ∘ (𝐴 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐵 ∘ (2nd ↾ (V × V)))))

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3458   ∩ cin 3907   × cxp 5664  ^◡ccnv 5665   ↾ cres 5668   ∘ ccom 5670  1^st c1st 7993  2^nd c2nd 7994   ⊗ ctxp 36341  pprodcpprod 36342

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-txp 36365  df-pprod 36366

This theorem is used by:  pprodcnveq  36394