Metamath Proof Explorer


Theorem erov

Description: The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 30-Dec-2014)

Ref Expression
Hypotheses eropr.1 J=A/R
eropr.2 K=B/S
eropr.3 φTZ
eropr.4 φRErU
eropr.5 φSErV
eropr.6 φTErW
eropr.7 φAU
eropr.8 φBV
eropr.9 φCW
eropr.10 φ+˙:A×BC
eropr.11 φrAsAtBuBrRstSur+˙tTs+˙u
eropr.12 ˙=xyz|pAqBx=pRy=qSz=p+˙qT
eropr.13 φRX
eropr.14 φSY
Assertion erov φPAQBPR˙QS=P+˙QT

Proof

Step Hyp Ref Expression
1 eropr.1 J=A/R
2 eropr.2 K=B/S
3 eropr.3 φTZ
4 eropr.4 φRErU
5 eropr.5 φSErV
6 eropr.6 φTErW
7 eropr.7 φAU
8 eropr.8 φBV
9 eropr.9 φCW
10 eropr.10 φ+˙:A×BC
11 eropr.11 φrAsAtBuBrRstSur+˙tTs+˙u
12 eropr.12 ˙=xyz|pAqBx=pRy=qSz=p+˙qT
13 eropr.13 φRX
14 eropr.14 φSY
15 1 2 3 4 5 6 7 8 9 10 11 12 erovlem φ˙=xJ,yKιz|pAqBx=pRy=qSz=p+˙qT
16 15 3ad2ant1 φPAQB˙=xJ,yKιz|pAqBx=pRy=qSz=p+˙qT
17 simprl φPAQBx=PRy=QSx=PR
18 17 eqeq1d φPAQBx=PRy=QSx=pRPR=pR
19 simprr φPAQBx=PRy=QSy=QS
20 19 eqeq1d φPAQBx=PRy=QSy=qSQS=qS
21 18 20 anbi12d φPAQBx=PRy=QSx=pRy=qSPR=pRQS=qS
22 21 anbi1d φPAQBx=PRy=QSx=pRy=qSz=p+˙qTPR=pRQS=qSz=p+˙qT
23 22 2rexbidv φPAQBx=PRy=QSpAqBx=pRy=qSz=p+˙qTpAqBPR=pRQS=qSz=p+˙qT
24 23 iotabidv φPAQBx=PRy=QSιz|pAqBx=pRy=qSz=p+˙qT=ιz|pAqBPR=pRQS=qSz=p+˙qT
25 ecelqsg RXPAPRA/R
26 25 1 eleqtrrdi RXPAPRJ
27 13 26 sylan φPAPRJ
28 27 3adant3 φPAQBPRJ
29 ecelqsg SYQBQSB/S
30 29 2 eleqtrrdi SYQBQSK
31 14 30 sylan φQBQSK
32 31 3adant2 φPAQBQSK
33 iotaex ιz|pAqBPR=pRQS=qSz=p+˙qTV
34 33 a1i φPAQBιz|pAqBPR=pRQS=qSz=p+˙qTV
35 16 24 28 32 34 ovmpod φPAQBPR˙QS=ιz|pAqBPR=pRQS=qSz=p+˙qT
36 eqid PR=PR
37 eqid QS=QS
38 36 37 pm3.2i PR=PRQS=QS
39 eqid P+˙QT=P+˙QT
40 38 39 pm3.2i PR=PRQS=QSP+˙QT=P+˙QT
41 eceq1 p=PpR=PR
42 41 eqeq2d p=PPR=pRPR=PR
43 42 anbi1d p=PPR=pRQS=qSPR=PRQS=qS
44 oveq1 p=Pp+˙q=P+˙q
45 44 eceq1d p=Pp+˙qT=P+˙qT
46 45 eqeq2d p=PP+˙QT=p+˙qTP+˙QT=P+˙qT
47 43 46 anbi12d p=PPR=pRQS=qSP+˙QT=p+˙qTPR=PRQS=qSP+˙QT=P+˙qT
48 eceq1 q=QqS=QS
49 48 eqeq2d q=QQS=qSQS=QS
50 49 anbi2d q=QPR=PRQS=qSPR=PRQS=QS
51 oveq2 q=QP+˙q=P+˙Q
52 51 eceq1d q=QP+˙qT=P+˙QT
53 52 eqeq2d q=QP+˙QT=P+˙qTP+˙QT=P+˙QT
54 50 53 anbi12d q=QPR=PRQS=qSP+˙QT=P+˙qTPR=PRQS=QSP+˙QT=P+˙QT
55 47 54 rspc2ev PAQBPR=PRQS=QSP+˙QT=P+˙QTpAqBPR=pRQS=qSP+˙QT=p+˙qT
56 40 55 mp3an3 PAQBpAqBPR=pRQS=qSP+˙QT=p+˙qT
57 56 3adant1 φPAQBpAqBPR=pRQS=qSP+˙QT=p+˙qT
58 ecexg TZP+˙QTV
59 3 58 syl φP+˙QTV
60 59 3ad2ant1 φPAQBP+˙QTV
61 simp1 φPAQBφ
62 1 2 3 4 5 6 7 8 9 10 11 eroveu φPRJQSK∃!zpAqBPR=pRQS=qSz=p+˙qT
63 61 28 32 62 syl12anc φPAQB∃!zpAqBPR=pRQS=qSz=p+˙qT
64 simpr φPAQBz=P+˙QTz=P+˙QT
65 64 eqeq1d φPAQBz=P+˙QTz=p+˙qTP+˙QT=p+˙qT
66 65 anbi2d φPAQBz=P+˙QTPR=pRQS=qSz=p+˙qTPR=pRQS=qSP+˙QT=p+˙qT
67 66 2rexbidv φPAQBz=P+˙QTpAqBPR=pRQS=qSz=p+˙qTpAqBPR=pRQS=qSP+˙QT=p+˙qT
68 60 63 67 iota2d φPAQBpAqBPR=pRQS=qSP+˙QT=p+˙qTιz|pAqBPR=pRQS=qSz=p+˙qT=P+˙QT
69 57 68 mpbid φPAQBιz|pAqBPR=pRQS=qSz=p+˙qT=P+˙QT
70 35 69 eqtrd φPAQBPR˙QS=P+˙QT