This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lhpjat2

Description: The join of a co-atom (hyperplane) and an atom not under it is the lattice unity. (Contributed by NM, 4-Jun-2012)

Ref Expression
Hypotheses lhpjat.l ⊢ ≤ ˙ = ≤ K
lhpjat.j ⊢ ∨ ˙ = join ⁡ K
lhpjat.u ⊢ 1 ˙ = 1. ⁡ K
lhpjat.a ⊢ A = Atoms ⁡ K
lhpjat.h ⊢ H = LHyp ⁡ K
Assertion lhpjat2 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ W = 1 ˙

Proof

Step Hyp Ref Expression
1 lhpjat.l ⊢ ≤ ˙ = ≤ K
2 lhpjat.j ⊢ ∨ ˙ = join ⁡ K
3 lhpjat.u ⊢ 1 ˙ = 1. ⁡ K
4 lhpjat.a ⊢ A = Atoms ⁡ K
5 lhpjat.h ⊢ H = LHyp ⁡ K
6 hllat ⊢ K ∈ HL → K ∈ Lat
7 6 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ Lat
8 eqid ⊢ Base K = Base K
9 8 4 atbase ⊢ P ∈ A → P ∈ Base K
10 9 ad2antrl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∈ Base K
11 8 5 lhpbase ⊢ W ∈ H → W ∈ Base K
12 11 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∈ Base K
13 8 2 latjcom ⊢ K ∈ Lat ∧ P ∈ Base K ∧ W ∈ Base K → P ∨ ˙ W = W ∨ ˙ P
14 7 10 12 13 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ W = W ∨ ˙ P
15 1 2 3 4 5 lhpjat1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∨ ˙ P = 1 ˙
16 14 15 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ W = 1 ˙