lmhmf1o

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

	Ref	Expression
Hypotheses	lmhmf1o.x	$⊢ X = {Base}_{S}$
	lmhmf1o.y	$⊢ Y = {Base}_{T}$
Assertion	lmhmf1o	$⊢ F \in (S LMHom T) \to (F : X \underset{1-1 onto}{⟶} Y \leftrightarrow F^{-1} \in (T LMHom S))$

Proof

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

Metamath Proof Explorer

Theorem lmhmf1o

Proof