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=BaseW
pjdm2.l ⊢L=LSubSp⁡W
pjdm2.o ⊢⊥˙=ocv⁡W
pjdm2.s ⊢⊕˙=LSSum⁡W
pjdm2.k ⊢K=proj⁡W
Assertion pjdm2 ⊢W∈PreHil→T∈dom⁡K↔T∈L∧T⊕˙⊥˙⁡T=V

Proof

Step Hyp Ref Expression
1 pjdm2.v ⊢V=BaseW
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∈dom⁡K↔T∈L∧Tproj1⁡W⊥˙⁡T:V⟶V
8 eqid ⊢+W=+W
9 eqid ⊢0W=0W
10 eqid ⊢Cntz⁡W=Cntz⁡W
11 phllmod ⊢W∈PreHil→W∈LMod
12 11 adantr ⊢W∈PreHil∧T∈L→W∈LMod
13 2 lsssssubg ⊢W∈LMod→L⊆SubGrp⁡W
14 12 13 syl ⊢W∈PreHil∧T∈L→L⊆SubGrp⁡W
15 simpr ⊢W∈PreHil∧T∈L→T∈L
16 14 15 sseldd ⊢W∈PreHil∧T∈L→T∈SubGrp⁡W
17 1 2 lssss ⊢T∈L→T⊆V
18 1 3 2 ocvlss ⊢W∈PreHil∧T⊆V→⊥˙⁡T∈L
19 17 18 sylan2 ⊢W∈PreHil∧T∈L→⊥˙⁡T∈L
20 14 19 sseldd ⊢W∈PreHil∧T∈L→⊥˙⁡T∈SubGrp⁡W
21 3 2 9 ocvin ⊢W∈PreHil∧T∈L→T∩⊥˙⁡T=0W
22 lmodabl ⊢W∈LMod→W∈Abel
23 12 22 syl ⊢W∈PreHil∧T∈L→W∈Abel
24 10 23 16 20 ablcntzd ⊢W∈PreHil∧T∈L→T⊆Cntz⁡W⁡⊥˙⁡T
25 8 4 9 10 16 20 21 24 6 pj1f ⊢W∈PreHil∧T∈L→Tproj1⁡W⊥˙⁡T:T⊕˙⊥˙⁡T⟶T
26 17 adantl ⊢W∈PreHil∧T∈L→T⊆V
27 25 26 fssd ⊢W∈PreHil∧T∈L→Tproj1⁡W⊥˙⁡T:T⊕˙⊥˙⁡T⟶V
28 fdm ⊢Tproj1⁡W⊥˙⁡T:T⊕˙⊥˙⁡T⟶V→dom⁡Tproj1⁡W⊥˙⁡T=T⊕˙⊥˙⁡T
29 28 eqcomd ⊢Tproj1⁡W⊥˙⁡T:T⊕˙⊥˙⁡T⟶V→T⊕˙⊥˙⁡T=dom⁡Tproj1⁡W⊥˙⁡T
30 fdm ⊢Tproj1⁡W⊥˙⁡T:V⟶V→dom⁡Tproj1⁡W⊥˙⁡T=V
31 30 eqeq2d ⊢Tproj1⁡W⊥˙⁡T:V⟶V→T⊕˙⊥˙⁡T=dom⁡Tproj1⁡W⊥˙⁡T↔T⊕˙⊥˙⁡T=V
32 29 31 syl5ibcom ⊢Tproj1⁡W⊥˙⁡T:T⊕˙⊥˙⁡T⟶V→Tproj1⁡W⊥˙⁡T:V⟶V→T⊕˙⊥˙⁡T=V
33 feq2 ⊢T⊕˙⊥˙⁡T=V→Tproj1⁡W⊥˙⁡T:T⊕˙⊥˙⁡T⟶V↔Tproj1⁡W⊥˙⁡T:V⟶V
34 33 biimpcd ⊢Tproj1⁡W⊥˙⁡T:T⊕˙⊥˙⁡T⟶V→T⊕˙⊥˙⁡T=V→Tproj1⁡W⊥˙⁡T:V⟶V
35 32 34 impbid ⊢Tproj1⁡W⊥˙⁡T:T⊕˙⊥˙⁡T⟶V→Tproj1⁡W⊥˙⁡T:V⟶V↔T⊕˙⊥˙⁡T=V
36 27 35 syl ⊢W∈PreHil∧T∈L→Tproj1⁡W⊥˙⁡T:V⟶V↔T⊕˙⊥˙⁡T=V
37 36 pm5.32da ⊢W∈PreHil→T∈L∧Tproj1⁡W⊥˙⁡T:V⟶V↔T∈L∧T⊕˙⊥˙⁡T=V
38 7 37 bitrid ⊢W∈PreHil→T∈dom⁡K↔T∈L∧T⊕˙⊥˙⁡T=V