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

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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pexmidALT.p ⊢ + = ( +𝑃 ‘ 𝐾 )
pexmidALT.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion pexmidALTN ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) = 𝐴 )

Proof

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