Theorem dochexmidat

Description: Special case of excluded middle for the singleton of a vector. (Contributed by NM, 27-Oct-2014)

	Ref	Expression
Hypotheses	dochexmidat.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochexmidat.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochexmidat.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochexmidat.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochexmidat.z	⊢ 0 = ( 0g ‘ 𝑈 )
	dochexmidat.r	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	dochexmidat.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	dochexmidat.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochexmidat.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion	dochexmidat	⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		dochexmidat.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochexmidat.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochexmidat.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochexmidat.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochexmidat.z	⊢ 0 = ( 0g ‘ 𝑈 )
6		dochexmidat.r	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
7		dochexmidat.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
8		dochexmidat.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		dochexmidat.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
10	1 2 3 4 5 8 9	dochnel	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘ { 𝑋 } ) )
11		eqid	⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
12	1 3 8	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
13	1 2 3 4 5 11 8 9	dochsnshp	⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ∈ ( LSHyp ‘ 𝑈 ) )
14	9	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
15	4 6 7 11 12 13 14	lshpnelb	⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { 𝑋 } ) ↔ ( ( ⊥ ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) )
16	10 15	mpbid	⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )