Theorem lmhmf1o 19812

Description: A bijective module homomorphism is also converse homomorphic. (Contributed by Stefan O'Rear, 25-Jan-2015.)

Hypotheses

Ref	Expression
lmhmf1o.x	⊢ 𝑋 = (Base‘𝑆)
lmhmf1o.y	⊢ 𝑌 = (Base‘𝑇)

Assertion

Ref	Expression
lmhmf1o	⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 LMHom 𝑆)))

Proof of Theorem lmhmf1o

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lmhmf1o.y	. . 3 ⊢ 𝑌 = (Base‘𝑇)
2		eqid 2821	. . 3 ⊢ ( ·𝑠 ‘𝑇) = ( ·𝑠 ‘𝑇)
3		eqid 2821	. . 3 ⊢ ( ·𝑠 ‘𝑆) = ( ·𝑠 ‘𝑆)
4		eqid 2821	. . 3 ⊢ (Scalar‘𝑇) = (Scalar‘𝑇)
5		eqid 2821	. . 3 ⊢ (Scalar‘𝑆) = (Scalar‘𝑆)
6		eqid 2821	. . 3 ⊢ (Base‘(Scalar‘𝑇)) = (Base‘(Scalar‘𝑇))
7		lmhmlmod2 19798	. . . 4 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod)
8	7	adantr 483	. . 3 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → 𝑇 ∈ LMod)
9		lmhmlmod1 19799	. . . 4 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod)
10	9	adantr 483	. . 3 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → 𝑆 ∈ LMod)
11	5, 4	lmhmsca 19796	. . . . 5 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑇) = (Scalar‘𝑆))
12	11	eqcomd 2827	. . . 4 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (Scalar‘𝑆) = (Scalar‘𝑇))
13	12	adantr 483	. . 3 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → (Scalar‘𝑆) = (Scalar‘𝑇))
14		lmghm 19797	. . . . 5 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
15		lmhmf1o.x	. . . . . 6 ⊢ 𝑋 = (Base‘𝑆)
16	15, 1	ghmf1o 18382	. . . . 5 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 GrpHom 𝑆)))
17	14, 16	syl 17	. . . 4 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 GrpHom 𝑆)))
18	17	biimpa 479	. . 3 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → ◡𝐹 ∈ (𝑇 GrpHom 𝑆))
19		simpll 765	. . . . . 6 ⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → 𝐹 ∈ (𝑆 LMHom 𝑇))
20	13	fveq2d 6668	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → (Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑇)))
21	20	eleq2d 2898	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑎 ∈ (Base‘(Scalar‘𝑆)) ↔ 𝑎 ∈ (Base‘(Scalar‘𝑇))))
22	21	biimpar 480	. . . . . . 7 ⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑇))) → 𝑎 ∈ (Base‘(Scalar‘𝑆)))
23	22	adantrr 715	. . . . . 6 ⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → 𝑎 ∈ (Base‘(Scalar‘𝑆)))
24		f1ocnv 6621	. . . . . . . . . 10 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌–1-1-onto→𝑋)
25		f1of 6609	. . . . . . . . . 10 ⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → ◡𝐹:𝑌⟶𝑋)
26	24, 25	syl 17	. . . . . . . . 9 ⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌⟶𝑋)
27	26	adantl 484	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → ◡𝐹:𝑌⟶𝑋)
28	27	ffvelrnda 6845	. . . . . . 7 ⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑏 ∈ 𝑌) → (◡𝐹‘𝑏) ∈ 𝑋)
29	28	adantrl 714	. . . . . 6 ⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (◡𝐹‘𝑏) ∈ 𝑋)
30		eqid 2821	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆))
31	5, 30, 15, 3, 2	lmhmlin 19801	. . . . . 6 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ (◡𝐹‘𝑏) ∈ 𝑋) → (𝐹‘(𝑎( ·𝑠 ‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠 ‘𝑇)(𝐹‘(◡𝐹‘𝑏))))
32	19, 23, 29, 31	syl3anc 1367	. . . . 5 ⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝐹‘(𝑎( ·𝑠 ‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠 ‘𝑇)(𝐹‘(◡𝐹‘𝑏))))
33		f1ocnvfv2 7028	. . . . . . 7 ⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑏 ∈ 𝑌) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
34	33	ad2ant2l 744	. . . . . 6 ⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
35	34	oveq2d 7166	. . . . 5 ⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝑎( ·𝑠 ‘𝑇)(𝐹‘(◡𝐹‘𝑏))) = (𝑎( ·𝑠 ‘𝑇)𝑏))
36	32, 35	eqtrd 2856	. . . 4 ⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝐹‘(𝑎( ·𝑠 ‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠 ‘𝑇)𝑏))
37		simplr 767	. . . . 5 ⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → 𝐹:𝑋–1-1-onto→𝑌)
38	10	adantr 483	. . . . . 6 ⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → 𝑆 ∈ LMod)
39	15, 5, 3, 30	lmodvscl 19645	. . . . . 6 ⊢ ((𝑆 ∈ LMod ∧ 𝑎 ∈ (Base‘(Scalar‘𝑆)) ∧ (◡𝐹‘𝑏) ∈ 𝑋) → (𝑎( ·𝑠 ‘𝑆)(◡𝐹‘𝑏)) ∈ 𝑋)
40	38, 23, 29, 39	syl3anc 1367	. . . . 5 ⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ (𝑎 ∈ (Base‘(Scalar‘𝑇)) ∧ 𝑏 ∈ 𝑌)) → (𝑎( ·𝑠 ‘𝑆)(◡𝐹‘𝑏)) ∈ 𝑋)
41		f1ocnvfv 7029	. . . . 5 ⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ (𝑎( ·𝑠 ‘𝑆)(◡𝐹‘𝑏)) ∈ 𝑋) → ((𝐹‘(𝑎( ·𝑠 ‘𝑆)(◡𝐹‘𝑏))) = (𝑎( ·𝑠 ‘𝑇)𝑏) → (◡𝐹‘(𝑎( ·𝑠 ‘𝑇)𝑏)) = (𝑎( ·𝑠 ‘𝑆)(◡𝐹‘𝑏))))
42	37, 40, 41	syl2anc 586	. . . 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 19805	. 2 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹:𝑋–1-1-onto→𝑌) → ◡𝐹 ∈ (𝑇 LMHom 𝑆))
45	15, 1	lmhmf 19800	. . . . 5 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝑋⟶𝑌)
46	45	ffnd 6509	. . . 4 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 Fn 𝑋)
47	46	adantr 483	. . 3 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ ◡𝐹 ∈ (𝑇 LMHom 𝑆)) → 𝐹 Fn 𝑋)
48	1, 15	lmhmf 19800	. . . . 5 ⊢ (◡𝐹 ∈ (𝑇 LMHom 𝑆) → ◡𝐹:𝑌⟶𝑋)
49	48	adantl 484	. . . 4 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ ◡𝐹 ∈ (𝑇 LMHom 𝑆)) → ◡𝐹:𝑌⟶𝑋)
50	49	ffnd 6509	. . 3 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ ◡𝐹 ∈ (𝑇 LMHom 𝑆)) → ◡𝐹 Fn 𝑌)
51		dff1o4 6617	. . 3 ⊢ (𝐹:𝑋–1-1-onto→𝑌 ↔ (𝐹 Fn 𝑋 ∧ ◡𝐹 Fn 𝑌))
52	47, 50, 51	sylanbrc 585	. 2 ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ ◡𝐹 ∈ (𝑇 LMHom 𝑆)) → 𝐹:𝑋–1-1-onto→𝑌)
53	44, 52	impbida 799	1 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 LMHom 𝑆)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ^◡ccnv 5548   Fn wfn 6344  ⟶wf 6345  –1-1-onto→wf1o 6348  ‘cfv 6349  (class class class)co 7150  Basecbs 16477  Scalarcsca 16562   ·_𝑠 cvsca 16563   GrpHom cghm 18349  LModclmod 19628   LMHom clmhm 19785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-oprab 7154  df-mpo 7155  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-grp 18100  df-ghm 18350  df-lmod 19630  df-lmhm 19788

This theorem is referenced by:  islmim2  19832