Metamath Proof Explorer


Theorem brpprod3a

Description: Condition for parallel product when the last argument is not an ordered pair. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brpprod3.1 X V
brpprod3.2 Y V
brpprod3.3 Z V
Assertion brpprod3a X Y pprod R S Z z w Z = z w X R z Y S w

Proof

Step Hyp Ref Expression
1 brpprod3.1 X V
2 brpprod3.2 Y V
3 brpprod3.3 Z V
4 pprodss4v pprod R S V × V × V × V
5 4 brel X Y pprod R S Z X Y V × V Z V × V
6 5 simprd X Y pprod R S Z Z V × V
7 elvv Z V × V z w Z = z w
8 6 7 sylib X Y pprod R S Z z w Z = z w
9 8 pm4.71ri X Y pprod R S Z z w Z = z w X Y pprod R S Z
10 19.41vv z w Z = z w X Y pprod R S Z z w Z = z w X Y pprod R S Z
11 9 10 bitr4i X Y pprod R S Z z w Z = z w X Y pprod R S Z
12 breq2 Z = z w X Y pprod R S Z X Y pprod R S z w
13 12 pm5.32i Z = z w X Y pprod R S Z Z = z w X Y pprod R S z w
14 13 2exbii z w Z = z w X Y pprod R S Z z w Z = z w X Y pprod R S z w
15 vex z V
16 vex w V
17 1 2 15 16 brpprod X Y pprod R S z w X R z Y S w
18 17 anbi2i Z = z w X Y pprod R S z w Z = z w X R z Y S w
19 3anass Z = z w X R z Y S w Z = z w X R z Y S w
20 18 19 bitr4i Z = z w X Y pprod R S z w Z = z w X R z Y S w
21 20 2exbii z w Z = z w X Y pprod R S z w z w Z = z w X R z Y S w
22 11 14 21 3bitri X Y pprod R S Z z w Z = z w X R z Y S w