This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )