Theorem dochoc0

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

	Ref	Expression
Hypotheses	dochoc0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochoc0.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochoc0.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochoc0.z	⊢ 0 = ( 0g ‘ 𝑈 )
	dochoc0.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	dochoc0	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ { 0 } ) ) = { 0 } )

Proof

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