Metamath Proof Explorer

Theorem ocvpj

Description: The orthocomplement of a projection subspace is a projection subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses ocvpj.k 
|- K = ( proj ` W )
ocvpj.o 
|- ._|_ = ( ocv ` W )
Assertion ocvpj 
|- ( ( W e. PreHil /\ T e. dom K ) -> ( ._|_ ` T ) e. dom K )

Proof

Step Hyp Ref Expression
1 ocvpj.k 
 |-  K = ( proj ` W )
2 ocvpj.o 
 |-  ._|_ = ( ocv ` W )
3 eqid 
 |-  ( ClSubSp ` W ) = ( ClSubSp ` W )
4 1 3 pjcss 
 |-  ( W e. PreHil -> dom K C_ ( ClSubSp ` W ) )
5 4 sselda 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T e. ( ClSubSp ` W ) )
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 6 3 cssss 
 |-  ( T e. ( ClSubSp ` W ) -> T C_ ( Base ` W ) )
8 5 7 syl 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T C_ ( Base ` W ) )
9 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
10 6 2 9 ocvlss 
 |-  ( ( W e. PreHil /\ T C_ ( Base ` W ) ) -> ( ._|_ ` T ) e. ( LSubSp ` W ) )
11 8 10 syldan 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( ._|_ ` T ) e. ( LSubSp ` W ) )
12 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
13 12 adantr 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> W e. LMod )
14 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
15 13 14 syl 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> W e. Abel )
16 9 lsssssubg 
 |-  ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
17 13 16 syl 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
18 17 11 sseldd 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( ._|_ ` T ) e. ( SubGrp ` W ) )
19 3 9 csslss 
 |-  ( ( W e. PreHil /\ T e. ( ClSubSp ` W ) ) -> T e. ( LSubSp ` W ) )
20 5 19 syldan 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T e. ( LSubSp ` W ) )
21 17 20 sseldd 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T e. ( SubGrp ` W ) )
22 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
23 22 lsmcom 
 |-  ( ( W e. Abel /\ ( ._|_ ` T ) e. ( SubGrp ` W ) /\ T e. ( SubGrp ` W ) ) -> ( ( ._|_ ` T ) ( LSSum ` W ) T ) = ( T ( LSSum ` W ) ( ._|_ ` T ) ) )
24 15 18 21 23 syl3anc 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( ( ._|_ ` T ) ( LSSum ` W ) T ) = ( T ( LSSum ` W ) ( ._|_ ` T ) ) )
25 2 3 cssi 
 |-  ( T e. ( ClSubSp ` W ) -> T = ( ._|_ ` ( ._|_ ` T ) ) )
26 5 25 syl 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T = ( ._|_ ` ( ._|_ ` T ) ) )
27 26 oveq2d 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( ( ._|_ ` T ) ( LSSum ` W ) T ) = ( ( ._|_ ` T ) ( LSSum ` W ) ( ._|_ ` ( ._|_ ` T ) ) ) )
28 6 9 2 22 1 pjdm2 
 |-  ( W e. PreHil -> ( T e. dom K <-> ( T e. ( LSubSp ` W ) /\ ( T ( LSSum ` W ) ( ._|_ ` T ) ) = ( Base ` W ) ) ) )
29 28 simplbda 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( T ( LSSum ` W ) ( ._|_ ` T ) ) = ( Base ` W ) )
30 24 27 29 3eqtr3d 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( ( ._|_ ` T ) ( LSSum ` W ) ( ._|_ ` ( ._|_ ` T ) ) ) = ( Base ` W ) )
31 6 9 2 22 1 pjdm2 
 |-  ( W e. PreHil -> ( ( ._|_ ` T ) e. dom K <-> ( ( ._|_ ` T ) e. ( LSubSp ` W ) /\ ( ( ._|_ ` T ) ( LSSum ` W ) ( ._|_ ` ( ._|_ ` T ) ) ) = ( Base ` W ) ) ) )
32 31 adantr 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( ( ._|_ ` T ) e. dom K <-> ( ( ._|_ ` T ) e. ( LSubSp ` W ) /\ ( ( ._|_ ` T ) ( LSSum ` W ) ( ._|_ ` ( ._|_ ` T ) ) ) = ( Base ` W ) ) ) )
33 11 30 32 mpbir2and 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( ._|_ ` T ) e. dom K )