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 
|- 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 )