Metamath Proof Explorer


Theorem cdlemg12a

Description: TODO: FIX COMMENT. (Contributed by NM, 5-May-2013)

Ref Expression
Hypotheses cdlemg12.l ˙ = K
cdlemg12.j ˙ = join K
cdlemg12.m ˙ = meet K
cdlemg12.a A = Atoms K
cdlemg12.h H = LHyp K
cdlemg12.t T = LTrn K W
cdlemg12.u U = P ˙ Q ˙ W
Assertion cdlemg12a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U P ˙ U ˙ G P ˙ U ˙ F G P ˙ U

Proof

Step Hyp Ref Expression
1 cdlemg12.l ˙ = K
2 cdlemg12.j ˙ = join K
3 cdlemg12.m ˙ = meet K
4 cdlemg12.a A = Atoms K
5 cdlemg12.h H = LHyp K
6 cdlemg12.t T = LTrn K W
7 cdlemg12.u U = P ˙ Q ˙ W
8 simp1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U K HL
9 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U P A
10 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U K HL W H
11 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U G T
12 1 4 5 6 ltrnat K HL W H G T P A G P A
13 10 11 9 12 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U G P A
14 simp1r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U W H
15 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U P A ¬ P ˙ W
16 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U Q A
17 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U P Q
18 1 2 3 4 5 7 cdleme0a K HL W H P A ¬ P ˙ W Q A P Q U A
19 8 14 15 16 17 18 syl212anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U U A
20 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U P ˙ U G P ˙ U
21 1 2 3 4 2llnma3r K HL P A G P A U A P ˙ U G P ˙ U P ˙ U ˙ G P ˙ U = U
22 8 9 13 19 20 21 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U P ˙ U ˙ G P ˙ U = U
23 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U F T
24 1 4 5 6 ltrncoat K HL W H F T G T P A F G P A
25 10 23 11 9 24 syl121anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U F G P A
26 1 2 4 hlatlej2 K HL F G P A U A U ˙ F G P ˙ U
27 8 25 19 26 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U U ˙ F G P ˙ U
28 22 27 eqbrtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ U G P ˙ U P ˙ U ˙ G P ˙ U ˙ F G P ˙ U