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 ⊢ H = LHyp ⁡ K
dih0rn.i ⊢ I = DIsoH ⁡ K ⁡ W
dih0rn.u ⊢ U = DVecH ⁡ K ⁡ W
dih0rn.o ⊢ 0 ˙ = 0 U
Assertion dih0rn ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ ran ⁡ I

Proof

Step Hyp Ref Expression
1 dih0rn.h ⊢ H = LHyp ⁡ K
2 dih0rn.i ⊢ I = DIsoH ⁡ K ⁡ W
3 dih0rn.u ⊢ U = DVecH ⁡ K ⁡ W
4 dih0rn.o ⊢ 0 ˙ = 0 U
5 eqid ⊢ 0. ⁡ K = 0. ⁡ K
6 5 1 2 3 4 dih0 ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 0. ⁡ K = 0 ˙
7 eqid ⊢ Base K = Base K
8 7 1 2 dihfn ⊢ K ∈ HL ∧ W ∈ H → I Fn Base K
9 hlop ⊢ K ∈ HL → K ∈ OP
10 9 adantr ⊢ K ∈ HL ∧ W ∈ H → K ∈ OP
11 7 5 op0cl ⊢ K ∈ OP → 0. ⁡ K ∈ Base K
12 10 11 syl ⊢ K ∈ HL ∧ W ∈ H → 0. ⁡ K ∈ Base K
13 fnfvelrn ⊢ I Fn Base K ∧ 0. ⁡ K ∈ Base K → I ⁡ 0. ⁡ K ∈ ran ⁡ I
14 8 12 13 syl2anc ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 0. ⁡ K ∈ ran ⁡ I
15 6 14 eqeltrrd ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ ran ⁡ I