Metamath Proof Explorer

Theorem dalem39

Description: Lemma for dath . Auxiliary atoms G , H , and I are not colinear. (Contributed by NM, 4-Aug-2012)

Ref Expression
Hypotheses dalem.ph ⊢ φ ↔ K ∈ HL ∧ C ∈ Base K ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A ∧ T ∈ A ∧ U ∈ A ∧ Y ∈ O ∧ Z ∈ O ∧ ¬ C ≤ ˙ P ∨ ˙ Q ∧ ¬ C ≤ ˙ Q ∨ ˙ R ∧ ¬ C ≤ ˙ R ∨ ˙ P ∧ ¬ C ≤ ˙ S ∨ ˙ T ∧ ¬ C ≤ ˙ T ∨ ˙ U ∧ ¬ C ≤ ˙ U ∨ ˙ S ∧ C ≤ ˙ P ∨ ˙ S ∧ C ≤ ˙ Q ∨ ˙ T ∧ C ≤ ˙ R ∨ ˙ U
dalem.l ⊢ ≤ ˙ = ≤ K
dalem.j ⊢ ∨ ˙ = join ⁡ K
dalem.a ⊢ A = Atoms ⁡ K
dalem.ps ⊢ ψ ↔ c ∈ A ∧ d ∈ A ∧ ¬ c ≤ ˙ Y ∧ d ≠ c ∧ ¬ d ≤ ˙ Y ∧ C ≤ ˙ c ∨ ˙ d
dalem38.m ⊢ ∧ ˙ = meet ⁡ K
dalem38.o ⊢ O = LPlanes ⁡ K
dalem38.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
dalem38.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
dalem38.g ⊢ G = c ∨ ˙ P ∧ ˙ d ∨ ˙ S
dalem38.h ⊢ H = c ∨ ˙ Q ∧ ˙ d ∨ ˙ T
dalem38.i ⊢ I = c ∨ ˙ R ∧ ˙ d ∨ ˙ U
Assertion dalem39 ⊢ φ ∧ Y = Z ∧ ψ → ¬ H ≤ ˙ I ∨ ˙ G

Proof

