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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	pjdm2.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
	pjdm2.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
	pjdm2.s	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	pjdm2.k	⊢ 𝐾 = ( proj ‘ 𝑊 )
Assertion	pjdm2	⊢ ( 𝑊 ∈ PreHil → ( 𝑇 ∈ dom 𝐾 ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) = 𝑉 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjdm2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		pjdm2.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
3		pjdm2.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
4		pjdm2.s	⊢ ⊕ = ( LSSum ‘ 𝑊 )
5		pjdm2.k	⊢ 𝐾 = ( proj ‘ 𝑊 )
6		eqid	⊢ ( proj1 ‘ 𝑊 ) = ( proj1 ‘ 𝑊 )
7	1 2 3 6 5	pjdm	⊢ ( 𝑇 ∈ dom 𝐾 ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 ) )
8		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
9		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
10		eqid	⊢ ( Cntz ‘ 𝑊 ) = ( Cntz ‘ 𝑊 )
11		phllmod	⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
12	11	adantr	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → 𝑊 ∈ LMod )
13	2	lsssssubg	⊢ ( 𝑊 ∈ LMod → 𝐿 ⊆ ( SubGrp ‘ 𝑊 ) )
14	12 13	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → 𝐿 ⊆ ( SubGrp ‘ 𝑊 ) )
15		simpr	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → 𝑇 ∈ 𝐿 )
16	14 15	sseldd	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
17	1 2	lssss	⊢ ( 𝑇 ∈ 𝐿 → 𝑇 ⊆ 𝑉 )
18	1 3 2	ocvlss	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑇 ) ∈ 𝐿 )
19	17 18	sylan2	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → ( ⊥ ‘ 𝑇 ) ∈ 𝐿 )
20	14 19	sseldd	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → ( ⊥ ‘ 𝑇 ) ∈ ( SubGrp ‘ 𝑊 ) )
21	3 2 9	ocvin	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ∩ ( ⊥ ‘ 𝑇 ) ) = { ( 0g ‘ 𝑊 ) } )
22		lmodabl	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
23	12 22	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → 𝑊 ∈ Abel )
24	10 23 16 20	ablcntzd	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → 𝑇 ⊆ ( ( Cntz ‘ 𝑊 ) ‘ ( ⊥ ‘ 𝑇 ) ) )
25	8 4 9 10 16 20 21 24 6	pj1f	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) ⟶ 𝑇 )
26	17	adantl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → 𝑇 ⊆ 𝑉 )
27	25 26	fssd	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) ⟶ 𝑉 )
28		fdm	⊢ ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) ⟶ 𝑉 → dom ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) = ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) )
29	28	eqcomd	⊢ ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) ⟶ 𝑉 → ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) = dom ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) )
30		fdm	⊢ ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 → dom ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) = 𝑉 )
31	30	eqeq2d	⊢ ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 → ( ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) = dom ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) ↔ ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) = 𝑉 ) )
32	29 31	syl5ibcom	⊢ ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) ⟶ 𝑉 → ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 → ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) = 𝑉 ) )
33		feq2	⊢ ( ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) = 𝑉 → ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) ⟶ 𝑉 ↔ ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 ) )
34	33	biimpcd	⊢ ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) ⟶ 𝑉 → ( ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) = 𝑉 → ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 ) )
35	32 34	impbid	⊢ ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) ⟶ 𝑉 → ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 ↔ ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) = 𝑉 ) )
36	27 35	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ 𝐿 ) → ( ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 ↔ ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) = 𝑉 ) )
37	36	pm5.32da	⊢ ( 𝑊 ∈ PreHil → ( ( 𝑇 ∈ 𝐿 ∧ ( 𝑇 ( proj1 ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 ) ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) = 𝑉 ) ) )
38	7 37	bitrid	⊢ ( 𝑊 ∈ PreHil → ( 𝑇 ∈ dom 𝐾 ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑇 ⊕ ( ⊥ ‘ 𝑇 ) ) = 𝑉 ) ) )