Step |
Hyp |
Ref |
Expression |
1 |
|
lmhmf1o.x |
⊢ 𝑋 = ( Base ‘ 𝑆 ) |
2 |
|
lmhmf1o.y |
⊢ 𝑌 = ( Base ‘ 𝑇 ) |
3 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑇 ) = ( ·𝑠 ‘ 𝑇 ) |
4 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 ) |
5 |
|
eqid |
⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 ) |
6 |
|
eqid |
⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 ) |
7 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) ) |
8 |
|
lmhmlmod2 |
⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod ) |
9 |
8
|
adantr |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → 𝑇 ∈ LMod ) |
10 |
|
lmhmlmod1 |
⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod ) |
11 |
10
|
adantr |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → 𝑆 ∈ LMod ) |
12 |
6 5
|
lmhmsca |
⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) ) |
13 |
12
|
eqcomd |
⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑇 ) ) |
14 |
13
|
adantr |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑇 ) ) |
15 |
|
lmghm |
⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) |
16 |
1 2
|
ghmf1o |
⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ) ) |
17 |
15 16
|
syl |
⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ) ) |
18 |
17
|
biimpa |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ◡ 𝐹 ∈ ( 𝑇 GrpHom 𝑆 ) ) |
19 |
|
simpll |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ 𝑌 ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ) |
20 |
14
|
fveq2d |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) |
21 |
20
|
eleq2d |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ↔ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) ) |
22 |
21
|
biimpar |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) |
23 |
22
|
adantrr |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ 𝑌 ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) |
24 |
|
f1ocnv |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) |
25 |
|
f1of |
⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 ) |
26 |
24 25
|
syl |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 ) |
27 |
26
|
adantl |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ◡ 𝐹 : 𝑌 ⟶ 𝑋 ) |
28 |
27
|
ffvelrnda |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑏 ∈ 𝑌 ) → ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝑋 ) |
29 |
28
|
adantrl |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ 𝑌 ) ) → ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝑋 ) |
30 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) ) |
31 |
6 30 1 4 3
|
lmhmlin |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) ) |
32 |
19 23 29 31
|
syl3anc |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ 𝑌 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) ) |
33 |
|
f1ocnvfv2 |
⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑏 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = 𝑏 ) |
34 |
33
|
ad2ant2l |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ 𝑌 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = 𝑏 ) |
35 |
34
|
oveq2d |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ 𝑌 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ) |
36 |
32 35
|
eqtrd |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ 𝑌 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ) |
37 |
|
simplr |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ 𝑌 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) |
38 |
11
|
adantr |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ 𝑌 ) ) → 𝑆 ∈ LMod ) |
39 |
1 6 4 30
|
lmodvscl |
⊢ ( ( 𝑆 ∈ LMod ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝑋 ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑏 ) ) ∈ 𝑋 ) |
40 |
38 23 29 39
|
syl3anc |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ 𝑌 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑏 ) ) ∈ 𝑋 ) |
41 |
|
f1ocnvfv |
⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑏 ) ) ∈ 𝑋 ) → ( ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) → ( ◡ 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑏 ) ) ) ) |
42 |
37 40 41
|
syl2anc |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) → ( ◡ 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑏 ) ) ) ) |
43 |
36 42
|
mpd |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ 𝑏 ∈ 𝑌 ) ) → ( ◡ 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑇 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑆 ) ( ◡ 𝐹 ‘ 𝑏 ) ) ) |
44 |
2 3 4 5 6 7 9 11 14 18 43
|
islmhmd |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ◡ 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) ) |
45 |
1 2
|
lmhmf |
⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : 𝑋 ⟶ 𝑌 ) |
46 |
45
|
ffnd |
⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 Fn 𝑋 ) |
47 |
46
|
adantr |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ◡ 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) ) → 𝐹 Fn 𝑋 ) |
48 |
2 1
|
lmhmf |
⊢ ( ◡ 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) → ◡ 𝐹 : 𝑌 ⟶ 𝑋 ) |
49 |
48
|
adantl |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ◡ 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) ) → ◡ 𝐹 : 𝑌 ⟶ 𝑋 ) |
50 |
49
|
ffnd |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ◡ 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) ) → ◡ 𝐹 Fn 𝑌 ) |
51 |
|
dff1o4 |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ ( 𝐹 Fn 𝑋 ∧ ◡ 𝐹 Fn 𝑌 ) ) |
52 |
47 50 51
|
sylanbrc |
⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ◡ 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) |
53 |
44 52
|
impbida |
⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ ◡ 𝐹 ∈ ( 𝑇 LMHom 𝑆 ) ) ) |