Metamath Proof Explorer


Theorem 4atexlemcnd

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
4thatlem0.d D = R ˙ T ˙ P ˙ S
Assertion 4atexlemcnd φ C D

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 4thatlem0.d D = R ˙ T ˙ P ˙ S
11 1 2 3 4 5 6 7 8 4atexlemtlw φ T ˙ W
12 1 2 3 4 5 6 7 8 9 4atexlemnclw φ ¬ C ˙ W
13 nbrne2 T ˙ W ¬ C ˙ W T C
14 11 12 13 syl2anc φ T C
15 1 4atexlemk φ K HL
16 1 4atexlemq φ Q A
17 1 4atexlemt φ T A
18 3 5 hlatjcom K HL Q A T A Q ˙ T = T ˙ Q
19 15 16 17 18 syl3anc φ Q ˙ T = T ˙ Q
20 simp221 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 R A
21 1 20 sylbi φ R A
22 3 5 hlatjcom K HL R A T A R ˙ T = T ˙ R
23 15 21 17 22 syl3anc φ R ˙ T = T ˙ R
24 19 23 oveq12d φ Q ˙ T ˙ R ˙ T = T ˙ Q ˙ T ˙ R
25 1 4atexlemkc φ K CvLat
26 1 4atexlemp φ P A
27 1 4atexlempnq φ P Q
28 simp223 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 P ˙ R = Q ˙ R
29 1 28 sylbi φ P ˙ R = Q ˙ R
30 5 3 cvlsupr6 K CvLat P A Q A R A P Q P ˙ R = Q ˙ R R Q
31 30 necomd K CvLat P A Q A R A P Q P ˙ R = Q ˙ R Q R
32 25 26 16 21 27 29 31 syl132anc φ Q R
33 1 2 3 4 5 6 7 8 4atexlemntlpq φ ¬ T ˙ P ˙ Q
34 5 3 cvlsupr7 K CvLat P A Q A R A P Q P ˙ R = Q ˙ R P ˙ Q = R ˙ Q
35 25 26 16 21 27 29 34 syl132anc φ P ˙ Q = R ˙ Q
36 3 5 hlatjcom K HL Q A R A Q ˙ R = R ˙ Q
37 15 16 21 36 syl3anc φ Q ˙ R = R ˙ Q
38 35 37 eqtr4d φ P ˙ Q = Q ˙ R
39 38 breq2d φ T ˙ P ˙ Q T ˙ Q ˙ R
40 33 39 mtbid φ ¬ T ˙ Q ˙ R
41 2 3 4 5 2llnma2 K HL Q A R A T A Q R ¬ T ˙ Q ˙ R T ˙ Q ˙ T ˙ R = T
42 15 16 21 17 32 40 41 syl132anc φ T ˙ Q ˙ T ˙ R = T
43 24 42 eqtr2d φ T = Q ˙ T ˙ R ˙ T
44 43 adantr φ C = D T = Q ˙ T ˙ R ˙ T
45 1 4atexlemkl φ K Lat
46 1 3 5 4atexlemqtb φ Q ˙ T Base K
47 1 3 5 4atexlempsb φ P ˙ S Base K
48 eqid Base K = Base K
49 48 2 4 latmle1 K Lat Q ˙ T Base K P ˙ S Base K Q ˙ T ˙ P ˙ S ˙ Q ˙ T
50 45 46 47 49 syl3anc φ Q ˙ T ˙ P ˙ S ˙ Q ˙ T
51 9 50 eqbrtrid φ C ˙ Q ˙ T
52 51 adantr φ C = D C ˙ Q ˙ T
53 simpr φ C = D C = D
54 48 3 5 hlatjcl K HL R A T A R ˙ T Base K
55 15 21 17 54 syl3anc φ R ˙ T Base K
56 48 2 4 latmle1 K Lat R ˙ T Base K P ˙ S Base K R ˙ T ˙ P ˙ S ˙ R ˙ T
57 45 55 47 56 syl3anc φ R ˙ T ˙ P ˙ S ˙ R ˙ T
58 10 57 eqbrtrid φ D ˙ R ˙ T
59 58 adantr φ C = D D ˙ R ˙ T
60 53 59 eqbrtrd φ C = D C ˙ R ˙ T
61 1 2 3 4 5 6 7 8 9 4atexlemc φ C A
62 48 5 atbase C A C Base K
63 61 62 syl φ C Base K
64 48 2 4 latlem12 K Lat C Base K Q ˙ T Base K R ˙ T Base K C ˙ Q ˙ T C ˙ R ˙ T C ˙ Q ˙ T ˙ R ˙ T
65 45 63 46 55 64 syl13anc φ C ˙ Q ˙ T C ˙ R ˙ T C ˙ Q ˙ T ˙ R ˙ T
66 65 adantr φ C = D C ˙ Q ˙ T C ˙ R ˙ T C ˙ Q ˙ T ˙ R ˙ T
67 52 60 66 mpbi2and φ C = D C ˙ Q ˙ T ˙ R ˙ T
68 hlatl K HL K AtLat
69 15 68 syl φ K AtLat
70 43 17 eqeltrrd φ Q ˙ T ˙ R ˙ T A
71 2 5 atcmp K AtLat C A Q ˙ T ˙ R ˙ T A C ˙ Q ˙ T ˙ R ˙ T C = Q ˙ T ˙ R ˙ T
72 69 61 70 71 syl3anc φ C ˙ Q ˙ T ˙ R ˙ T C = Q ˙ T ˙ R ˙ T
73 72 adantr φ C = D C ˙ Q ˙ T ˙ R ˙ T C = Q ˙ T ˙ R ˙ T
74 67 73 mpbid φ C = D C = Q ˙ T ˙ R ˙ T
75 44 74 eqtr4d φ C = D T = C
76 75 ex φ C = D T = C
77 76 necon3d φ T C C D
78 14 77 mpd φ C D