Metamath Proof Explorer

Theorem pexmidALTN

Description: Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N . Lemma 3.3(2) in Holland95 p. 215. In our proof, we use the variables X , M , p , q , r in place of Hollands' l, m, P, Q, L respectively. TODO: should we make this obsolete? (Contributed by NM, 3-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pexmidALT.a ⊢ A = Atoms ⁡ K
pexmidALT.p ⊢ + ˙ = + 𝑃 ⁡ K
pexmidALT.o ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
Assertion pexmidALTN ⊢ K ∈ HL ∧ X ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X → X + ˙ ⊥ ˙ ⁡ X = A

Proof

Step Hyp Ref Expression
1 pexmidALT.a ⊢ A = Atoms ⁡ K
2 pexmidALT.p ⊢ + ˙ = + 𝑃 ⁡ K
3 pexmidALT.o ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
4 id ⊢ X = ∅ → X = ∅
5 fveq2 ⊢ X = ∅ → ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ ∅
6 4 5 oveq12d ⊢ X = ∅ → X + ˙ ⊥ ˙ ⁡ X = ∅ + ˙ ⊥ ˙ ⁡ ∅
7 1 3 pol0N ⊢ K ∈ HL → ⊥ ˙ ⁡ ∅ = A
8 eqimss ⊢ ⊥ ˙ ⁡ ∅ = A → ⊥ ˙ ⁡ ∅ ⊆ A
9 7 8 syl ⊢ K ∈ HL → ⊥ ˙ ⁡ ∅ ⊆ A
10 1 2 padd02 ⊢ K ∈ HL ∧ ⊥ ˙ ⁡ ∅ ⊆ A → ∅ + ˙ ⊥ ˙ ⁡ ∅ = ⊥ ˙ ⁡ ∅
11 9 10 mpdan ⊢ K ∈ HL → ∅ + ˙ ⊥ ˙ ⁡ ∅ = ⊥ ˙ ⁡ ∅
12 11 7 eqtrd ⊢ K ∈ HL → ∅ + ˙ ⊥ ˙ ⁡ ∅ = A
13 12 ad2antrr ⊢ K ∈ HL ∧ X ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X → ∅ + ˙ ⊥ ˙ ⁡ ∅ = A
14 6 13 sylan9eqr ⊢ K ∈ HL ∧ X ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X ∧ X = ∅ → X + ˙ ⊥ ˙ ⁡ X = A
15 1 2 3 pexmidlem8N ⊢ K ∈ HL ∧ X ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X ∧ X ≠ ∅ → X + ˙ ⊥ ˙ ⁡ X = A
16 15 anassrs ⊢ K ∈ HL ∧ X ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X ∧ X ≠ ∅ → X + ˙ ⊥ ˙ ⁡ X = A
17 14 16 pm2.61dane ⊢ K ∈ HL ∧ X ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X → X + ˙ ⊥ ˙ ⁡ X = A