Metamath Proof Explorer

Theorem dalem38

Description: Lemma for dath . Plane Y belongs to the 3-dimensional volume G H I c . (Contributed by NM, 5-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 dalem38 ⊢ φ ∧ Y = Z ∧ ψ → Y ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c

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 2 3 4 5 6 7 8 9 10 dalem28 ⊢ φ ∧ Y = Z ∧ ψ → P ≤ ˙ G ∨ ˙ c
14 1 2 3 4 5 6 7 8 9 11 dalem33 ⊢ φ ∧ Y = Z ∧ ψ → Q ≤ ˙ H ∨ ˙ c
15 1 dalemkelat ⊢ φ → K ∈ Lat
16 15 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → K ∈ Lat
17 1 4 dalempeb ⊢ φ → P ∈ Base K
18 17 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → P ∈ Base K
19 1 dalemkehl ⊢ φ → K ∈ HL
20 19 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → K ∈ HL
21 1 2 3 4 5 6 7 8 9 10 dalem23 ⊢ φ ∧ Y = Z ∧ ψ → G ∈ A
22 5 dalemccea ⊢ ψ → c ∈ A
23 22 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → c ∈ A
24 eqid ⊢ Base K = Base K
25 24 3 4 hlatjcl ⊢ K ∈ HL ∧ G ∈ A ∧ c ∈ A → G ∨ ˙ c ∈ Base K
26 20 21 23 25 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ c ∈ Base K
27 1 4 dalemqeb ⊢ φ → Q ∈ Base K
28 27 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → Q ∈ Base K
29 1 2 3 4 5 6 7 8 9 11 dalem29 ⊢ φ ∧ Y = Z ∧ ψ → H ∈ A
30 24 3 4 hlatjcl ⊢ K ∈ HL ∧ H ∈ A ∧ c ∈ A → H ∨ ˙ c ∈ Base K
31 20 29 23 30 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → H ∨ ˙ c ∈ Base K
32 24 2 3 latjlej12 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ G ∨ ˙ c ∈ Base K ∧ Q ∈ Base K ∧ H ∨ ˙ c ∈ Base K → P ≤ ˙ G ∨ ˙ c ∧ Q ≤ ˙ H ∨ ˙ c → P ∨ ˙ Q ≤ ˙ G ∨ ˙ c ∨ ˙ H ∨ ˙ c
33 16 18 26 28 31 32 syl122anc ⊢ φ ∧ Y = Z ∧ ψ → P ≤ ˙ G ∨ ˙ c ∧ Q ≤ ˙ H ∨ ˙ c → P ∨ ˙ Q ≤ ˙ G ∨ ˙ c ∨ ˙ H ∨ ˙ c
34 13 14 33 mp2and ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ Q ≤ ˙ G ∨ ˙ c ∨ ˙ H ∨ ˙ c
35 24 4 atbase ⊢ G ∈ A → G ∈ Base K
36 21 35 syl ⊢ φ ∧ Y = Z ∧ ψ → G ∈ Base K
37 24 4 atbase ⊢ H ∈ A → H ∈ Base K
38 29 37 syl ⊢ φ ∧ Y = Z ∧ ψ → H ∈ Base K
39 5 4 dalemcceb ⊢ ψ → c ∈ Base K
40 39 3ad2ant3 ⊢ φ ∧ Y = Z ∧ ψ → c ∈ Base K
41 24 3 latjjdir ⊢ K ∈ Lat ∧ G ∈ Base K ∧ H ∈ Base K ∧ c ∈ Base K → G ∨ ˙ H ∨ ˙ c = G ∨ ˙ c ∨ ˙ H ∨ ˙ c
42 16 36 38 40 41 syl13anc ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∨ ˙ c = G ∨ ˙ c ∨ ˙ H ∨ ˙ c
43 34 42 breqtrrd ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ Q ≤ ˙ G ∨ ˙ H ∨ ˙ c
44 1 2 3 4 5 6 7 8 9 12 dalem37 ⊢ φ ∧ Y = Z ∧ ψ → R ≤ ˙ I ∨ ˙ c
45 1 3 4 dalempjqeb ⊢ φ → P ∨ ˙ Q ∈ Base K
46 45 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ Q ∈ Base K
47 24 3 4 hlatjcl ⊢ K ∈ HL ∧ G ∈ A ∧ H ∈ A → G ∨ ˙ H ∈ Base K
48 20 21 29 47 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∈ Base K
49 24 3 latjcl ⊢ K ∈ Lat ∧ G ∨ ˙ H ∈ Base K ∧ c ∈ Base K → G ∨ ˙ H ∨ ˙ c ∈ Base K
50 16 48 40 49 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∨ ˙ c ∈ Base K
51 1 4 dalemreb ⊢ φ → R ∈ Base K
52 51 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → R ∈ Base K
53 1 2 3 4 5 6 7 8 9 12 dalem34 ⊢ φ ∧ Y = Z ∧ ψ → I ∈ A
54 24 3 4 hlatjcl ⊢ K ∈ HL ∧ I ∈ A ∧ c ∈ A → I ∨ ˙ c ∈ Base K
55 20 53 23 54 syl3anc ⊢ φ ∧ Y = Z ∧ ψ → I ∨ ˙ c ∈ Base K
56 24 2 3 latjlej12 ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ G ∨ ˙ H ∨ ˙ c ∈ Base K ∧ R ∈ Base K ∧ I ∨ ˙ c ∈ Base K → P ∨ ˙ Q ≤ ˙ G ∨ ˙ H ∨ ˙ c ∧ R ≤ ˙ I ∨ ˙ c → P ∨ ˙ Q ∨ ˙ R ≤ ˙ G ∨ ˙ H ∨ ˙ c ∨ ˙ I ∨ ˙ c
57 16 46 50 52 55 56 syl122anc ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ Q ≤ ˙ G ∨ ˙ H ∨ ˙ c ∧ R ≤ ˙ I ∨ ˙ c → P ∨ ˙ Q ∨ ˙ R ≤ ˙ G ∨ ˙ H ∨ ˙ c ∨ ˙ I ∨ ˙ c
58 43 44 57 mp2and ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ Q ∨ ˙ R ≤ ˙ G ∨ ˙ H ∨ ˙ c ∨ ˙ I ∨ ˙ c
59 24 4 atbase ⊢ I ∈ A → I ∈ Base K
60 53 59 syl ⊢ φ ∧ Y = Z ∧ ψ → I ∈ Base K
61 24 3 latjjdir ⊢ K ∈ Lat ∧ G ∨ ˙ H ∈ Base K ∧ I ∈ Base K ∧ c ∈ Base K → G ∨ ˙ H ∨ ˙ I ∨ ˙ c = G ∨ ˙ H ∨ ˙ c ∨ ˙ I ∨ ˙ c
62 16 48 60 40 61 syl13anc ⊢ φ ∧ Y = Z ∧ ψ → G ∨ ˙ H ∨ ˙ I ∨ ˙ c = G ∨ ˙ H ∨ ˙ c ∨ ˙ I ∨ ˙ c
63 58 62 breqtrrd ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ Q ∨ ˙ R ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c
64 8 63 eqbrtrid ⊢ φ ∧ Y = Z ∧ ψ → Y ≤ ˙ G ∨ ˙ H ∨ ˙ I ∨ ˙ c