Description: The full vector space belongs to the range of isomorphism H. (Contributed by NM, 19-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dih1rn.h | |
|
dih1rn.i | |
||
dih1rn.u | |
||
dih1rn.v | |
||
Assertion | dih1rn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dih1rn.h | |
|
2 | dih1rn.i | |
|
3 | dih1rn.u | |
|
4 | dih1rn.v | |
|
5 | eqid | |
|
6 | 5 1 2 3 4 | dih1 | |
7 | hlop | |
|
8 | 7 | adantr | |
9 | eqid | |
|
10 | 9 5 | op1cl | |
11 | 8 10 | syl | |
12 | 9 1 2 | dihcl | |
13 | 11 12 | mpdan | |
14 | 6 13 | eqeltrrd | |