Metamath Proof Explorer


Theorem cdlemeg46rjgN

Description: NOT NEEDED? TODO FIX COMMENT. r \/ g(s) = r \/ v_2 p. 115 last line. (Contributed by NM, 2-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemef46g.b B=BaseK
cdlemef46g.l ˙=K
cdlemef46g.j ˙=joinK
cdlemef46g.m ˙=meetK
cdlemef46g.a A=AtomsK
cdlemef46g.h H=LHypK
cdlemef46g.u U=P˙Q˙W
cdlemef46g.d D=t˙U˙Q˙P˙t˙W
cdlemefs46g.e E=P˙Q˙D˙s˙t˙W
cdlemef46g.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
cdlemef46.v V=Q˙P˙W
cdlemef46.n N=v˙V˙P˙Q˙v˙W
cdlemefs46.o O=Q˙P˙N˙u˙v˙W
cdlemef46.g G=aBifQP¬a˙WιcB|uA¬u˙Wu˙a˙W=ac=ifu˙Q˙PιbB|vA¬v˙W¬v˙Q˙Pb=Ou/vN˙a˙Wa
cdlemeg46.y Y=R˙GS˙W
Assertion cdlemeg46rjgN KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QR˙GS=R˙Y

Proof

Step Hyp Ref Expression
1 cdlemef46g.b B=BaseK
2 cdlemef46g.l ˙=K
3 cdlemef46g.j ˙=joinK
4 cdlemef46g.m ˙=meetK
5 cdlemef46g.a A=AtomsK
6 cdlemef46g.h H=LHypK
7 cdlemef46g.u U=P˙Q˙W
8 cdlemef46g.d D=t˙U˙Q˙P˙t˙W
9 cdlemefs46g.e E=P˙Q˙D˙s˙t˙W
10 cdlemef46g.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
11 cdlemef46.v V=Q˙P˙W
12 cdlemef46.n N=v˙V˙P˙Q˙v˙W
13 cdlemefs46.o O=Q˙P˙N˙u˙v˙W
14 cdlemef46.g G=aBifQP¬a˙WιcB|uA¬u˙Wu˙a˙W=ac=ifu˙Q˙PιbB|vA¬v˙W¬v˙Q˙Pb=Ou/vN˙a˙Wa
15 cdlemeg46.y Y=R˙GS˙W
16 eqid S˙U˙Q˙P˙S˙W=S˙U˙Q˙P˙S˙W
17 eqid P˙Q˙S˙U˙Q˙P˙S˙W˙R˙S˙W=P˙Q˙S˙U˙Q˙P˙S˙W˙R˙S˙W
18 eqid S˙V˙P˙Q˙S˙W=S˙V˙P˙Q˙S˙W
19 eqid Q˙P˙S˙V˙P˙Q˙S˙W˙P˙Q˙S˙U˙Q˙P˙S˙W˙R˙S˙W˙S˙W=Q˙P˙S˙V˙P˙Q˙S˙W˙P˙Q˙S˙U˙Q˙P˙S˙W˙R˙S˙W˙S˙W
20 eqid S˙V˙P˙Q˙S˙W˙U˙Q˙P˙S˙V˙P˙Q˙S˙W˙W=S˙V˙P˙Q˙S˙W˙U˙Q˙P˙S˙V˙P˙Q˙S˙W˙W
21 eqid P˙Q˙S˙U˙Q˙P˙S˙W˙R˙S˙W˙S˙W=P˙Q˙S˙U˙Q˙P˙S˙W˙R˙S˙W˙S˙W
22 eqid R˙S˙V˙P˙Q˙S˙W˙W=R˙S˙V˙P˙Q˙S˙W˙W
23 1 2 3 4 5 6 7 11 16 17 18 19 20 21 22 cdleme43cN KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬S˙P˙QR˙S˙V˙P˙Q˙S˙W=R˙R˙S˙V˙P˙Q˙S˙W˙W
24 23 3adant3l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QR˙S˙V˙P˙Q˙S˙W=R˙R˙S˙V˙P˙Q˙S˙W˙W
25 simp1 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QKHLWHPA¬P˙WQA¬Q˙W
26 simp21 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QPQ
27 simp23 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QSA¬S˙W
28 simp3r KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙Q¬S˙P˙Q
29 1 2 3 4 5 6 11 12 13 14 cdlemeg47b KHLWHPA¬P˙WQA¬Q˙WPQSA¬S˙W¬S˙P˙QGS=S/vN
30 25 26 27 28 29 syl121anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QGS=S/vN
31 simp23l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QSA
32 12 18 cdleme31sc SAS/vN=S˙V˙P˙Q˙S˙W
33 31 32 syl KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QS/vN=S˙V˙P˙Q˙S˙W
34 30 33 eqtrd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QGS=S˙V˙P˙Q˙S˙W
35 34 oveq2d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QR˙GS=R˙S˙V˙P˙Q˙S˙W
36 35 oveq1d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QR˙GS˙W=R˙S˙V˙P˙Q˙S˙W˙W
37 15 36 eqtrid KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QY=R˙S˙V˙P˙Q˙S˙W˙W
38 37 oveq2d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QR˙Y=R˙R˙S˙V˙P˙Q˙S˙W˙W
39 24 35 38 3eqtr4d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QR˙GS=R˙Y