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 ∈ PreHil → T ∈ dom ⁡ K ↔ T ∈ 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 ⊢ proj 1 ⁡ W = proj 1 ⁡ W
7 1 2 3 6 5 pjdm ⊢ T ∈ dom ⁡ K ↔ T ∈ L ∧ T proj 1 ⁡ W ⊥ ˙ ⁡ T : V ⟶ V
8 eqid ⊢ + W = + W
9 eqid ⊢ 0 W = 0 W
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 = 0 W
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 → T proj 1 ⁡ W ⊥ ˙ ⁡ T : T ⊕ ˙ ⊥ ˙ ⁡ T ⟶ T
26 17 adantl ⊢ W ∈ PreHil ∧ T ∈ L → T ⊆ V
27 25 26 fssd ⊢ W ∈ PreHil ∧ T ∈ L → T proj 1 ⁡ W ⊥ ˙ ⁡ T : T ⊕ ˙ ⊥ ˙ ⁡ T ⟶ V
28 fdm ⊢ T proj 1 ⁡ W ⊥ ˙ ⁡ T : T ⊕ ˙ ⊥ ˙ ⁡ T ⟶ V → dom ⁡ T proj 1 ⁡ W ⊥ ˙ ⁡ T = T ⊕ ˙ ⊥ ˙ ⁡ T
29 28 eqcomd ⊢ T proj 1 ⁡ W ⊥ ˙ ⁡ T : T ⊕ ˙ ⊥ ˙ ⁡ T ⟶ V → T ⊕ ˙ ⊥ ˙ ⁡ T = dom ⁡ T proj 1 ⁡ W ⊥ ˙ ⁡ T
30 fdm ⊢ T proj 1 ⁡ W ⊥ ˙ ⁡ T : V ⟶ V → dom ⁡ T proj 1 ⁡ W ⊥ ˙ ⁡ T = V
31 30 eqeq2d ⊢ T proj 1 ⁡ W ⊥ ˙ ⁡ T : V ⟶ V → T ⊕ ˙ ⊥ ˙ ⁡ T = dom ⁡ T proj 1 ⁡ W ⊥ ˙ ⁡ T ↔ T ⊕ ˙ ⊥ ˙ ⁡ T = V
32 29 31 syl5ibcom ⊢ T proj 1 ⁡ W ⊥ ˙ ⁡ T : T ⊕ ˙ ⊥ ˙ ⁡ T ⟶ V → T proj 1 ⁡ W ⊥ ˙ ⁡ T : V ⟶ V → T ⊕ ˙ ⊥ ˙ ⁡ T = V
33 feq2 ⊢ T ⊕ ˙ ⊥ ˙ ⁡ T = V → T proj 1 ⁡ W ⊥ ˙ ⁡ T : T ⊕ ˙ ⊥ ˙ ⁡ T ⟶ V ↔ T proj 1 ⁡ W ⊥ ˙ ⁡ T : V ⟶ V
34 33 biimpcd ⊢ T proj 1 ⁡ W ⊥ ˙ ⁡ T : T ⊕ ˙ ⊥ ˙ ⁡ T ⟶ V → T ⊕ ˙ ⊥ ˙ ⁡ T = V → T proj 1 ⁡ W ⊥ ˙ ⁡ T : V ⟶ V
35 32 34 impbid ⊢ T proj 1 ⁡ W ⊥ ˙ ⁡ T : T ⊕ ˙ ⊥ ˙ ⁡ T ⟶ V → T proj 1 ⁡ W ⊥ ˙ ⁡ T : V ⟶ V ↔ T ⊕ ˙ ⊥ ˙ ⁡ T = V
36 27 35 syl ⊢ W ∈ PreHil ∧ T ∈ L → T proj 1 ⁡ W ⊥ ˙ ⁡ T : V ⟶ V ↔ T ⊕ ˙ ⊥ ˙ ⁡ T = V
37 36 pm5.32da ⊢ W ∈ PreHil → T ∈ L ∧ T proj 1 ⁡ W ⊥ ˙ ⁡ T : V ⟶ V ↔ T ∈ L ∧ T ⊕ ˙ ⊥ ˙ ⁡ T = V
38 7 37 bitrid ⊢ W ∈ PreHil → T ∈ dom ⁡ K ↔ T ∈ L ∧ T ⊕ ˙ ⊥ ˙ ⁡ T = V