Metamath Proof Explorer

Theorem lhpjat1

Description: The join of a co-atom (hyperplane) and an atom not under it is the lattice unity. (Contributed by NM, 18-May-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 lhpjat1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∨ ˙ P = 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 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ HL
7 eqid ⊢ Base K = Base K
8 7 5 lhpbase ⊢ W ∈ H → W ∈ Base K
9 8 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∈ Base K
10 simprl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∈ A
11 eqid ⊢ ⋖ K = ⋖ K
12 3 11 5 lhp1cvr ⊢ K ∈ HL ∧ W ∈ H → W ⋖ K 1 ˙
13 12 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ⋖ K 1 ˙
14 simprr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → ¬ P ≤ ˙ W
15 7 1 2 3 11 4 1cvrjat ⊢ K ∈ HL ∧ W ∈ Base K ∧ P ∈ A ∧ W ⋖ K 1 ˙ ∧ ¬ P ≤ ˙ W → W ∨ ˙ P = 1 ˙
16 6 9 10 13 14 15 syl32anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∨ ˙ P = 1 ˙