Metamath Proof Explorer


Theorem brpprod3b

Description: Condition for parallel product when the first argument is not an ordered pair. (Contributed by Scott Fenton, 3-May-2014)

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

Proof

Step Hyp Ref Expression
1 brpprod3.1 X V
2 brpprod3.2 Y V
3 brpprod3.3 Z V
4 pprodcnveq pprod R S = pprod R -1 S -1 -1
5 4 breqi X pprod R S Y Z X pprod R -1 S -1 -1 Y Z
6 opex Y Z V
7 1 6 brcnv X pprod R -1 S -1 -1 Y Z Y Z pprod R -1 S -1 X
8 2 3 1 brpprod3a Y Z pprod R -1 S -1 X z w X = z w Y R -1 z Z S -1 w
9 7 8 bitri X pprod R -1 S -1 -1 Y Z z w X = z w Y R -1 z Z S -1 w
10 biid X = z w X = z w
11 vex z V
12 2 11 brcnv Y R -1 z z R Y
13 vex w V
14 3 13 brcnv Z S -1 w w S Z
15 10 12 14 3anbi123i X = z w Y R -1 z Z S -1 w X = z w z R Y w S Z
16 15 2exbii z w X = z w Y R -1 z Z S -1 w z w X = z w z R Y w S Z
17 9 16 bitri X pprod R -1 S -1 -1 Y Z z w X = z w z R Y w S Z
18 5 17 bitri X pprod R S Y Z z w X = z w z R Y w S Z