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
|- .+ = ( +P ` K )
pexmidALT.o
|- ._|_ = ( _|_P ` K )
Assertion pexmidALTN
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( X .+ ( ._|_ ` X ) ) = A )

Proof

Step Hyp Ref Expression
1 pexmidALT.a
 |-  A = ( Atoms ` K )
2 pexmidALT.p
 |-  .+ = ( +P ` K )
3 pexmidALT.o
 |-  ._|_ = ( _|_P ` K )
4 id
 |-  ( X = (/) -> X = (/) )
5 fveq2
 |-  ( X = (/) -> ( ._|_ ` X ) = ( ._|_ ` (/) ) )
6 4 5 oveq12d
 |-  ( X = (/) -> ( X .+ ( ._|_ ` X ) ) = ( (/) .+ ( ._|_ ` (/) ) ) )
7 1 3 pol0N
 |-  ( K e. HL -> ( ._|_ ` (/) ) = A )
8 eqimss
 |-  ( ( ._|_ ` (/) ) = A -> ( ._|_ ` (/) ) C_ A )
9 7 8 syl
 |-  ( K e. HL -> ( ._|_ ` (/) ) C_ A )
10 1 2 padd02
 |-  ( ( K e. HL /\ ( ._|_ ` (/) ) C_ A ) -> ( (/) .+ ( ._|_ ` (/) ) ) = ( ._|_ ` (/) ) )
11 9 10 mpdan
 |-  ( K e. HL -> ( (/) .+ ( ._|_ ` (/) ) ) = ( ._|_ ` (/) ) )
12 11 7 eqtrd
 |-  ( K e. HL -> ( (/) .+ ( ._|_ ` (/) ) ) = A )
13 12 ad2antrr
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( (/) .+ ( ._|_ ` (/) ) ) = A )
14 6 13 sylan9eqr
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) /\ X = (/) ) -> ( X .+ ( ._|_ ` X ) ) = A )
15 1 2 3 pexmidlem8N
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( X .+ ( ._|_ ` X ) ) = A )
16 15 anassrs
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) /\ X =/= (/) ) -> ( X .+ ( ._|_ ` X ) ) = A )
17 14 16 pm2.61dane
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( X .+ ( ._|_ ` X ) ) = A )