Metamath Proof Explorer


Theorem cdlemefrs29bpre0

Description: TODO fix comment. (Contributed by NM, 29-Mar-2013)

Ref Expression
Hypotheses cdlemefrs27.b B=BaseK
cdlemefrs27.l ˙=K
cdlemefrs27.j ˙=joinK
cdlemefrs27.m ˙=meetK
cdlemefrs27.a A=AtomsK
cdlemefrs27.h H=LHypK
cdlemefrs27.eq s=Rφψ
cdlemefrs27.nb KHLWHPA¬P˙WQA¬Q˙WPQsA¬s˙WφNB
Assertion cdlemefrs29bpre0 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=Rz=N˙R˙Wz=R/sN

Proof

Step Hyp Ref Expression
1 cdlemefrs27.b B=BaseK
2 cdlemefrs27.l ˙=K
3 cdlemefrs27.j ˙=joinK
4 cdlemefrs27.m ˙=meetK
5 cdlemefrs27.a A=AtomsK
6 cdlemefrs27.h H=LHypK
7 cdlemefrs27.eq s=Rφψ
8 cdlemefrs27.nb KHLWHPA¬P˙WQA¬Q˙WPQsA¬s˙WφNB
9 df-ral sA¬s˙Wφs˙R˙W=Rz=N˙R˙WssA¬s˙Wφs˙R˙W=Rz=N˙R˙W
10 anass sA¬s˙Wφs˙R˙W=RsA¬s˙Wφs˙R˙W=R
11 10 imbi1i sA¬s˙Wφs˙R˙W=Rz=N˙R˙WsA¬s˙Wφs˙R˙W=Rz=N˙R˙W
12 impexp sA¬s˙Wφs˙R˙W=Rz=N˙R˙WsA¬s˙Wφs˙R˙W=Rz=N˙R˙W
13 impexp sA¬s˙Wφs˙R˙W=Rz=N˙R˙WsA¬s˙Wφs˙R˙W=Rz=N˙R˙W
14 11 12 13 3bitr3ri sA¬s˙Wφs˙R˙W=Rz=N˙R˙WsA¬s˙Wφs˙R˙W=Rz=N˙R˙W
15 simpl11 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙WφKHLWH
16 simpl2r KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙WφRA¬R˙W
17 eqid 0.K=0.K
18 2 4 17 5 6 lhpmat KHLWHRA¬R˙WR˙W=0.K
19 15 16 18 syl2anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙WφR˙W=0.K
20 19 oveq2d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=s˙0.K
21 simp11l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψKHL
22 hlol KHLKOL
23 21 22 syl KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψKOL
24 23 adantr KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙WφKOL
25 simprl KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙WφsA
26 1 5 atbase sAsB
27 25 26 syl KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙WφsB
28 1 3 17 olj01 KOLsBs˙0.K=s
29 24 27 28 syl2anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙0.K=s
30 20 29 eqtrd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=s
31 30 eqeq1d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=Rs=R
32 19 oveq2d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙WφN˙R˙W=N˙0.K
33 simpl1 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙WφKHLWHPA¬P˙WQA¬Q˙W
34 simpl2l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙WφPQ
35 simprr KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφ¬s˙Wφ
36 33 34 25 35 8 syl112anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙WφNB
37 1 3 17 olj01 KOLNBN˙0.K=N
38 24 36 37 syl2anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙WφN˙0.K=N
39 32 38 eqtrd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙WφN˙R˙W=N
40 39 eqeq2d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφz=N˙R˙Wz=N
41 31 40 imbi12d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=Rz=N˙R˙Ws=Rz=N
42 41 pm5.74da KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=Rz=N˙R˙WsA¬s˙Wφs=Rz=N
43 impexp sA¬s˙Wφs=Rz=NsA¬s˙Wφs=Rz=N
44 simp2rl KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψRA
45 simp2rr KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙Wψ¬R˙W
46 simp3 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙Wψψ
47 eleq1 s=RsARA
48 breq1 s=Rs˙WR˙W
49 48 notbid s=R¬s˙W¬R˙W
50 49 7 anbi12d s=R¬s˙Wφ¬R˙Wψ
51 47 50 anbi12d s=RsA¬s˙WφRA¬R˙Wψ
52 51 biimprcd RA¬R˙Wψs=RsA¬s˙Wφ
53 44 45 46 52 syl12anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙Wψs=RsA¬s˙Wφ
54 53 pm4.71rd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙Wψs=RsA¬s˙Wφs=R
55 54 imbi1d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙Wψs=Rz=NsA¬s˙Wφs=Rz=N
56 eqcom z=NN=z
57 56 imbi2i s=Rz=Ns=RN=z
58 55 57 bitr3di KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs=Rz=Ns=RN=z
59 43 58 bitr3id KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs=Rz=Ns=RN=z
60 42 59 bitrd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=Rz=N˙R˙Ws=RN=z
61 14 60 syl5bb KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=Rz=N˙R˙Ws=RN=z
62 61 albidv KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψssA¬s˙Wφs˙R˙W=Rz=N˙R˙Wss=RN=z
63 9 62 syl5bb KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=Rz=N˙R˙Wss=RN=z
64 nfcv _sz
65 64 csbiebg RAss=RN=zR/sN=z
66 44 65 syl KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙Wψss=RN=zR/sN=z
67 eqcom R/sN=zz=R/sN
68 66 67 bitrdi KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙Wψss=RN=zz=R/sN
69 63 68 bitrd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WψsA¬s˙Wφs˙R˙W=Rz=N˙R˙Wz=R/sN