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 ⊢ 𝐾 = ( proj ‘ 𝑊 )
ocvpj.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
Assertion ocvpj ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ⊥ ‘ 𝑇 ) ∈ dom 𝐾 )

Proof

Step Hyp Ref Expression
1 ocvpj.k ⊢ 𝐾 = ( proj ‘ 𝑊 )
2 ocvpj.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
3 eqid ⊢ ( ClSubSp ‘ 𝑊 ) = ( ClSubSp ‘ 𝑊 )
4 1 3 pjcss ⊢ ( 𝑊 ∈ PreHil → dom 𝐾 ⊆ ( ClSubSp ‘ 𝑊 ) )
5 4 sselda ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 ∈ ( ClSubSp ‘ 𝑊 ) )
6 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7 6 3 cssss ⊢ ( 𝑇 ∈ ( ClSubSp ‘ 𝑊 ) → 𝑇 ⊆ ( Base ‘ 𝑊 ) )
8 5 7 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 ⊆ ( Base ‘ 𝑊 ) )
9 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
10 6 2 9 ocvlss ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ⊆ ( Base ‘ 𝑊 ) ) → ( ⊥ ‘ 𝑇 ) ∈ ( LSubSp ‘ 𝑊 ) )
11 8 10 syldan ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ⊥ ‘ 𝑇 ) ∈ ( LSubSp ‘ 𝑊 ) )
12 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
13 12 adantr ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑊 ∈ LMod )
14 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
15 13 14 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑊 ∈ Abel )
16 9 lsssssubg ⊢ ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
17 13 16 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
18 17 11 sseldd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ⊥ ‘ 𝑇 ) ∈ ( SubGrp ‘ 𝑊 ) )
19 3 9 csslss ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ ( ClSubSp ‘ 𝑊 ) ) → 𝑇 ∈ ( LSubSp ‘ 𝑊 ) )
20 5 19 syldan ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 ∈ ( LSubSp ‘ 𝑊 ) )
21 17 20 sseldd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
22 eqid ⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
23 22 lsmcom ⊢ ( ( 𝑊 ∈ Abel ∧ ( ⊥ ‘ 𝑇 ) ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( ⊥ ‘ 𝑇 ) ( LSSum ‘ 𝑊 ) 𝑇 ) = ( 𝑇 ( LSSum ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) )
24 15 18 21 23 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ( ⊥ ‘ 𝑇 ) ( LSSum ‘ 𝑊 ) 𝑇 ) = ( 𝑇 ( LSSum ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) )
25 2 3 cssi ⊢ ( 𝑇 ∈ ( ClSubSp ‘ 𝑊 ) → 𝑇 = ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) )
26 5 25 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → 𝑇 = ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) )
27 26 oveq2d ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ( ⊥ ‘ 𝑇 ) ( LSSum ‘ 𝑊 ) 𝑇 ) = ( ( ⊥ ‘ 𝑇 ) ( LSSum ‘ 𝑊 ) ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) ) )
28 6 9 2 22 1 pjdm2 ⊢ ( 𝑊 ∈ PreHil → ( 𝑇 ∈ dom 𝐾 ↔ ( 𝑇 ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑇 ( LSSum ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) = ( Base ‘ 𝑊 ) ) ) )
29 28 simplbda ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( 𝑇 ( LSSum ‘ 𝑊 ) ( ⊥ ‘ 𝑇 ) ) = ( Base ‘ 𝑊 ) )
30 24 27 29 3eqtr3d ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ( ⊥ ‘ 𝑇 ) ( LSSum ‘ 𝑊 ) ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) ) = ( Base ‘ 𝑊 ) )
31 6 9 2 22 1 pjdm2 ⊢ ( 𝑊 ∈ PreHil → ( ( ⊥ ‘ 𝑇 ) ∈ dom 𝐾 ↔ ( ( ⊥ ‘ 𝑇 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( ( ⊥ ‘ 𝑇 ) ( LSSum ‘ 𝑊 ) ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) ) = ( Base ‘ 𝑊 ) ) ) )
32 31 adantr ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ( ⊥ ‘ 𝑇 ) ∈ dom 𝐾 ↔ ( ( ⊥ ‘ 𝑇 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( ( ⊥ ‘ 𝑇 ) ( LSSum ‘ 𝑊 ) ( ⊥ ‘ ( ⊥ ‘ 𝑇 ) ) ) = ( Base ‘ 𝑊 ) ) ) )
33 11 30 32 mpbir2and ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾 ) → ( ⊥ ‘ 𝑇 ) ∈ dom 𝐾 )