Theorem dochoc1

Description: The unit subspace (all vectors) is closed. (Contributed by NM, 16-Feb-2015)

	Ref	Expression
Hypotheses	dochoc1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochoc1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochoc1.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochoc1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochoc1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	dochoc1	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		dochoc1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochoc1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		dochoc1.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4		dochoc1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochoc1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
7	1 2 3 4 6	doch1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ 𝑉 ) = { ( 0g ‘ 𝑈 ) } )
8	7	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) )
9	1 2 3 4 6	doch0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) = 𝑉 )
10	8 9	eqtrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )
11	5 10	syl	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )