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 } )