Theorem dih0sb

Description: A subspace is zero iff the converse of its isomorphism is lattice zero. (Contributed by NM, 17-Aug-2014)

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

Proof

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