Step |
Hyp |
Ref |
Expression |
1 |
|
lmhmf1o.x |
|- X = ( Base ` S ) |
2 |
|
lmhmf1o.y |
|- Y = ( Base ` T ) |
3 |
|
eqid |
|- ( .s ` T ) = ( .s ` T ) |
4 |
|
eqid |
|- ( .s ` S ) = ( .s ` S ) |
5 |
|
eqid |
|- ( Scalar ` T ) = ( Scalar ` T ) |
6 |
|
eqid |
|- ( Scalar ` S ) = ( Scalar ` S ) |
7 |
|
eqid |
|- ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` T ) ) |
8 |
|
lmhmlmod2 |
|- ( F e. ( S LMHom T ) -> T e. LMod ) |
9 |
8
|
adantr |
|- ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> T e. LMod ) |
10 |
|
lmhmlmod1 |
|- ( F e. ( S LMHom T ) -> S e. LMod ) |
11 |
10
|
adantr |
|- ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> S e. LMod ) |
12 |
6 5
|
lmhmsca |
|- ( F e. ( S LMHom T ) -> ( Scalar ` T ) = ( Scalar ` S ) ) |
13 |
12
|
eqcomd |
|- ( F e. ( S LMHom T ) -> ( Scalar ` S ) = ( Scalar ` T ) ) |
14 |
13
|
adantr |
|- ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> ( Scalar ` S ) = ( Scalar ` T ) ) |
15 |
|
lmghm |
|- ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) ) |
16 |
1 2
|
ghmf1o |
|- ( F e. ( S GrpHom T ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( T GrpHom S ) ) ) |
17 |
15 16
|
syl |
|- ( F e. ( S LMHom T ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( T GrpHom S ) ) ) |
18 |
17
|
biimpa |
|- ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> `' F e. ( T GrpHom S ) ) |
19 |
|
simpll |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> F e. ( S LMHom T ) ) |
20 |
14
|
fveq2d |
|- ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` T ) ) ) |
21 |
20
|
eleq2d |
|- ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> ( a e. ( Base ` ( Scalar ` S ) ) <-> a e. ( Base ` ( Scalar ` T ) ) ) ) |
22 |
21
|
biimpar |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ a e. ( Base ` ( Scalar ` T ) ) ) -> a e. ( Base ` ( Scalar ` S ) ) ) |
23 |
22
|
adantrr |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> a e. ( Base ` ( Scalar ` S ) ) ) |
24 |
|
f1ocnv |
|- ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X ) |
25 |
|
f1of |
|- ( `' F : Y -1-1-onto-> X -> `' F : Y --> X ) |
26 |
24 25
|
syl |
|- ( F : X -1-1-onto-> Y -> `' F : Y --> X ) |
27 |
26
|
adantl |
|- ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> `' F : Y --> X ) |
28 |
27
|
ffvelrnda |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ b e. Y ) -> ( `' F ` b ) e. X ) |
29 |
28
|
adantrl |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( `' F ` b ) e. X ) |
30 |
|
eqid |
|- ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) ) |
31 |
6 30 1 4 3
|
lmhmlin |
|- ( ( F e. ( S LMHom T ) /\ a e. ( Base ` ( Scalar ` S ) ) /\ ( `' F ` b ) e. X ) -> ( F ` ( a ( .s ` S ) ( `' F ` b ) ) ) = ( a ( .s ` T ) ( F ` ( `' F ` b ) ) ) ) |
32 |
19 23 29 31
|
syl3anc |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( F ` ( a ( .s ` S ) ( `' F ` b ) ) ) = ( a ( .s ` T ) ( F ` ( `' F ` b ) ) ) ) |
33 |
|
f1ocnvfv2 |
|- ( ( F : X -1-1-onto-> Y /\ b e. Y ) -> ( F ` ( `' F ` b ) ) = b ) |
34 |
33
|
ad2ant2l |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( F ` ( `' F ` b ) ) = b ) |
35 |
34
|
oveq2d |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( a ( .s ` T ) ( F ` ( `' F ` b ) ) ) = ( a ( .s ` T ) b ) ) |
36 |
32 35
|
eqtrd |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( F ` ( a ( .s ` S ) ( `' F ` b ) ) ) = ( a ( .s ` T ) b ) ) |
37 |
|
simplr |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> F : X -1-1-onto-> Y ) |
38 |
11
|
adantr |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> S e. LMod ) |
39 |
1 6 4 30
|
lmodvscl |
|- ( ( S e. LMod /\ a e. ( Base ` ( Scalar ` S ) ) /\ ( `' F ` b ) e. X ) -> ( a ( .s ` S ) ( `' F ` b ) ) e. X ) |
40 |
38 23 29 39
|
syl3anc |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( a ( .s ` S ) ( `' F ` b ) ) e. X ) |
41 |
|
f1ocnvfv |
|- ( ( F : X -1-1-onto-> Y /\ ( a ( .s ` S ) ( `' F ` b ) ) e. X ) -> ( ( F ` ( a ( .s ` S ) ( `' F ` b ) ) ) = ( a ( .s ` T ) b ) -> ( `' F ` ( a ( .s ` T ) b ) ) = ( a ( .s ` S ) ( `' F ` b ) ) ) ) |
42 |
37 40 41
|
syl2anc |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( ( F ` ( a ( .s ` S ) ( `' F ` b ) ) ) = ( a ( .s ` T ) b ) -> ( `' F ` ( a ( .s ` T ) b ) ) = ( a ( .s ` S ) ( `' F ` b ) ) ) ) |
43 |
36 42
|
mpd |
|- ( ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) /\ ( a e. ( Base ` ( Scalar ` T ) ) /\ b e. Y ) ) -> ( `' F ` ( a ( .s ` T ) b ) ) = ( a ( .s ` S ) ( `' F ` b ) ) ) |
44 |
2 3 4 5 6 7 9 11 14 18 43
|
islmhmd |
|- ( ( F e. ( S LMHom T ) /\ F : X -1-1-onto-> Y ) -> `' F e. ( T LMHom S ) ) |
45 |
1 2
|
lmhmf |
|- ( F e. ( S LMHom T ) -> F : X --> Y ) |
46 |
45
|
ffnd |
|- ( F e. ( S LMHom T ) -> F Fn X ) |
47 |
46
|
adantr |
|- ( ( F e. ( S LMHom T ) /\ `' F e. ( T LMHom S ) ) -> F Fn X ) |
48 |
2 1
|
lmhmf |
|- ( `' F e. ( T LMHom S ) -> `' F : Y --> X ) |
49 |
48
|
adantl |
|- ( ( F e. ( S LMHom T ) /\ `' F e. ( T LMHom S ) ) -> `' F : Y --> X ) |
50 |
49
|
ffnd |
|- ( ( F e. ( S LMHom T ) /\ `' F e. ( T LMHom S ) ) -> `' F Fn Y ) |
51 |
|
dff1o4 |
|- ( F : X -1-1-onto-> Y <-> ( F Fn X /\ `' F Fn Y ) ) |
52 |
47 50 51
|
sylanbrc |
|- ( ( F e. ( S LMHom T ) /\ `' F e. ( T LMHom S ) ) -> F : X -1-1-onto-> Y ) |
53 |
44 52
|
impbida |
|- ( F e. ( S LMHom T ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( T LMHom S ) ) ) |