Metamath Proof Explorer


Theorem 4atexlemtlw

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
Assertion 4atexlemtlw φ T ˙ 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 eqid Base K = Base K
10 1 4atexlemkl φ K Lat
11 1 4atexlemt φ T A
12 9 5 atbase T A T Base K
13 11 12 syl φ T Base K
14 1 4atexlemk φ K HL
15 1 2 3 4 5 6 7 4atexlemu φ U A
16 1 2 3 4 5 6 7 8 4atexlemv φ V A
17 9 3 5 hlatjcl K HL U A V A U ˙ V Base K
18 14 15 16 17 syl3anc φ U ˙ V Base K
19 1 6 4atexlemwb φ W Base K
20 1 4atexlemkc φ K CvLat
21 1 2 3 4 5 6 7 8 4atexlemunv φ U V
22 1 4atexlemutvt φ U ˙ T = V ˙ T
23 5 2 3 cvlsupr4 K CvLat U A V A T A U V U ˙ T = V ˙ T T ˙ U ˙ V
24 20 15 16 11 21 22 23 syl132anc φ T ˙ U ˙ V
25 1 4atexlemp φ P A
26 1 4atexlemq φ Q A
27 9 3 5 hlatjcl K HL P A Q A P ˙ Q Base K
28 14 25 26 27 syl3anc φ P ˙ Q Base K
29 9 2 4 latmle2 K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W ˙ W
30 10 28 19 29 syl3anc φ P ˙ Q ˙ W ˙ W
31 7 30 eqbrtrid φ U ˙ W
32 1 3 5 4atexlempsb φ P ˙ S Base K
33 9 2 4 latmle2 K Lat P ˙ S Base K W Base K P ˙ S ˙ W ˙ W
34 10 32 19 33 syl3anc φ P ˙ S ˙ W ˙ W
35 8 34 eqbrtrid φ V ˙ W
36 9 5 atbase U A U Base K
37 15 36 syl φ U Base K
38 9 5 atbase V A V Base K
39 16 38 syl φ V Base K
40 9 2 3 latjle12 K Lat U Base K V Base K W Base K U ˙ W V ˙ W U ˙ V ˙ W
41 10 37 39 19 40 syl13anc φ U ˙ W V ˙ W U ˙ V ˙ W
42 31 35 41 mpbi2and φ U ˙ V ˙ W
43 9 2 10 13 18 19 24 42 lattrd φ T ˙ W