Metamath Proof Explorer

Theorem dalem21

Description: Lemma for dath . Show that lines c d and P S intersect at an atom. (Contributed by NM, 2-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
dalem21.m ⊢ ∧ ˙ = meet ⁡ K
dalem21.o ⊢ O = LPlanes ⁡ K
dalem21.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
dalem21.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
Assertion dalem21 ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ d ∧ ˙ P ∨ ˙ S ∈ A

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 dalem21.m ⊢ ∧ ˙ = meet ⁡ K
7 dalem21.o ⊢ O = LPlanes ⁡ K
8 dalem21.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
9 dalem21.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
10 1 dalemkehl ⊢ φ → K ∈ HL
11 10 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → K ∈ HL
12 1 2 3 4 5 dalemcjden ⊢ φ ∧ ψ → c ∨ ˙ d ∈ LLines ⁡ K
13 12 3adant2 ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ d ∈ LLines ⁡ K
14 1 2 3 4 7 8 dalempjsen ⊢ φ → P ∨ ˙ S ∈ LLines ⁡ K
15 14 3ad2ant1 ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ S ∈ LLines ⁡ K
16 1 2 3 4 7 8 dalemply ⊢ φ → P ≤ ˙ Y
17 16 adantr ⊢ φ ∧ Y = Z → P ≤ ˙ Y
18 1 2 3 4 9 dalemsly ⊢ φ ∧ Y = Z → S ≤ ˙ Y
19 1 dalemkelat ⊢ φ → K ∈ Lat
20 1 4 dalempeb ⊢ φ → P ∈ Base K
21 1 4 dalemseb ⊢ φ → S ∈ Base K
22 1 7 dalemyeb ⊢ φ → Y ∈ Base K
23 eqid ⊢ Base K = Base K
24 23 2 3 latjle12 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ S ∈ Base K ∧ Y ∈ Base K → P ≤ ˙ Y ∧ S ≤ ˙ Y ↔ P ∨ ˙ S ≤ ˙ Y
25 19 20 21 22 24 syl13anc ⊢ φ → P ≤ ˙ Y ∧ S ≤ ˙ Y ↔ P ∨ ˙ S ≤ ˙ Y
26 25 adantr ⊢ φ ∧ Y = Z → P ≤ ˙ Y ∧ S ≤ ˙ Y ↔ P ∨ ˙ S ≤ ˙ Y
27 17 18 26 mpbi2and ⊢ φ ∧ Y = Z → P ∨ ˙ S ≤ ˙ Y
28 27 3adant3 ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ S ≤ ˙ Y
29 5 dalem-ccly ⊢ ψ → ¬ c ≤ ˙ Y
30 29 adantl ⊢ φ ∧ ψ → ¬ c ≤ ˙ Y
31 19 adantr ⊢ φ ∧ ψ → K ∈ Lat
32 5 4 dalemcceb ⊢ ψ → c ∈ Base K
33 32 adantl ⊢ φ ∧ ψ → c ∈ Base K
34 5 dalemddea ⊢ ψ → d ∈ A
35 23 4 atbase ⊢ d ∈ A → d ∈ Base K
36 34 35 syl ⊢ ψ → d ∈ Base K
37 36 adantl ⊢ φ ∧ ψ → d ∈ Base K
38 23 2 3 latlej1 ⊢ K ∈ Lat ∧ c ∈ Base K ∧ d ∈ Base K → c ≤ ˙ c ∨ ˙ d
39 31 33 37 38 syl3anc ⊢ φ ∧ ψ → c ≤ ˙ c ∨ ˙ d
40 eqid ⊢ LLines ⁡ K = LLines ⁡ K
41 23 40 llnbase ⊢ c ∨ ˙ d ∈ LLines ⁡ K → c ∨ ˙ d ∈ Base K
42 12 41 syl ⊢ φ ∧ ψ → c ∨ ˙ d ∈ Base K
43 22 adantr ⊢ φ ∧ ψ → Y ∈ Base K
44 23 2 lattr ⊢ K ∈ Lat ∧ c ∈ Base K ∧ c ∨ ˙ d ∈ Base K ∧ Y ∈ Base K → c ≤ ˙ c ∨ ˙ d ∧ c ∨ ˙ d ≤ ˙ Y → c ≤ ˙ Y
45 31 33 42 43 44 syl13anc ⊢ φ ∧ ψ → c ≤ ˙ c ∨ ˙ d ∧ c ∨ ˙ d ≤ ˙ Y → c ≤ ˙ Y
46 39 45 mpand ⊢ φ ∧ ψ → c ∨ ˙ d ≤ ˙ Y → c ≤ ˙ Y
47 30 46 mtod ⊢ φ ∧ ψ → ¬ c ∨ ˙ d ≤ ˙ Y
48 47 3adant2 ⊢ φ ∧ Y = Z ∧ ψ → ¬ c ∨ ˙ d ≤ ˙ Y
49 nbrne2 ⊢ P ∨ ˙ S ≤ ˙ Y ∧ ¬ c ∨ ˙ d ≤ ˙ Y → P ∨ ˙ S ≠ c ∨ ˙ d
50 28 48 49 syl2anc ⊢ φ ∧ Y = Z ∧ ψ → P ∨ ˙ S ≠ c ∨ ˙ d
51 50 necomd ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ d ≠ P ∨ ˙ S
52 hlatl ⊢ K ∈ HL → K ∈ AtLat
53 10 52 syl ⊢ φ → K ∈ AtLat
54 53 adantr ⊢ φ ∧ ψ → K ∈ AtLat
55 1 dalempea ⊢ φ → P ∈ A
56 1 dalemsea ⊢ φ → S ∈ A
57 23 3 4 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ S ∈ A → P ∨ ˙ S ∈ Base K
58 10 55 56 57 syl3anc ⊢ φ → P ∨ ˙ S ∈ Base K
59 58 adantr ⊢ φ ∧ ψ → P ∨ ˙ S ∈ Base K
60 23 6 latmcl ⊢ K ∈ Lat ∧ c ∨ ˙ d ∈ Base K ∧ P ∨ ˙ S ∈ Base K → c ∨ ˙ d ∧ ˙ P ∨ ˙ S ∈ Base K
61 31 42 59 60 syl3anc ⊢ φ ∧ ψ → c ∨ ˙ d ∧ ˙ P ∨ ˙ S ∈ Base K
62 1 2 3 4 7 8 dalemcea ⊢ φ → C ∈ A
63 62 adantr ⊢ φ ∧ ψ → C ∈ A
64 5 dalemclccjdd ⊢ ψ → C ≤ ˙ c ∨ ˙ d
65 64 adantl ⊢ φ ∧ ψ → C ≤ ˙ c ∨ ˙ d
66 1 dalemclpjs ⊢ φ → C ≤ ˙ P ∨ ˙ S
67 66 adantr ⊢ φ ∧ ψ → C ≤ ˙ P ∨ ˙ S
68 1 4 dalemceb ⊢ φ → C ∈ Base K
69 68 adantr ⊢ φ ∧ ψ → C ∈ Base K
70 23 2 6 latlem12 ⊢ K ∈ Lat ∧ C ∈ Base K ∧ c ∨ ˙ d ∈ Base K ∧ P ∨ ˙ S ∈ Base K → C ≤ ˙ c ∨ ˙ d ∧ C ≤ ˙ P ∨ ˙ S ↔ C ≤ ˙ c ∨ ˙ d ∧ ˙ P ∨ ˙ S
71 31 69 42 59 70 syl13anc ⊢ φ ∧ ψ → C ≤ ˙ c ∨ ˙ d ∧ C ≤ ˙ P ∨ ˙ S ↔ C ≤ ˙ c ∨ ˙ d ∧ ˙ P ∨ ˙ S
72 65 67 71 mpbi2and ⊢ φ ∧ ψ → C ≤ ˙ c ∨ ˙ d ∧ ˙ P ∨ ˙ S
73 eqid ⊢ 0. ⁡ K = 0. ⁡ K
74 23 2 73 4 atlen0 ⊢ K ∈ AtLat ∧ c ∨ ˙ d ∧ ˙ P ∨ ˙ S ∈ Base K ∧ C ∈ A ∧ C ≤ ˙ c ∨ ˙ d ∧ ˙ P ∨ ˙ S → c ∨ ˙ d ∧ ˙ P ∨ ˙ S ≠ 0. ⁡ K
75 54 61 63 72 74 syl31anc ⊢ φ ∧ ψ → c ∨ ˙ d ∧ ˙ P ∨ ˙ S ≠ 0. ⁡ K
76 75 3adant2 ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ d ∧ ˙ P ∨ ˙ S ≠ 0. ⁡ K
77 6 73 4 40 2llnmat ⊢ K ∈ HL ∧ c ∨ ˙ d ∈ LLines ⁡ K ∧ P ∨ ˙ S ∈ LLines ⁡ K ∧ c ∨ ˙ d ≠ P ∨ ˙ S ∧ c ∨ ˙ d ∧ ˙ P ∨ ˙ S ≠ 0. ⁡ K → c ∨ ˙ d ∧ ˙ P ∨ ˙ S ∈ A
78 11 13 15 51 76 77 syl32anc ⊢ φ ∧ Y = Z ∧ ψ → c ∨ ˙ d ∧ ˙ P ∨ ˙ S ∈ A