Metamath Proof Explorer

Theorem lhpj1

Description: The join of a co-atom (hyperplane) and an element not under it is the lattice unit. (Contributed by NM, 7-Dec-2012)

Ref Expression
Hypotheses lhpj1.b ⊢ B = Base K
lhpj1.l ⊢ ≤ ˙ = ≤ K
lhpj1.j ⊢ ∨ ˙ = join ⁡ K
lhpj1.u ⊢ 1 ˙ = 1. ⁡ K
lhpj1.h ⊢ H = LHyp ⁡ K
Assertion lhpj1 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → W ∨ ˙ X = 1 ˙

Proof

Step Hyp Ref Expression
1 lhpj1.b ⊢ B = Base K
2 lhpj1.l ⊢ ≤ ˙ = ≤ K
3 lhpj1.j ⊢ ∨ ˙ = join ⁡ K
4 lhpj1.u ⊢ 1 ˙ = 1. ⁡ K
5 lhpj1.h ⊢ H = LHyp ⁡ K
6 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → K ∈ HL
7 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → X ∈ B
8 1 5 lhpbase ⊢ W ∈ H → W ∈ B
9 8 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → W ∈ B
10 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
11 1 2 10 hlrelat2 ⊢ K ∈ HL ∧ X ∈ B ∧ W ∈ B → ¬ X ≤ ˙ W ↔ ∃ p ∈ Atoms ⁡ K p ≤ ˙ X ∧ ¬ p ≤ ˙ W
12 6 7 9 11 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → ¬ X ≤ ˙ W ↔ ∃ p ∈ Atoms ⁡ K p ≤ ˙ X ∧ ¬ p ≤ ˙ W
13 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → K ∈ HL ∧ W ∈ H
14 simp2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → p ∈ Atoms ⁡ K
15 simp3r ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → ¬ p ≤ ˙ W
16 2 3 4 10 5 lhpjat1 ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ ˙ W → W ∨ ˙ p = 1 ˙
17 13 14 15 16 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → W ∨ ˙ p = 1 ˙
18 simp3l ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → p ≤ ˙ X
19 simp1ll ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → K ∈ HL
20 19 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → K ∈ Lat
21 1 10 atbase ⊢ p ∈ Atoms ⁡ K → p ∈ B
22 21 3ad2ant2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → p ∈ B
23 simp1r ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → X ∈ B
24 9 3ad2ant1 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → W ∈ B
25 1 2 3 latjlej2 ⊢ K ∈ Lat ∧ p ∈ B ∧ X ∈ B ∧ W ∈ B → p ≤ ˙ X → W ∨ ˙ p ≤ ˙ W ∨ ˙ X
26 20 22 23 24 25 syl13anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → p ≤ ˙ X → W ∨ ˙ p ≤ ˙ W ∨ ˙ X
27 18 26 mpd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → W ∨ ˙ p ≤ ˙ W ∨ ˙ X
28 17 27 eqbrtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → 1 ˙ ≤ ˙ W ∨ ˙ X
29 hlop ⊢ K ∈ HL → K ∈ OP
30 19 29 syl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → K ∈ OP
31 1 3 latjcl ⊢ K ∈ Lat ∧ W ∈ B ∧ X ∈ B → W ∨ ˙ X ∈ B
32 20 24 23 31 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → W ∨ ˙ X ∈ B
33 1 2 4 op1le ⊢ K ∈ OP ∧ W ∨ ˙ X ∈ B → 1 ˙ ≤ ˙ W ∨ ˙ X ↔ W ∨ ˙ X = 1 ˙
34 30 32 33 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → 1 ˙ ≤ ˙ W ∨ ˙ X ↔ W ∨ ˙ X = 1 ˙
35 28 34 mpbid ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ p ∈ Atoms ⁡ K ∧ p ≤ ˙ X ∧ ¬ p ≤ ˙ W → W ∨ ˙ X = 1 ˙
36 35 rexlimdv3a ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → ∃ p ∈ Atoms ⁡ K p ≤ ˙ X ∧ ¬ p ≤ ˙ W → W ∨ ˙ X = 1 ˙
37 12 36 sylbid ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → ¬ X ≤ ˙ W → W ∨ ˙ X = 1 ˙
38 37 impr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W → W ∨ ˙ X = 1 ˙