Step | Hyp | Ref
| Expression |
1 | | lmhmf1o.y |
. . 3
⊢ 𝑌 = (Base‘𝑇) |
2 | | eqid 2610 |
. . 3
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) |
3 | | eqid 2610 |
. . 3
⊢ (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆) |
4 | | eqid 2610 |
. . 3
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) |
5 | | eqid 2610 |
. . 3
⊢
(Scalar‘𝑆) =
(Scalar‘𝑆) |
6 | | eqid 2610 |
. . 3
⊢
(Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇)) |
7 | | lmhmlmod2 18853 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
8 | 7 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → 𝑇 ∈ LMod) |
9 | | lmhmlmod1 18854 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
10 | 9 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → 𝑆 ∈ LMod) |
11 | 5, 4 | lmhmsca 18851 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑇) = (Scalar‘𝑆)) |
12 | 11 | eqcomd 2616 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑆) = (Scalar‘𝑇)) |
13 | 12 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → (Scalar‘𝑆) = (Scalar‘𝑇)) |
14 | | lmghm 18852 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
15 | | lmhmf1o.x |
. . . . . 6
⊢ 𝑋 = (Base‘𝑆) |
16 | 15, 1 | ghmf1o 17513 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 GrpHom 𝑆))) |
17 | 14, 16 | syl 17 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 GrpHom 𝑆))) |
18 | 17 | biimpa 500 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → ◡𝐹 ∈ (𝑇 GrpHom 𝑆)) |
19 | | simpll 786 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
20 | 13 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) →
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑇))) |
21 | 20 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑎 ∈ (Base‘(Scalar‘𝑆)) ↔ 𝑎 ∈ (Base‘(Scalar‘𝑇)))) |
22 | 21 | biimpar 501 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑇))) → 𝑎 ∈ (Base‘(Scalar‘𝑆))) |
23 | 22 | adantrr 749 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → 𝑎 ∈ (Base‘(Scalar‘𝑆))) |
24 | | f1ocnv 6062 |
. . . . . . . . . 10
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌–1-1-onto→𝑋) |
25 | | f1of 6050 |
. . . . . . . . . 10
⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → ◡𝐹:𝑌⟶𝑋) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌⟶𝑋) |
27 | 26 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → ◡𝐹:𝑌⟶𝑋) |
28 | 27 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑏 ∈ 𝑌) → (◡𝐹‘𝑏) ∈ 𝑋) |
29 | 28 | adantrl 748 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (◡𝐹‘𝑏) ∈ 𝑋) |
30 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆)) |
31 | 5, 30, 15, 3, 2 | lmhmlin 18856 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ (◡𝐹‘𝑏) ∈ 𝑋) → (𝐹‘(𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠
‘𝑇)(𝐹‘(◡𝐹‘𝑏)))) |
32 | 19, 23, 29, 31 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝐹‘(𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠
‘𝑇)(𝐹‘(◡𝐹‘𝑏)))) |
33 | | f1ocnvfv2 6433 |
. . . . . . 7
⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑏 ∈ 𝑌) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏) |
34 | 33 | ad2ant2l 778 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏) |
35 | 34 | oveq2d 6565 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝑎( ·𝑠
‘𝑇)(𝐹‘(◡𝐹‘𝑏))) = (𝑎( ·𝑠
‘𝑇)𝑏)) |
36 | 32, 35 | eqtrd 2644 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝐹‘(𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠
‘𝑇)𝑏)) |
37 | | simplr 788 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → 𝐹:𝑋–1-1-onto→𝑌) |
38 | 10 | adantr 480 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → 𝑆 ∈ LMod) |
39 | 15, 5, 3, 30 | lmodvscl 18703 |
. . . . . 6
⊢ ((𝑆 ∈ LMod ∧ 𝑎 ∈
(Base‘(Scalar‘𝑆)) ∧ (◡𝐹‘𝑏) ∈ 𝑋) → (𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏)) ∈ 𝑋) |
40 | 38, 23, 29, 39 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏)) ∈ 𝑋) |
41 | | f1ocnvfv 6434 |
. . . . 5
⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ (𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏)) ∈ 𝑋) → ((𝐹‘(𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠
‘𝑇)𝑏) → (◡𝐹‘(𝑎( ·𝑠
‘𝑇)𝑏)) = (𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏)))) |
42 | 37, 40, 41 | syl2anc 691 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → ((𝐹‘(𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠
‘𝑇)𝑏) → (◡𝐹‘(𝑎( ·𝑠
‘𝑇)𝑏)) = (𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏)))) |
43 | 36, 42 | mpd 15 |
. . 3
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (◡𝐹‘(𝑎( ·𝑠
‘𝑇)𝑏)) = (𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏))) |
44 | 1, 2, 3, 4, 5, 6, 8, 10, 13, 18, 43 | islmhmd 18860 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → ◡𝐹 ∈ (𝑇 LMHom 𝑆)) |
45 | 15, 1 | lmhmf 18855 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝑋⟶𝑌) |
46 | | ffn 5958 |
. . . . 5
⊢ (𝐹:𝑋⟶𝑌 → 𝐹 Fn 𝑋) |
47 | 45, 46 | syl 17 |
. . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 Fn 𝑋) |
48 | 47 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ ◡𝐹 ∈ (𝑇 LMHom 𝑆)) → 𝐹 Fn 𝑋) |
49 | 1, 15 | lmhmf 18855 |
. . . . 5
⊢ (◡𝐹 ∈ (𝑇 LMHom 𝑆) → ◡𝐹:𝑌⟶𝑋) |
50 | 49 | adantl 481 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ ◡𝐹 ∈ (𝑇 LMHom 𝑆)) → ◡𝐹:𝑌⟶𝑋) |
51 | | ffn 5958 |
. . . 4
⊢ (◡𝐹:𝑌⟶𝑋 → ◡𝐹 Fn 𝑌) |
52 | 50, 51 | syl 17 |
. . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ ◡𝐹 ∈ (𝑇 LMHom 𝑆)) → ◡𝐹 Fn 𝑌) |
53 | | dff1o4 6058 |
. . 3
⊢ (𝐹:𝑋–1-1-onto→𝑌 ↔ (𝐹 Fn 𝑋 ∧ ◡𝐹 Fn 𝑌)) |
54 | 48, 52, 53 | sylanbrc 695 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ ◡𝐹 ∈ (𝑇 LMHom 𝑆)) → 𝐹:𝑋–1-1-onto→𝑌) |
55 | 44, 54 | impbida 873 |
1
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 LMHom 𝑆))) |