| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lmhmf1o.y | . . 3
⊢ 𝑌 = (Base‘𝑇) | 
| 2 |  | eqid 2737 | . . 3
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) | 
| 3 |  | eqid 2737 | . . 3
⊢ (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆) | 
| 4 |  | eqid 2737 | . . 3
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) | 
| 5 |  | eqid 2737 | . . 3
⊢
(Scalar‘𝑆) =
(Scalar‘𝑆) | 
| 6 |  | eqid 2737 | . . 3
⊢
(Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇)) | 
| 7 |  | lmhmlmod2 21031 | . . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) | 
| 8 | 7 | adantr 480 | . . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → 𝑇 ∈ LMod) | 
| 9 |  | lmhmlmod1 21032 | . . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) | 
| 10 | 9 | adantr 480 | . . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → 𝑆 ∈ LMod) | 
| 11 | 5, 4 | lmhmsca 21029 | . . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑇) = (Scalar‘𝑆)) | 
| 12 | 11 | eqcomd 2743 | . . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑆) = (Scalar‘𝑇)) | 
| 13 | 12 | adantr 480 | . . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → (Scalar‘𝑆) = (Scalar‘𝑇)) | 
| 14 |  | lmghm 21030 | . . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | 
| 15 |  | lmhmf1o.x | . . . . . 6
⊢ 𝑋 = (Base‘𝑆) | 
| 16 | 15, 1 | ghmf1o 19266 | . . . . 5
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 GrpHom 𝑆))) | 
| 17 | 14, 16 | syl 17 | . . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 GrpHom 𝑆))) | 
| 18 | 17 | biimpa 476 | . . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → ◡𝐹 ∈ (𝑇 GrpHom 𝑆)) | 
| 19 |  | simpll 767 | . . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → 𝐹 ∈ (𝑆 LMHom 𝑇)) | 
| 20 | 13 | fveq2d 6910 | . . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) →
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑇))) | 
| 21 | 20 | eleq2d 2827 | . . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑎 ∈ (Base‘(Scalar‘𝑆)) ↔ 𝑎 ∈ (Base‘(Scalar‘𝑇)))) | 
| 22 | 21 | biimpar 477 | . . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑇))) → 𝑎 ∈ (Base‘(Scalar‘𝑆))) | 
| 23 | 22 | adantrr 717 | . . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → 𝑎 ∈ (Base‘(Scalar‘𝑆))) | 
| 24 |  | f1ocnv 6860 | . . . . . . . . . 10
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌–1-1-onto→𝑋) | 
| 25 |  | f1of 6848 | . . . . . . . . . 10
⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → ◡𝐹:𝑌⟶𝑋) | 
| 26 | 24, 25 | syl 17 | . . . . . . . . 9
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌⟶𝑋) | 
| 27 | 26 | adantl 481 | . . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → ◡𝐹:𝑌⟶𝑋) | 
| 28 | 27 | ffvelcdmda 7104 | . . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑏 ∈ 𝑌) → (◡𝐹‘𝑏) ∈ 𝑋) | 
| 29 | 28 | adantrl 716 | . . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (◡𝐹‘𝑏) ∈ 𝑋) | 
| 30 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆)) | 
| 31 | 5, 30, 15, 3, 2 | lmhmlin 21034 | . . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ (◡𝐹‘𝑏) ∈ 𝑋) → (𝐹‘(𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠
‘𝑇)(𝐹‘(◡𝐹‘𝑏)))) | 
| 32 | 19, 23, 29, 31 | syl3anc 1373 | . . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝐹‘(𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠
‘𝑇)(𝐹‘(◡𝐹‘𝑏)))) | 
| 33 |  | f1ocnvfv2 7297 | . . . . . . 7
⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑏 ∈ 𝑌) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏) | 
| 34 | 33 | ad2ant2l 746 | . . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏) | 
| 35 | 34 | oveq2d 7447 | . . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝑎( ·𝑠
‘𝑇)(𝐹‘(◡𝐹‘𝑏))) = (𝑎( ·𝑠
‘𝑇)𝑏)) | 
| 36 | 32, 35 | eqtrd 2777 | . . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝐹‘(𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠
‘𝑇)𝑏)) | 
| 37 |  | simplr 769 | . . . . 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 20876 | . . . . . 6
⊢ ((𝑆 ∈ LMod ∧ 𝑎 ∈
(Base‘(Scalar‘𝑆)) ∧ (◡𝐹‘𝑏) ∈ 𝑋) → (𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏)) ∈ 𝑋) | 
| 40 | 38, 23, 29, 39 | syl3anc 1373 | . . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏)) ∈ 𝑋) | 
| 41 |  | f1ocnvfv 7298 | . . . . 5
⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ (𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏)) ∈ 𝑋) → ((𝐹‘(𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠
‘𝑇)𝑏) → (◡𝐹‘(𝑎( ·𝑠
‘𝑇)𝑏)) = (𝑎( ·𝑠
‘𝑆)(◡𝐹‘𝑏)))) | 
| 42 | 37, 40, 41 | syl2anc 584 | . . . 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 21038 | . 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → ◡𝐹 ∈ (𝑇 LMHom 𝑆)) | 
| 45 | 15, 1 | lmhmf 21033 | . . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝑋⟶𝑌) | 
| 46 | 45 | ffnd 6737 | . . . 4
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 Fn 𝑋) | 
| 47 | 46 | adantr 480 | . . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ ◡𝐹 ∈ (𝑇 LMHom 𝑆)) → 𝐹 Fn 𝑋) | 
| 48 | 1, 15 | lmhmf 21033 | . . . . 5
⊢ (◡𝐹 ∈ (𝑇 LMHom 𝑆) → ◡𝐹:𝑌⟶𝑋) | 
| 49 | 48 | adantl 481 | . . . 4
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ ◡𝐹 ∈ (𝑇 LMHom 𝑆)) → ◡𝐹:𝑌⟶𝑋) | 
| 50 | 49 | ffnd 6737 | . . 3
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ ◡𝐹 ∈ (𝑇 LMHom 𝑆)) → ◡𝐹 Fn 𝑌) | 
| 51 |  | dff1o4 6856 | . . 3
⊢ (𝐹:𝑋–1-1-onto→𝑌 ↔ (𝐹 Fn 𝑋 ∧ ◡𝐹 Fn 𝑌)) | 
| 52 | 47, 50, 51 | sylanbrc 583 | . 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ ◡𝐹 ∈ (𝑇 LMHom 𝑆)) → 𝐹:𝑋–1-1-onto→𝑌) | 
| 53 | 44, 52 | impbida 801 | 1
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 LMHom 𝑆))) |