Metamath Proof Explorer

Theorem dalemcea

Description: Lemma for dath . Frequently-used utility lemma. Here we show that C must be an atom. This is an assumption in most presentations of Desargues's theorem; instead, we assume only the C is a lattice element, in order to make later substitutions for C easier. (Contributed by NM, 23-Sep-2012)

Ref Expression
Hypotheses dalema.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
dalemc.l ⊢ ≤ ˙ = ≤ K
dalemc.j ⊢ ∨ ˙ = join ⁡ K
dalemc.a ⊢ A = Atoms ⁡ K
dalem1.o ⊢ O = LPlanes ⁡ K
dalem1.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
Assertion dalemcea ⊢ φ → C ∈ A

Proof

Step Hyp Ref Expression
1 dalema.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 dalemc.l ⊢ ≤ ˙ = ≤ K
3 dalemc.j ⊢ ∨ ˙ = join ⁡ K
4 dalemc.a ⊢ A = Atoms ⁡ K
5 dalem1.o ⊢ O = LPlanes ⁡ K
6 dalem1.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
7 1 dalemkeop ⊢ φ → K ∈ OP
8 1 4 dalemceb ⊢ φ → C ∈ Base K
9 1 dalemkehl ⊢ φ → K ∈ HL
10 1 2 3 4 5 6 dalempjsen ⊢ φ → P ∨ ˙ S ∈ LLines ⁡ K
11 1 dalemqea ⊢ φ → Q ∈ A
12 1 dalemtea ⊢ φ → T ∈ A
13 1 2 3 4 5 6 dalemqnet ⊢ φ → Q ≠ T
14 eqid ⊢ LLines ⁡ K = LLines ⁡ K
15 3 4 14 llni2 ⊢ K ∈ HL ∧ Q ∈ A ∧ T ∈ A ∧ Q ≠ T → Q ∨ ˙ T ∈ LLines ⁡ K
16 9 11 12 13 15 syl31anc ⊢ φ → Q ∨ ˙ T ∈ LLines ⁡ K
17 1 2 3 4 5 6 dalem1 ⊢ φ → P ∨ ˙ S ≠ Q ∨ ˙ T
18 1 dalem-clpjq ⊢ φ → ¬ C ≤ ˙ P ∨ ˙ Q
19 1 3 4 dalempjqeb ⊢ φ → P ∨ ˙ Q ∈ Base K
20 eqid ⊢ Base K = Base K
21 eqid ⊢ 0. ⁡ K = 0. ⁡ K
22 20 2 21 op0le ⊢ K ∈ OP ∧ P ∨ ˙ Q ∈ Base K → 0. ⁡ K ≤ ˙ P ∨ ˙ Q
23 7 19 22 syl2anc ⊢ φ → 0. ⁡ K ≤ ˙ P ∨ ˙ Q
24 breq1 ⊢ C = 0. ⁡ K → C ≤ ˙ P ∨ ˙ Q ↔ 0. ⁡ K ≤ ˙ P ∨ ˙ Q
25 23 24 syl5ibrcom ⊢ φ → C = 0. ⁡ K → C ≤ ˙ P ∨ ˙ Q
26 25 necon3bd ⊢ φ → ¬ C ≤ ˙ P ∨ ˙ Q → C ≠ 0. ⁡ K
27 18 26 mpd ⊢ φ → C ≠ 0. ⁡ K
28 eqid ⊢ < K = < K
29 20 28 21 opltn0 ⊢ K ∈ OP ∧ C ∈ Base K → 0. ⁡ K < K C ↔ C ≠ 0. ⁡ K
30 7 8 29 syl2anc ⊢ φ → 0. ⁡ K < K C ↔ C ≠ 0. ⁡ K
31 27 30 mpbird ⊢ φ → 0. ⁡ K < K C
32 1 dalemclpjs ⊢ φ → C ≤ ˙ P ∨ ˙ S
33 1 dalemclqjt ⊢ φ → C ≤ ˙ Q ∨ ˙ T
34 1 dalemkelat ⊢ φ → K ∈ Lat
35 1 dalempea ⊢ φ → P ∈ A
36 1 dalemsea ⊢ φ → S ∈ A
37 20 3 4 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ S ∈ A → P ∨ ˙ S ∈ Base K
38 9 35 36 37 syl3anc ⊢ φ → P ∨ ˙ S ∈ Base K
39 20 3 4 hlatjcl ⊢ K ∈ HL ∧ Q ∈ A ∧ T ∈ A → Q ∨ ˙ T ∈ Base K
40 9 11 12 39 syl3anc ⊢ φ → Q ∨ ˙ T ∈ Base K
41 eqid ⊢ meet ⁡ K = meet ⁡ K
42 20 2 41 latlem12 ⊢ K ∈ Lat ∧ C ∈ Base K ∧ P ∨ ˙ S ∈ Base K ∧ Q ∨ ˙ T ∈ Base K → C ≤ ˙ P ∨ ˙ S ∧ C ≤ ˙ Q ∨ ˙ T ↔ C ≤ ˙ P ∨ ˙ S meet ⁡ K Q ∨ ˙ T
43 34 8 38 40 42 syl13anc ⊢ φ → C ≤ ˙ P ∨ ˙ S ∧ C ≤ ˙ Q ∨ ˙ T ↔ C ≤ ˙ P ∨ ˙ S meet ⁡ K Q ∨ ˙ T
44 32 33 43 mpbi2and ⊢ φ → C ≤ ˙ P ∨ ˙ S meet ⁡ K Q ∨ ˙ T
45 opposet ⊢ K ∈ OP → K ∈ Poset
46 7 45 syl ⊢ φ → K ∈ Poset
47 20 21 op0cl ⊢ K ∈ OP → 0. ⁡ K ∈ Base K
48 7 47 syl ⊢ φ → 0. ⁡ K ∈ Base K
49 20 41 latmcl ⊢ K ∈ Lat ∧ P ∨ ˙ S ∈ Base K ∧ Q ∨ ˙ T ∈ Base K → P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ∈ Base K
50 34 38 40 49 syl3anc ⊢ φ → P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ∈ Base K
51 20 2 28 pltletr ⊢ K ∈ Poset ∧ 0. ⁡ K ∈ Base K ∧ C ∈ Base K ∧ P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ∈ Base K → 0. ⁡ K < K C ∧ C ≤ ˙ P ∨ ˙ S meet ⁡ K Q ∨ ˙ T → 0. ⁡ K < K P ∨ ˙ S meet ⁡ K Q ∨ ˙ T
52 46 48 8 50 51 syl13anc ⊢ φ → 0. ⁡ K < K C ∧ C ≤ ˙ P ∨ ˙ S meet ⁡ K Q ∨ ˙ T → 0. ⁡ K < K P ∨ ˙ S meet ⁡ K Q ∨ ˙ T
53 31 44 52 mp2and ⊢ φ → 0. ⁡ K < K P ∨ ˙ S meet ⁡ K Q ∨ ˙ T
54 20 28 21 opltn0 ⊢ K ∈ OP ∧ P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ∈ Base K → 0. ⁡ K < K P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ↔ P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ≠ 0. ⁡ K
55 7 50 54 syl2anc ⊢ φ → 0. ⁡ K < K P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ↔ P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ≠ 0. ⁡ K
56 53 55 mpbid ⊢ φ → P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ≠ 0. ⁡ K
57 41 21 4 14 2llnmat ⊢ K ∈ HL ∧ P ∨ ˙ S ∈ LLines ⁡ K ∧ Q ∨ ˙ T ∈ LLines ⁡ K ∧ P ∨ ˙ S ≠ Q ∨ ˙ T ∧ P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ≠ 0. ⁡ K → P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ∈ A
58 9 10 16 17 56 57 syl32anc ⊢ φ → P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ∈ A
59 20 2 21 4 leat2 ⊢ K ∈ OP ∧ C ∈ Base K ∧ P ∨ ˙ S meet ⁡ K Q ∨ ˙ T ∈ A ∧ C ≠ 0. ⁡ K ∧ C ≤ ˙ P ∨ ˙ S meet ⁡ K Q ∨ ˙ T → C = P ∨ ˙ S meet ⁡ K Q ∨ ˙ T
60 7 8 58 27 44 59 syl32anc ⊢ φ → C = P ∨ ˙ S meet ⁡ K Q ∨ ˙ T
61 60 58 eqeltrd ⊢ φ → C ∈ A