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}={\mathrm{Base}}_{{W}}$
pjdm2.l ${⊢}{L}=\mathrm{LSubSp}\left({W}\right)$
pjdm2.o
pjdm2.s
pjdm2.k ${⊢}{K}=\mathrm{proj}\left({W}\right)$
Assertion pjdm2

Proof

Step Hyp Ref Expression
1 pjdm2.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 pjdm2.l ${⊢}{L}=\mathrm{LSubSp}\left({W}\right)$
3 pjdm2.o
4 pjdm2.s
5 pjdm2.k ${⊢}{K}=\mathrm{proj}\left({W}\right)$
6 eqid ${⊢}{proj}_{1}\left({W}\right)={proj}_{1}\left({W}\right)$
7 1 2 3 6 5 pjdm
8 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
9 eqid ${⊢}{0}_{{W}}={0}_{{W}}$
10 eqid ${⊢}\mathrm{Cntz}\left({W}\right)=\mathrm{Cntz}\left({W}\right)$
11 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
12 11 adantr ${⊢}\left({W}\in \mathrm{PreHil}\wedge {T}\in {L}\right)\to {W}\in \mathrm{LMod}$
13 2 lsssssubg ${⊢}{W}\in \mathrm{LMod}\to {L}\subseteq \mathrm{SubGrp}\left({W}\right)$
14 12 13 syl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {T}\in {L}\right)\to {L}\subseteq \mathrm{SubGrp}\left({W}\right)$
15 simpr ${⊢}\left({W}\in \mathrm{PreHil}\wedge {T}\in {L}\right)\to {T}\in {L}$
16 14 15 sseldd ${⊢}\left({W}\in \mathrm{PreHil}\wedge {T}\in {L}\right)\to {T}\in \mathrm{SubGrp}\left({W}\right)$
17 1 2 lssss ${⊢}{T}\in {L}\to {T}\subseteq {V}$
18 1 3 2 ocvlss
19 17 18 sylan2
20 14 19 sseldd
21 3 2 9 ocvin
22 lmodabl ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Abel}$
23 12 22 syl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {T}\in {L}\right)\to {W}\in \mathrm{Abel}$
24 10 23 16 20 ablcntzd
25 8 4 9 10 16 20 21 24 6 pj1f
26 17 adantl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {T}\in {L}\right)\to {T}\subseteq {V}$
27 25 26 fssd
28 fdm
29 28 eqcomd
30 fdm
31 30 eqeq2d
32 29 31 syl5ibcom
33 feq2
34 33 biimpcd
35 32 34 impbid
36 27 35 syl
37 36 pm5.32da
38 7 37 syl5bb