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