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

Metamath Proof Explorer

Theorem dih0rn

Description: The zero subspace belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014)

Ref Expression
Hypotheses dih0rn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dih0rn.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dih0rn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dih0rn.o ⊢ 0 = ( 0g ‘ 𝑈 )
Assertion dih0rn ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → { 0 } ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dih0rn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dih0rn.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 dih0rn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dih0rn.o ⊢ 0 = ( 0g ‘ 𝑈 )
5 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
6 5 1 2 3 4 dih0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) = { 0 } )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 7 1 2 dihfn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn ( Base ‘ 𝐾 ) )
9 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
10 9 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ OP )
11 7 5 op0cl ⊢ ( 𝐾 ∈ OP → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
12 10 11 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
13 fnfvelrn ⊢ ( ( 𝐼 Fn ( Base ‘ 𝐾 ) ∧ ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) ∈ ran 𝐼 )
14 8 12 13 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) ∈ ran 𝐼 )
15 6 14 eqeltrrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → { 0 } ∈ ran 𝐼 )