Metamath Proof Explorer


Theorem dih1rn

Description: The full vector space belongs to the range of isomorphism H. (Contributed by NM, 19-Jun-2014)

Ref Expression
Hypotheses dih1rn.h H=LHypK
dih1rn.i I=DIsoHKW
dih1rn.u U=DVecHKW
dih1rn.v V=BaseU
Assertion dih1rn KHLWHVranI

Proof

Step Hyp Ref Expression
1 dih1rn.h H=LHypK
2 dih1rn.i I=DIsoHKW
3 dih1rn.u U=DVecHKW
4 dih1rn.v V=BaseU
5 eqid 1.K=1.K
6 5 1 2 3 4 dih1 KHLWHI1.K=V
7 hlop KHLKOP
8 7 adantr KHLWHKOP
9 eqid BaseK=BaseK
10 9 5 op1cl KOP1.KBaseK
11 8 10 syl KHLWH1.KBaseK
12 9 1 2 dihcl KHLWH1.KBaseKI1.KranI
13 11 12 mpdan KHLWHI1.KranI
14 6 13 eqeltrrd KHLWHVranI