Step Hyp Ref Expression
1 dalem.ph ⊢ φ ↔ K ∈ HL ∧ C ∈ Base K ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A ∧ T ∈ A ∧ U ∈ A ∧ Y ∈ O ∧ Z ∈ O ∧ ¬ C ≤ ˙ P ∨ ˙ Q ∧ ¬ C ≤ ˙ Q ∨ ˙ R ∧ ¬ C ≤ ˙ R ∨ ˙ P ∧ ¬ C ≤ ˙ S ∨ ˙ T ∧ ¬ C ≤ ˙ T ∨ ˙ U ∧ ¬ C ≤ ˙ U ∨ ˙ S ∧ C ≤ ˙ P ∨ ˙ S ∧ C ≤ ˙ Q ∨ ˙ T ∧ C ≤ ˙ R ∨ ˙ U
2 dalem.l ⊢ ≤ ˙ = ≤ K
3 dalem.j ⊢ ∨ ˙ = join ⁡ K
4 dalem.a ⊢ A = Atoms ⁡ K
5 dalem.ps ⊢ ψ ↔ c ∈ A ∧ d ∈ A ∧ ¬ c ≤ ˙ Y ∧ d ≠ c ∧ ¬ d ≤ ˙ Y ∧ C ≤ ˙ c ∨ ˙ d
6 dalem38.m ⊢ ∧ ˙ = meet ⁡ K
7 dalem38.o ⊢ O = LPlanes ⁡ K
8 dalem38.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
9 dalem38.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
10 dalem38.g ⊢ G = c ∨ ˙ P ∧ ˙ d ∨ ˙ S
11 dalem38.h ⊢ H = c ∨ ˙ Q ∧ ˙ d ∨ ˙ T
12 dalem38.i ⊢ I = c ∨ ˙ R ∧ ˙ d ∨ ˙ U
13 1 dalemkehl ⊢ φ → K ∈ HL
14 13 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → K ∈ HL
15 1 dalemyeo ⊢ φ → Y ∈ O
16 15 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → Y ∈ O
17 5 dalemccea ⊢ ψ → c ∈ A
18 17 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → c ∈ A
19 5 dalem-ccly ⊢ ψ → ¬ c ≤ ˙ Y
20 19 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → ¬ c ≤ ˙ Y
21 eqid ⊢ LVols ⁡ K = LVols ⁡ K
22 2 3 4 7 21 lvoli3 ⊢ K ∈ HL ∧ Y ∈ O ∧ c ∈ A ∧ ¬ c ≤ ˙ Y → Y ∨ ˙ c ∈ LVols ⁡ K
23 14 16 18 20 22 syl31anc ⊢ φ ∧ Y = Z ∧ ψ → Y ∨ ˙ c ∈ LVols ⁡ K
24 1 2 3 4 5 6 7 8 9 12 dalem34 ⊢ φ ∧ Y = Z ∧ ψ → I ∈ A
25 1 2 3 4 5 6 7 8 9 10 dalem23 ⊢ φ ∧ Y = Z ∧ ψ → G ∈ A
26 2 3 4 21 lvolnle3at ⊢ K ∈ HL ∧ Y ∨ ˙ c ∈ LVols ⁡ K ∧ I ∈ A ∧ G ∈ A ∧ c ∈ A → ¬ Y ∨ ˙ c ≤ ˙ I ∨ ˙ G ∨ ˙ c
27 14 23 24 25 18 26 syl23anc ⊢ φ ∧ Y = Z ∧ ψ → ¬ Y ∨ ˙ c ≤ ˙ I ∨ ˙ G ∨ ˙ c
28 1 2 3 4 5 6 7 8 9 10 11 12 dalem38 ⊢ φ ∧ Y = Z ∧ ψ → Y ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c
29 1 dalemkelat ⊢ φ → K ∈ Lat
30 29 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → K ∈ Lat
31 1 2 3 4 5 6 7 8 9 11 dalem29 ⊢ φ ∧ Y = Z ∧ ψ → H ∈ A
32 eqid ⊢ Base K = Base K
33 32 3 4 hlatjcl ⊢ K ∈ HL ∧ G ∈ A ∧ H ∈ A → G ∨ ˙ H ∈ Base K
34 14 25 31 33 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∈ Base K
35 32 4 atbase ⊢ I ∈ A → I ∈ Base K
36 24 35 syl ⊢ φ ∧ Y = Z ∧ ψ → I ∈ Base K
37 32 3 latjcl ⊢ K ∈ Lat ∧ G ∨ ˙ H ∈ Base K ∧ I ∈ Base K → G ∨ ˙ H ∨ ˙ I ∈ Base K
38 30 34 36 37 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∨ ˙ I ∈ Base K
39 5 4 dalemcceb ⊢ ψ → c ∈ Base K
40 39 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → c ∈ Base K
41 32 2 3 latlej2 ⊢ K ∈ Lat ∧ G ∨ ˙ H ∨ ˙ I ∈ Base K ∧ c ∈ Base K → c ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c
42 30 38 40 41 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → c ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c
43 1 7 dalemyeb ⊢ φ → Y ∈ Base K
44 43 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → Y ∈ Base K
45 32 3 latjcl ⊢ K ∈ Lat ∧ G ∨ ˙ H ∨ ˙ I ∈ Base K ∧ c ∈ Base K → G ∨ ˙ H ∨ ˙ I ∨ ˙ c ∈ Base K
46 30 38 40 45 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∨ ˙ I ∨ ˙ c ∈ Base K
47 32 2 3 latjle12 ⊢ K ∈ Lat ∧ Y ∈ Base K ∧ c ∈ Base K ∧ G ∨ ˙ H ∨ ˙ I ∨ ˙ c ∈ Base K → Y ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c ∧ c ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c ↔ Y ∨ ˙ c ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c
48 30 44 40 46 47 syl13anc ⊢ φ ∧ Y = Z ∧ ψ → Y ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c ∧ c ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c ↔ Y ∨ ˙ c ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c
49 28 42 48 mpbi2and ⊢ φ ∧ Y = Z ∧ ψ → Y ∨ ˙ c ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c
50 3 4 hlatjrot ⊢ K ∈ HL ∧ G ∈ A ∧ H ∈ A ∧ I ∈ A → G ∨ ˙ H ∨ ˙ I = I ∨ ˙ G ∨ ˙ H
51 14 25 31 24 50 syl13anc ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∨ ˙ I = I ∨ ˙ G ∨ ˙ H
52 51 oveq1d ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∨ ˙ I ∨ ˙ c = I ∨ ˙ G ∨ ˙ H ∨ ˙ c
53 49 52 breqtrd ⊢ φ ∧ Y = Z ∧ ψ → Y ∨ ˙ c ≤ ˙ I ∨ ˙ G ∨ ˙ H ∨ ˙ c
54 53 adantr ⊢ φ ∧ Y = Z ∧ ψ ∧ H ≤ ˙ I ∨ ˙ G → Y ∨ ˙ c ≤ ˙ I ∨ ˙ G ∨ ˙ H ∨ ˙ c
55 32 4 atbase ⊢ H ∈ A → H ∈ Base K
56 31 55 syl ⊢ φ ∧ Y = Z ∧ ψ → H ∈ Base K
57 32 3 4 hlatjcl ⊢ K ∈ HL ∧ I ∈ A ∧ G ∈ A → I ∨ ˙ G ∈ Base K
58 14 24 25 57 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → I ∨ ˙ G ∈ Base K
59 32 2 3 latleeqj2 ⊢ K ∈ Lat ∧ H ∈ Base K ∧ I ∨ ˙ G ∈ Base K → H ≤ ˙ I ∨ ˙ G ↔ I ∨ ˙ G ∨ ˙ H = I ∨ ˙ G
60 30 56 58 59 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → H ≤ ˙ I ∨ ˙ G ↔ I ∨ ˙ G ∨ ˙ H = I ∨ ˙ G
61 60 biimpa ⊢ φ ∧ Y = Z ∧ ψ ∧ H ≤ ˙ I ∨ ˙ G → I ∨ ˙ G ∨ ˙ H = I ∨ ˙ G
62 61 oveq1d ⊢ φ ∧ Y = Z ∧ ψ ∧ H ≤ ˙ I ∨ ˙ G → I ∨ ˙ G ∨ ˙ H ∨ ˙ c = I ∨ ˙ G ∨ ˙ c
63 54 62 breqtrd ⊢ φ ∧ Y = Z ∧ ψ ∧ H ≤ ˙ I ∨ ˙ G → Y ∨ ˙ c ≤ ˙ I ∨ ˙ G ∨ ˙ c
64 27 63 mtand ⊢ φ ∧ Y = Z ∧ ψ → ¬ H ≤ ˙ I ∨ ˙ G