Theorem dochnel2

Description: A nonzero member of a subspace doesn't belong to the orthocomplement of the subspace. (Contributed by NM, 28-Feb-2015)

	Ref	Expression
Hypotheses	dochnoncon.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochnoncon.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochnoncon.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
	dochnoncon.z	⊢ 0 = ( 0g ‘ 𝑈 )
	dochnoncon.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochnel2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochnel2.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
	dochnel2.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑇 ∖ { 0 } ) )
Assertion	dochnel2	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		dochnoncon.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochnoncon.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		dochnoncon.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
4		dochnoncon.z	⊢ 0 = ( 0g ‘ 𝑈 )
5		dochnoncon.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
6		dochnel2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		dochnel2.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
8		dochnel2.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑇 ∖ { 0 } ) )
9	8	eldifbd	⊢ ( 𝜑 → ¬ 𝑋 ∈ { 0 } )
10	8	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑇 )
11		elin	⊢ ( 𝑋 ∈ ( 𝑇 ∩ ( ⊥ ‘ 𝑇 ) ) ↔ ( 𝑋 ∈ 𝑇 ∧ 𝑋 ∈ ( ⊥ ‘ 𝑇 ) ) )
12	1 2 3 4 5	dochnoncon	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑇 ∈ 𝑆 ) → ( 𝑇 ∩ ( ⊥ ‘ 𝑇 ) ) = { 0 } )
13	6 7 12	syl2anc	⊢ ( 𝜑 → ( 𝑇 ∩ ( ⊥ ‘ 𝑇 ) ) = { 0 } )
14	13	eleq2d	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑇 ∩ ( ⊥ ‘ 𝑇 ) ) ↔ 𝑋 ∈ { 0 } ) )
15	11 14	bitr3id	⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝑇 ∧ 𝑋 ∈ ( ⊥ ‘ 𝑇 ) ) ↔ 𝑋 ∈ { 0 } ) )
16	15	biimpd	⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝑇 ∧ 𝑋 ∈ ( ⊥ ‘ 𝑇 ) ) → 𝑋 ∈ { 0 } ) )
17	10 16	mpand	⊢ ( 𝜑 → ( 𝑋 ∈ ( ⊥ ‘ 𝑇 ) → 𝑋 ∈ { 0 } ) )
18	9 17	mtod	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘ 𝑇 ) )