Metamath Proof Explorer

Theorem pjdm2

Description: A subspace is in the domain of the projection function iff the subspace admits a projection decomposition of the whole space. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses pjdm2.v 
|- V = ( Base ` W )
pjdm2.l 
|- L = ( LSubSp ` W )
pjdm2.o 
|- ._|_ = ( ocv ` W )
pjdm2.s 
|- .(+) = ( LSSum ` W )
pjdm2.k 
|- K = ( proj ` W )
Assertion pjdm2 
|- ( W e. PreHil -> ( T e. dom K <-> ( T e. L /\ ( T .(+) ( ._|_ ` T ) ) = V ) ) )

Proof

Step Hyp Ref Expression
1 pjdm2.v 
 |-  V = ( Base ` W )
2 pjdm2.l 
 |-  L = ( LSubSp ` W )
3 pjdm2.o 
 |-  ._|_ = ( ocv ` W )
4 pjdm2.s 
 |-  .(+) = ( LSSum ` W )
5 pjdm2.k 
 |-  K = ( proj ` W )
6 eqid 
 |-  ( proj1 ` W ) = ( proj1 ` W )
7 1 2 3 6 5 pjdm 
 |-  ( T e. dom K <-> ( T e. L /\ ( T ( proj1 ` W ) ( ._|_ ` T ) ) : V --> V ) )
8 eqid 
 |-  ( +g ` W ) = ( +g ` W )
9 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
10 eqid 
 |-  ( Cntz ` W ) = ( Cntz ` W )
11 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
12 11 adantr 
 |-  ( ( W e. PreHil /\ T e. L ) -> W e. LMod )
13 2 lsssssubg 
 |-  ( W e. LMod -> L C_ ( SubGrp ` W ) )
14 12 13 syl 
 |-  ( ( W e. PreHil /\ T e. L ) -> L C_ ( SubGrp ` W ) )
15 simpr 
 |-  ( ( W e. PreHil /\ T e. L ) -> T e. L )
16 14 15 sseldd 
 |-  ( ( W e. PreHil /\ T e. L ) -> T e. ( SubGrp ` W ) )
17 1 2 lssss 
 |-  ( T e. L -> T C_ V )
18 1 3 2 ocvlss 
 |-  ( ( W e. PreHil /\ T C_ V ) -> ( ._|_ ` T ) e. L )
19 17 18 sylan2 
 |-  ( ( W e. PreHil /\ T e. L ) -> ( ._|_ ` T ) e. L )
20 14 19 sseldd 
 |-  ( ( W e. PreHil /\ T e. L ) -> ( ._|_ ` T ) e. ( SubGrp ` W ) )
21 3 2 9 ocvin 
 |-  ( ( W e. PreHil /\ T e. L ) -> ( T i^i ( ._|_ ` T ) ) = { ( 0g ` W ) } )
22 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
23 12 22 syl 
 |-  ( ( W e. PreHil /\ T e. L ) -> W e. Abel )
24 10 23 16 20 ablcntzd 
 |-  ( ( W e. PreHil /\ T e. L ) -> T C_ ( ( Cntz ` W ) ` ( ._|_ ` T ) ) )
25 8 4 9 10 16 20 21 24 6 pj1f 
 |-  ( ( W e. PreHil /\ T e. L ) -> ( T ( proj1 ` W ) ( ._|_ ` T ) ) : ( T .(+) ( ._|_ ` T ) ) --> T )
26 17 adantl 
 |-  ( ( W e. PreHil /\ T e. L ) -> T C_ V )
27 25 26 fssd 
 |-  ( ( W e. PreHil /\ T e. L ) -> ( T ( proj1 ` W ) ( ._|_ ` T ) ) : ( T .(+) ( ._|_ ` T ) ) --> V )
28 fdm 
 |-  ( ( T ( proj1 ` W ) ( ._|_ ` T ) ) : ( T .(+) ( ._|_ ` T ) ) --> V -> dom ( T ( proj1 ` W ) ( ._|_ ` T ) ) = ( T .(+) ( ._|_ ` T ) ) )
29 28 eqcomd 
 |-  ( ( T ( proj1 ` W ) ( ._|_ ` T ) ) : ( T .(+) ( ._|_ ` T ) ) --> V -> ( T .(+) ( ._|_ ` T ) ) = dom ( T ( proj1 ` W ) ( ._|_ ` T ) ) )
30 fdm 
 |-  ( ( T ( proj1 ` W ) ( ._|_ ` T ) ) : V --> V -> dom ( T ( proj1 ` W ) ( ._|_ ` T ) ) = V )
31 30 eqeq2d 
 |-  ( ( T ( proj1 ` W ) ( ._|_ ` T ) ) : V --> V -> ( ( T .(+) ( ._|_ ` T ) ) = dom ( T ( proj1 ` W ) ( ._|_ ` T ) ) <-> ( T .(+) ( ._|_ ` T ) ) = V ) )
32 29 31 syl5ibcom 
 |-  ( ( T ( proj1 ` W ) ( ._|_ ` T ) ) : ( T .(+) ( ._|_ ` T ) ) --> V -> ( ( T ( proj1 ` W ) ( ._|_ ` T ) ) : V --> V -> ( T .(+) ( ._|_ ` T ) ) = V ) )
33 feq2 
 |-  ( ( T .(+) ( ._|_ ` T ) ) = V -> ( ( T ( proj1 ` W ) ( ._|_ ` T ) ) : ( T .(+) ( ._|_ ` T ) ) --> V <-> ( T ( proj1 ` W ) ( ._|_ ` T ) ) : V --> V ) )
34 33 biimpcd 
 |-  ( ( T ( proj1 ` W ) ( ._|_ ` T ) ) : ( T .(+) ( ._|_ ` T ) ) --> V -> ( ( T .(+) ( ._|_ ` T ) ) = V -> ( T ( proj1 ` W ) ( ._|_ ` T ) ) : V --> V ) )
35 32 34 impbid 
 |-  ( ( T ( proj1 ` W ) ( ._|_ ` T ) ) : ( T .(+) ( ._|_ ` T ) ) --> V -> ( ( T ( proj1 ` W ) ( ._|_ ` T ) ) : V --> V <-> ( T .(+) ( ._|_ ` T ) ) = V ) )
36 27 35 syl 
 |-  ( ( W e. PreHil /\ T e. L ) -> ( ( T ( proj1 ` W ) ( ._|_ ` T ) ) : V --> V <-> ( T .(+) ( ._|_ ` T ) ) = V ) )
37 36 pm5.32da 
 |-  ( W e. PreHil -> ( ( T e. L /\ ( T ( proj1 ` W ) ( ._|_ ` T ) ) : V --> V ) <-> ( T e. L /\ ( T .(+) ( ._|_ ` T ) ) = V ) ) )
38 7 37 bitrid 
 |-  ( W e. PreHil -> ( T e. dom K <-> ( T e. L /\ ( T .(+) ( ._|_ ` T ) ) = V ) ) )