Theorem dih0vbN

Description: A vector is zero iff its span is the isomorphism of lattice zero. (Contributed by NM, 16-Aug-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dih0vb.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dih0vb.o	⊢ 0 = ( 0. ‘ 𝐾 )
	dih0vb.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dih0vb.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dih0vb.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dih0vb.z	⊢ 𝑍 = ( 0g ‘ 𝑈 )
	dih0vb.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	dih0vb.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dih0vb.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	dih0vbN	⊢ ( 𝜑 → ( 𝑋 = 𝑍 ↔ ( 𝑁 ‘ { 𝑋 } ) = ( 𝐼 ‘ 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dih0vb.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dih0vb.o	⊢ 0 = ( 0. ‘ 𝐾 )
3		dih0vb.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4		dih0vb.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		dih0vb.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
6		dih0vb.z	⊢ 𝑍 = ( 0g ‘ 𝑈 )
7		dih0vb.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8		dih0vb.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		dih0vb.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10	2 1 3 4 6	dih0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 0 ) = { 𝑍 } )
11	8 10	syl	⊢ ( 𝜑 → ( 𝐼 ‘ 0 ) = { 𝑍 } )
12	11	eqeq2d	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = ( 𝐼 ‘ 0 ) ↔ ( 𝑁 ‘ { 𝑋 } ) = { 𝑍 } ) )
13	1 4 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
14	5 6 7	lspsneq0	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) = { 𝑍 } ↔ 𝑋 = 𝑍 ) )
15	13 9 14	syl2anc	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) = { 𝑍 } ↔ 𝑋 = 𝑍 ) )
16	12 15	bitr2d	⊢ ( 𝜑 → ( 𝑋 = 𝑍 ↔ ( 𝑁 ‘ { 𝑋 } ) = ( 𝐼 ‘ 0 ) ) )