Metamath Proof Explorer


Theorem 4atexlemnclw

Description: Lemma for 4atexlem7 . (Contributed by NM, 24-Nov-2012)

Ref Expression
Hypotheses 4thatlem.ph φ K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R T A U ˙ T = V ˙ T P Q ¬ S ˙ P ˙ Q
4thatlem0.l ˙ = K
4thatlem0.j ˙ = join K
4thatlem0.m ˙ = meet K
4thatlem0.a A = Atoms K
4thatlem0.h H = LHyp K
4thatlem0.u U = P ˙ Q ˙ W
4thatlem0.v V = P ˙ S ˙ W
4thatlem0.c C = Q ˙ T ˙ P ˙ S
Assertion 4atexlemnclw φ ¬ C ˙ W

Proof

Step Hyp Ref Expression
1 4thatlem.ph φ K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R T A U ˙ T = V ˙ T P Q ¬ S ˙ P ˙ Q
2 4thatlem0.l ˙ = K
3 4thatlem0.j ˙ = join K
4 4thatlem0.m ˙ = meet K
5 4thatlem0.a A = Atoms K
6 4thatlem0.h H = LHyp K
7 4thatlem0.u U = P ˙ Q ˙ W
8 4thatlem0.v V = P ˙ S ˙ W
9 4thatlem0.c C = Q ˙ T ˙ P ˙ S
10 1 4atexlemkl φ K Lat
11 1 3 5 4atexlemqtb φ Q ˙ T Base K
12 1 3 5 4atexlempsb φ P ˙ S Base K
13 eqid Base K = Base K
14 13 2 4 latmle1 K Lat Q ˙ T Base K P ˙ S Base K Q ˙ T ˙ P ˙ S ˙ Q ˙ T
15 10 11 12 14 syl3anc φ Q ˙ T ˙ P ˙ S ˙ Q ˙ T
16 9 15 eqbrtrid φ C ˙ Q ˙ T
17 simp13r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R T A U ˙ T = V ˙ T P Q ¬ S ˙ P ˙ Q ¬ Q ˙ W
18 1 17 sylbi φ ¬ Q ˙ W
19 1 4atexlemkc φ K CvLat
20 1 2 3 4 5 6 7 8 4atexlemv φ V A
21 1 4atexlemq φ Q A
22 1 4atexlemt φ T A
23 1 2 3 4 5 6 7 4atexlemu φ U A
24 1 2 3 4 5 6 7 8 4atexlemunv φ U V
25 1 4atexlemutvt φ U ˙ T = V ˙ T
26 5 3 cvlsupr6 K CvLat U A V A T A U V U ˙ T = V ˙ T T V
27 26 necomd K CvLat U A V A T A U V U ˙ T = V ˙ T V T
28 19 23 20 22 24 25 27 syl132anc φ V T
29 2 3 5 cvlatexch2 K CvLat V A Q A T A V T V ˙ Q ˙ T Q ˙ V ˙ T
30 19 20 21 22 28 29 syl131anc φ V ˙ Q ˙ T Q ˙ V ˙ T
31 1 6 4atexlemwb φ W Base K
32 13 2 4 latmle2 K Lat P ˙ S Base K W Base K P ˙ S ˙ W ˙ W
33 10 12 31 32 syl3anc φ P ˙ S ˙ W ˙ W
34 8 33 eqbrtrid φ V ˙ W
35 1 2 3 4 5 6 7 8 4atexlemtlw φ T ˙ W
36 13 5 atbase V A V Base K
37 20 36 syl φ V Base K
38 13 5 atbase T A T Base K
39 22 38 syl φ T Base K
40 13 2 3 latjle12 K Lat V Base K T Base K W Base K V ˙ W T ˙ W V ˙ T ˙ W
41 10 37 39 31 40 syl13anc φ V ˙ W T ˙ W V ˙ T ˙ W
42 34 35 41 mpbi2and φ V ˙ T ˙ W
43 13 5 atbase Q A Q Base K
44 21 43 syl φ Q Base K
45 1 4atexlemk φ K HL
46 13 3 5 hlatjcl K HL V A T A V ˙ T Base K
47 45 20 22 46 syl3anc φ V ˙ T Base K
48 13 2 lattr K Lat Q Base K V ˙ T Base K W Base K Q ˙ V ˙ T V ˙ T ˙ W Q ˙ W
49 10 44 47 31 48 syl13anc φ Q ˙ V ˙ T V ˙ T ˙ W Q ˙ W
50 42 49 mpan2d φ Q ˙ V ˙ T Q ˙ W
51 30 50 syld φ V ˙ Q ˙ T Q ˙ W
52 18 51 mtod φ ¬ V ˙ Q ˙ T
53 nbrne2 C ˙ Q ˙ T ¬ V ˙ Q ˙ T C V
54 16 52 53 syl2anc φ C V
55 1 4atexlemw φ W H
56 45 55 jca φ K HL W H
57 1 4atexlempw φ P A ¬ P ˙ W
58 1 4atexlems φ S A
59 1 2 3 4 5 6 7 8 9 4atexlemc φ C A
60 1 2 3 5 4atexlempns φ P S
61 13 2 4 latmle2 K Lat Q ˙ T Base K P ˙ S Base K Q ˙ T ˙ P ˙ S ˙ P ˙ S
62 10 11 12 61 syl3anc φ Q ˙ T ˙ P ˙ S ˙ P ˙ S
63 9 62 eqbrtrid φ C ˙ P ˙ S
64 2 3 4 5 6 8 lhpat3 K HL W H P A ¬ P ˙ W S A C A P S C ˙ P ˙ S ¬ C ˙ W C V
65 56 57 58 59 60 63 64 syl222anc φ ¬ C ˙ W C V
66 54 65 mpbird φ ¬ C ˙ W