islmim

Description: An isomorphism of left modules is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015)

	Ref	Expression
Hypotheses	islmim.b	$⊢ B = {Base}_{R}$
	islmim.c	$⊢ C = {Base}_{S}$
Assertion	islmim	$⊢ F \in (R LMIso S) \leftrightarrow (F \in (R LMHom S) \land F : B \underset{1-1 onto}{⟶} C)$

Proof

Step	Hyp	Ref	Expression
1		islmim.b	$⊢ B = {Base}_{R}$
2		islmim.c	$⊢ C = {Base}_{S}$
3		df-lmim	$⊢ LMIso = (a \in LMod, b \in LMod ⟼ \{c \in (a LMHom b) \| c : {Base}_{a} \underset{1-1 onto}{⟶} {Base}_{b}\})$
4		ovex	$⊢ a LMHom b \in V$
5	4	rabex	$⊢ \{c \in (a LMHom b) \| c : {Base}_{a} \underset{1-1 onto}{⟶} {Base}_{b}\} \in V$
6		oveq12	$⊢ (a = R \land b = S) \to a LMHom b = R LMHom S$
7		fveq2	$⊢ a = R \to {Base}_{a} = {Base}_{R}$
8	7 1	eqtr4di	$⊢ a = R \to {Base}_{a} = B$
9		fveq2	$⊢ b = S \to {Base}_{b} = {Base}_{S}$
10	9 2	eqtr4di	$⊢ b = S \to {Base}_{b} = C$
11		f1oeq23	$⊢ ({Base}_{a} = B \land {Base}_{b} = C) \to (c : {Base}_{a} \underset{1-1 onto}{⟶} {Base}_{b} \leftrightarrow c : B \underset{1-1 onto}{⟶} C)$
12	8 10 11	syl2an	$⊢ (a = R \land b = S) \to (c : {Base}_{a} \underset{1-1 onto}{⟶} {Base}_{b} \leftrightarrow c : B \underset{1-1 onto}{⟶} C)$
13	6 12	rabeqbidv	$⊢ (a = R \land b = S) \to \{c \in (a LMHom b) \| c : {Base}_{a} \underset{1-1 onto}{⟶} {Base}_{b}\} = \{c \in (R LMHom S) \| c : B \underset{1-1 onto}{⟶} C\}$
14	3 5 13	elovmpo	$⊢ F \in (R LMIso S) \leftrightarrow (R \in LMod \land S \in LMod \land F \in \{c \in (R LMHom S) \| c : B \underset{1-1 onto}{⟶} C\})$
15		df-3an	$⊢ (R \in LMod \land S \in LMod \land F \in \{c \in (R LMHom S) \| c : B \underset{1-1 onto}{⟶} C\}) \leftrightarrow ((R \in LMod \land S \in LMod) \land F \in \{c \in (R LMHom S) \| c : B \underset{1-1 onto}{⟶} C\})$
16		f1oeq1	$⊢ c = F \to (c : B \underset{1-1 onto}{⟶} C \leftrightarrow F : B \underset{1-1 onto}{⟶} C)$
17	16	elrab	$⊢ F \in \{c \in (R LMHom S) \| c : B \underset{1-1 onto}{⟶} C\} \leftrightarrow (F \in (R LMHom S) \land F : B \underset{1-1 onto}{⟶} C)$
18	17	anbi2i	$⊢ ((R \in LMod \land S \in LMod) \land F \in \{c \in (R LMHom S) \| c : B \underset{1-1 onto}{⟶} C\}) \leftrightarrow ((R \in LMod \land S \in LMod) \land (F \in (R LMHom S) \land F : B \underset{1-1 onto}{⟶} C))$
19		lmhmlmod1	$⊢ F \in (R LMHom S) \to R \in LMod$
20		lmhmlmod2	$⊢ F \in (R LMHom S) \to S \in LMod$
21	19 20	jca	$⊢ F \in (R LMHom S) \to (R \in LMod \land S \in LMod)$
22	21	adantr	$⊢ (F \in (R LMHom S) \land F : B \underset{1-1 onto}{⟶} C) \to (R \in LMod \land S \in LMod)$
23	22	pm4.71ri	$⊢ (F \in (R LMHom S) \land F : B \underset{1-1 onto}{⟶} C) \leftrightarrow ((R \in LMod \land S \in LMod) \land (F \in (R LMHom S) \land F : B \underset{1-1 onto}{⟶} C))$
24	18 23	bitr4i	$⊢ ((R \in LMod \land S \in LMod) \land F \in \{c \in (R LMHom S) \| c : B \underset{1-1 onto}{⟶} C\}) \leftrightarrow (F \in (R LMHom S) \land F : B \underset{1-1 onto}{⟶} C)$
25	14 15 24	3bitri	$⊢ F \in (R LMIso S) \leftrightarrow (F \in (R LMHom S) \land F : B \underset{1-1 onto}{⟶} C)$

Metamath Proof Explorer

Theorem islmim

Proof