Metamath Proof Explorer


Theorem 4atexlemc

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 4atexlemc φ C A

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 4 latmcom K Lat Q ˙ T Base K P ˙ S Base K Q ˙ T ˙ P ˙ S = P ˙ S ˙ Q ˙ T
15 10 11 12 14 syl3anc φ Q ˙ T ˙ P ˙ S = P ˙ S ˙ Q ˙ T
16 9 15 syl5eq φ C = P ˙ S ˙ Q ˙ T
17 1 4atexlemk φ K HL
18 1 4atexlemp φ P A
19 1 4atexlems φ S A
20 1 4atexlemq φ Q A
21 1 4atexlemt φ T A
22 1 2 3 5 4atexlempns φ P S
23 1 2 3 4 5 6 7 8 4atexlemntlpq φ ¬ T ˙ P ˙ Q
24 2 3 5 atnlej2 K HL T A P A Q A ¬ T ˙ P ˙ Q T Q
25 24 necomd K HL T A P A Q A ¬ T ˙ P ˙ Q Q T
26 17 21 18 20 23 25 syl131anc φ Q T
27 1 4atexlempnq φ P Q
28 1 4atexlemnslpq φ ¬ S ˙ P ˙ Q
29 2 3 5 4atlem0ae K HL P A Q A S A P Q ¬ S ˙ P ˙ Q ¬ Q ˙ P ˙ S
30 17 18 20 19 27 28 29 syl132anc φ ¬ Q ˙ P ˙ S
31 13 5 atbase T A T Base K
32 21 31 syl φ T Base K
33 1 2 3 4 5 6 7 4atexlemu φ U A
34 1 2 3 4 5 6 7 8 4atexlemv φ V A
35 13 3 5 hlatjcl K HL U A V A U ˙ V Base K
36 17 33 34 35 syl3anc φ U ˙ V Base K
37 13 5 atbase Q A Q Base K
38 20 37 syl φ Q Base K
39 13 3 latjcl K Lat P ˙ S Base K Q Base K P ˙ S ˙ Q Base K
40 10 12 38 39 syl3anc φ P ˙ S ˙ Q Base K
41 1 4atexlemkc φ K CvLat
42 1 2 3 4 5 6 7 8 4atexlemunv φ U V
43 1 4atexlemutvt φ U ˙ T = V ˙ T
44 5 2 3 cvlsupr4 K CvLat U A V A T A U V U ˙ T = V ˙ T T ˙ U ˙ V
45 41 33 34 21 42 43 44 syl132anc φ T ˙ U ˙ V
46 13 3 5 hlatjcl K HL P A Q A P ˙ Q Base K
47 17 18 20 46 syl3anc φ P ˙ Q Base K
48 1 6 4atexlemwb φ W Base K
49 13 2 4 latmle1 K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W ˙ P ˙ Q
50 10 47 48 49 syl3anc φ P ˙ Q ˙ W ˙ P ˙ Q
51 7 50 eqbrtrid φ U ˙ P ˙ Q
52 13 2 4 latmle1 K Lat P ˙ S Base K W Base K P ˙ S ˙ W ˙ P ˙ S
53 10 12 48 52 syl3anc φ P ˙ S ˙ W ˙ P ˙ S
54 8 53 eqbrtrid φ V ˙ P ˙ S
55 13 5 atbase U A U Base K
56 33 55 syl φ U Base K
57 13 5 atbase V A V Base K
58 34 57 syl φ V Base K
59 13 2 3 latjlej12 K Lat U Base K P ˙ Q Base K V Base K P ˙ S Base K U ˙ P ˙ Q V ˙ P ˙ S U ˙ V ˙ P ˙ Q ˙ P ˙ S
60 10 56 47 58 12 59 syl122anc φ U ˙ P ˙ Q V ˙ P ˙ S U ˙ V ˙ P ˙ Q ˙ P ˙ S
61 51 54 60 mp2and φ U ˙ V ˙ P ˙ Q ˙ P ˙ S
62 3 5 hlatjass K HL P A Q A S A P ˙ Q ˙ S = P ˙ Q ˙ S
63 17 18 20 19 62 syl13anc φ P ˙ Q ˙ S = P ˙ Q ˙ S
64 13 5 atbase P A P Base K
65 18 64 syl φ P Base K
66 13 5 atbase S A S Base K
67 19 66 syl φ S Base K
68 13 3 latj32 K Lat P Base K Q Base K S Base K P ˙ Q ˙ S = P ˙ S ˙ Q
69 10 65 38 67 68 syl13anc φ P ˙ Q ˙ S = P ˙ S ˙ Q
70 13 3 latjjdi K Lat P Base K Q Base K S Base K P ˙ Q ˙ S = P ˙ Q ˙ P ˙ S
71 10 65 38 67 70 syl13anc φ P ˙ Q ˙ S = P ˙ Q ˙ P ˙ S
72 63 69 71 3eqtr3rd φ P ˙ Q ˙ P ˙ S = P ˙ S ˙ Q
73 61 72 breqtrd φ U ˙ V ˙ P ˙ S ˙ Q
74 13 2 10 32 36 40 45 73 lattrd φ T ˙ P ˙ S ˙ Q
75 2 3 4 5 2atmat K HL P A S A Q A T A P S Q T ¬ Q ˙ P ˙ S T ˙ P ˙ S ˙ Q P ˙ S ˙ Q ˙ T A
76 17 18 19 20 21 22 26 30 74 75 syl333anc φ P ˙ S ˙ Q ˙ T A
77 16 76 eqeltrd φ C A