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

Metamath Proof Explorer

Theorem lhpat4N

Description: Property of an atom under a co-atom. (Contributed by NM, 24-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lhpat.l ⊢ ≤ ˙ = ≤ K
lhpat.j ⊢ ∨ ˙ = join ⁡ K
lhpat.m ⊢ ∧ ˙ = meet ⁡ K
lhpat.a ⊢ A = Atoms ⁡ K
lhpat.h ⊢ H = LHyp ⁡ K
Assertion lhpat4N ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ U ∈ A ∧ U ≤ ˙ W → P ∨ ˙ U ∧ ˙ W = U

Proof

Step Hyp Ref Expression
1 lhpat.l ⊢ ≤ ˙ = ≤ K
2 lhpat.j ⊢ ∨ ˙ = join ⁡ K
3 lhpat.m ⊢ ∧ ˙ = meet ⁡ K
4 lhpat.a ⊢ A = Atoms ⁡ K
5 lhpat.h ⊢ H = LHyp ⁡ K
6 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ U ∈ A ∧ U ≤ ˙ W → K ∈ HL ∧ W ∈ H
7 simp2 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ U ∈ A ∧ U ≤ ˙ W → P ∈ A ∧ ¬ P ≤ ˙ W
8 simp3l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ U ∈ A ∧ U ≤ ˙ W → U ∈ A
9 eqid ⊢ Base K = Base K
10 9 4 atbase ⊢ U ∈ A → U ∈ Base K
11 8 10 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ U ∈ A ∧ U ≤ ˙ W → U ∈ Base K
12 simp3r ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ U ∈ A ∧ U ≤ ˙ W → U ≤ ˙ W
13 9 1 2 3 4 5 lhple ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ U ∈ Base K ∧ U ≤ ˙ W → P ∨ ˙ U ∧ ˙ W = U
14 6 7 11 12 13 syl112anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ U ∈ A ∧ U ≤ ˙ W → P ∨ ˙ U ∧ ˙ W = U