Metamath Proof Explorer

Theorem ocvin

Description: An orthocomplement has trivial intersection with the original subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses ocv2ss.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
ocvin.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
ocvin.z ⊢ 0 = ( 0g ‘ 𝑊 )
Assertion ocvin ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) → ( 𝑆 ∩ ( ⊥ ‘ 𝑆 ) ) = { 0 } )

Proof

Step Hyp Ref Expression
1 ocv2ss.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
2 ocvin.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
3 ocvin.z ⊢ 0 = ( 0g ‘ 𝑊 )
4 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
6 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
7 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
8 4 5 6 7 1 ocvi ⊢ ( ( 𝑥 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
9 8 ancoms ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( ⊥ ‘ 𝑆 ) ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
10 9 adantl ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
11 simpll ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑊 ∈ PreHil )
12 4 2 lssel ⊢ ( ( 𝑆 ∈ 𝐿 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
13 12 ad2ant2lr ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
14 6 5 4 7 3 ipeq0 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ 𝑥 = 0 ) )
15 11 13 14 syl2anc ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ 𝑥 = 0 ) )
16 10 15 mpbid ⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑥 = 0 )
17 16 ex ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) → ( ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( ⊥ ‘ 𝑆 ) ) → 𝑥 = 0 ) )
18 elin ⊢ ( 𝑥 ∈ ( 𝑆 ∩ ( ⊥ ‘ 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ ( ⊥ ‘ 𝑆 ) ) )
19 velsn ⊢ ( 𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
20 17 18 19 3imtr4g ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) → ( 𝑥 ∈ ( 𝑆 ∩ ( ⊥ ‘ 𝑆 ) ) → 𝑥 ∈ { 0 } ) )
21 20 ssrdv ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) → ( 𝑆 ∩ ( ⊥ ‘ 𝑆 ) ) ⊆ { 0 } )
22 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
23 4 2 lssss ⊢ ( 𝑆 ∈ 𝐿 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
24 4 1 2 ocvlss ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐿 )
25 23 24 sylan2 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐿 )
26 2 lssincl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝐿 ∧ ( ⊥ ‘ 𝑆 ) ∈ 𝐿 ) → ( 𝑆 ∩ ( ⊥ ‘ 𝑆 ) ) ∈ 𝐿 )
27 22 26 syl3an1 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ∧ ( ⊥ ‘ 𝑆 ) ∈ 𝐿 ) → ( 𝑆 ∩ ( ⊥ ‘ 𝑆 ) ) ∈ 𝐿 )
28 25 27 mpd3an3 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) → ( 𝑆 ∩ ( ⊥ ‘ 𝑆 ) ) ∈ 𝐿 )
29 3 2 lss0ss ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑆 ∩ ( ⊥ ‘ 𝑆 ) ) ∈ 𝐿 ) → { 0 } ⊆ ( 𝑆 ∩ ( ⊥ ‘ 𝑆 ) ) )
30 22 28 29 syl2an2r ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) → { 0 } ⊆ ( 𝑆 ∩ ( ⊥ ‘ 𝑆 ) ) )
31 21 30 eqssd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿 ) → ( 𝑆 ∩ ( ⊥ ‘ 𝑆 ) ) = { 0 } )