Metamath Proof Explorer


Theorem cdlemg2m

Description: TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013)

Ref Expression
Hypotheses cdlemg2inv.h H=LHypK
cdlemg2inv.t T=LTrnKW
cdlemg2j.l ˙=K
cdlemg2j.j ˙=joinK
cdlemg2j.a A=AtomsK
cdlemg2j.m ˙=meetK
cdlemg2j.u U=P˙Q˙W
Assertion cdlemg2m KHLWHPA¬P˙WQA¬Q˙WFTFP˙FQ˙W=U

Proof

Step Hyp Ref Expression
1 cdlemg2inv.h H=LHypK
2 cdlemg2inv.t T=LTrnKW
3 cdlemg2j.l ˙=K
4 cdlemg2j.j ˙=joinK
5 cdlemg2j.a A=AtomsK
6 cdlemg2j.m ˙=meetK
7 cdlemg2j.u U=P˙Q˙W
8 1 2 3 4 5 6 7 cdlemg2k KHLWHPA¬P˙WQA¬Q˙WFTFP˙FQ=FP˙U
9 8 oveq1d KHLWHPA¬P˙WQA¬Q˙WFTFP˙FQ˙W=FP˙U˙W
10 simp1 KHLWHPA¬P˙WQA¬Q˙WFTKHLWH
11 simp3 KHLWHPA¬P˙WQA¬Q˙WFTFT
12 simp2l KHLWHPA¬P˙WQA¬Q˙WFTPA¬P˙W
13 eqid 0.K=0.K
14 3 6 13 5 1 2 ltrnmw KHLWHFTPA¬P˙WFP˙W=0.K
15 10 11 12 14 syl3anc KHLWHPA¬P˙WQA¬Q˙WFTFP˙W=0.K
16 15 oveq1d KHLWHPA¬P˙WQA¬Q˙WFTFP˙W˙U=0.K˙U
17 simp1l KHLWHPA¬P˙WQA¬Q˙WFTKHL
18 3 5 1 2 ltrnel KHLWHFTPA¬P˙WFPA¬FP˙W
19 10 11 12 18 syl3anc KHLWHPA¬P˙WQA¬Q˙WFTFPA¬FP˙W
20 19 simpld KHLWHPA¬P˙WQA¬Q˙WFTFPA
21 simp1r KHLWHPA¬P˙WQA¬Q˙WFTWH
22 simp2ll KHLWHPA¬P˙WQA¬Q˙WFTPA
23 simp2rl KHLWHPA¬P˙WQA¬Q˙WFTQA
24 eqid BaseK=BaseK
25 3 4 6 5 1 7 24 cdleme0aa KHLWHPAQAUBaseK
26 17 21 22 23 25 syl211anc KHLWHPA¬P˙WQA¬Q˙WFTUBaseK
27 24 1 lhpbase WHWBaseK
28 21 27 syl KHLWHPA¬P˙WQA¬Q˙WFTWBaseK
29 17 hllatd KHLWHPA¬P˙WQA¬Q˙WFTKLat
30 24 4 5 hlatjcl KHLPAQAP˙QBaseK
31 17 22 23 30 syl3anc KHLWHPA¬P˙WQA¬Q˙WFTP˙QBaseK
32 24 3 6 latmle2 KLatP˙QBaseKWBaseKP˙Q˙W˙W
33 29 31 28 32 syl3anc KHLWHPA¬P˙WQA¬Q˙WFTP˙Q˙W˙W
34 7 33 eqbrtrid KHLWHPA¬P˙WQA¬Q˙WFTU˙W
35 24 3 4 6 5 atmod4i2 KHLFPAUBaseKWBaseKU˙WFP˙W˙U=FP˙U˙W
36 17 20 26 28 34 35 syl131anc KHLWHPA¬P˙WQA¬Q˙WFTFP˙W˙U=FP˙U˙W
37 hlol KHLKOL
38 17 37 syl KHLWHPA¬P˙WQA¬Q˙WFTKOL
39 24 4 13 olj02 KOLUBaseK0.K˙U=U
40 38 26 39 syl2anc KHLWHPA¬P˙WQA¬Q˙WFT0.K˙U=U
41 16 36 40 3eqtr3d KHLWHPA¬P˙WQA¬Q˙WFTFP˙U˙W=U
42 9 41 eqtrd KHLWHPA¬P˙WQA¬Q˙WFTFP˙FQ˙W=U