Metamath Proof Explorer

Theorem dochexmid

Description: Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 . 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. ( pexmidALTN analog.) (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dochexmid.h 
|- H = ( LHyp ` K )
dochexmid.o 
|- ._|_ = ( ( ocH ` K ) ` W )
dochexmid.u 
|- U = ( ( DVecH ` K ) ` W )
dochexmid.v 
|- V = ( Base ` U )
dochexmid.s 
|- S = ( LSubSp ` U )
dochexmid.p 
|- .(+) = ( LSSum ` U )
dochexmid.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochexmid.x 
|- ( ph -> X e. S )
dochexmid.c 
|- ( ph -> ( ._|_ ` ( ._|_ ` X ) ) = X )
Assertion dochexmid 
|- ( ph -> ( X .(+) ( ._|_ ` X ) ) = V )

Proof

Step Hyp Ref Expression
1 dochexmid.h 
 |-  H = ( LHyp ` K )
2 dochexmid.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochexmid.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochexmid.v 
 |-  V = ( Base ` U )
5 dochexmid.s 
 |-  S = ( LSubSp ` U )
6 dochexmid.p 
 |-  .(+) = ( LSSum ` U )
7 dochexmid.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 dochexmid.x 
 |-  ( ph -> X e. S )
9 dochexmid.c 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` X ) ) = X )
10 id 
 |-  ( X = { ( 0g ` U ) } -> X = { ( 0g ` U ) } )
11 fveq2 
 |-  ( X = { ( 0g ` U ) } -> ( ._|_ ` X ) = ( ._|_ ` { ( 0g ` U ) } ) )
12 10 11 oveq12d 
 |-  ( X = { ( 0g ` U ) } -> ( X .(+) ( ._|_ ` X ) ) = ( { ( 0g ` U ) } .(+) ( ._|_ ` { ( 0g ` U ) } ) ) )
13 1 3 7 dvhlmod 
 |-  ( ph -> U e. LMod )
14 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
15 4 14 lmod0vcl 
 |-  ( U e. LMod -> ( 0g ` U ) e. V )
16 13 15 syl 
 |-  ( ph -> ( 0g ` U ) e. V )
17 16 snssd 
 |-  ( ph -> { ( 0g ` U ) } C_ V )
18 1 3 4 5 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { ( 0g ` U ) } C_ V ) -> ( ._|_ ` { ( 0g ` U ) } ) e. S )
19 7 17 18 syl2anc 
 |-  ( ph -> ( ._|_ ` { ( 0g ` U ) } ) e. S )
20 5 lsssubg 
 |-  ( ( U e. LMod /\ ( ._|_ ` { ( 0g ` U ) } ) e. S ) -> ( ._|_ ` { ( 0g ` U ) } ) e. ( SubGrp ` U ) )
21 13 19 20 syl2anc 
 |-  ( ph -> ( ._|_ ` { ( 0g ` U ) } ) e. ( SubGrp ` U ) )
22 14 6 lsm02 
 |-  ( ( ._|_ ` { ( 0g ` U ) } ) e. ( SubGrp ` U ) -> ( { ( 0g ` U ) } .(+) ( ._|_ ` { ( 0g ` U ) } ) ) = ( ._|_ ` { ( 0g ` U ) } ) )
23 21 22 syl 
 |-  ( ph -> ( { ( 0g ` U ) } .(+) ( ._|_ ` { ( 0g ` U ) } ) ) = ( ._|_ ` { ( 0g ` U ) } ) )
24 1 3 2 4 14 doch0 
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` { ( 0g ` U ) } ) = V )
25 7 24 syl 
 |-  ( ph -> ( ._|_ ` { ( 0g ` U ) } ) = V )
26 23 25 eqtrd 
 |-  ( ph -> ( { ( 0g ` U ) } .(+) ( ._|_ ` { ( 0g ` U ) } ) ) = V )
27 12 26 sylan9eqr 
 |-  ( ( ph /\ X = { ( 0g ` U ) } ) -> ( X .(+) ( ._|_ ` X ) ) = V )
28 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
29 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
30 7 adantr 
 |-  ( ( ph /\ X =/= { ( 0g ` U ) } ) -> ( K e. HL /\ W e. H ) )
31 8 adantr 
 |-  ( ( ph /\ X =/= { ( 0g ` U ) } ) -> X e. S )
32 simpr 
 |-  ( ( ph /\ X =/= { ( 0g ` U ) } ) -> X =/= { ( 0g ` U ) } )
33 9 adantr 
 |-  ( ( ph /\ X =/= { ( 0g ` U ) } ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
34 1 2 3 4 5 28 6 29 30 31 14 32 33 dochexmidlem8 
 |-  ( ( ph /\ X =/= { ( 0g ` U ) } ) -> ( X .(+) ( ._|_ ` X ) ) = V )
35 27 34 pm2.61dane 
 |-  ( ph -> ( X .(+) ( ._|_ ` X ) ) = V )