Description: The isomorphic image of a basis is a basis. (Contributed by Stefan O'Rear, 26-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lmimlbs.j | |
|
lmimlbs.k | |
||
Assertion | lmimlbs | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmimlbs.j | |
|
2 | lmimlbs.k | |
|
3 | lmimlmhm | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 4 5 | lmimf1o | |
7 | f1of1 | |
|
8 | 6 7 | syl | |
9 | 1 | lbslinds | |
10 | 9 | sseli | |
11 | 4 5 | lindsmm2 | |
12 | 3 8 10 11 | syl2an3an | |
13 | eqid | |
|
14 | 4 1 13 | lbssp | |
15 | 14 | adantl | |
16 | 15 | imaeq2d | |
17 | 4 1 | lbsss | |
18 | eqid | |
|
19 | 4 13 18 | lmhmlsp | |
20 | 3 17 19 | syl2an | |
21 | 6 | adantr | |
22 | f1ofo | |
|
23 | foima | |
|
24 | 21 22 23 | 3syl | |
25 | 16 20 24 | 3eqtr3d | |
26 | 5 2 18 | islbs4 | |
27 | 12 25 26 | sylanbrc | |