Metamath Proof Explorer

Theorem isnmhm

Description: A normed module homomorphism is a left module homomorphism which is also a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015)

		Ref	Expression
	Assertion	isnmhm	$⊢ F \in (S NMHom T) \leftrightarrow ((S \in NrmMod \land T \in NrmMod) \land (F \in (S LMHom T) \land F \in (S NGHom T)))$

Proof

Step	Hyp	Ref	Expression
1		df-nmhm	$⊢ NMHom = (s \in NrmMod, t \in NrmMod ⟼ (s LMHom t) \cap (s NGHom t))$
2	1	elmpocl	$⊢ F \in (S NMHom T) \to (S \in NrmMod \land T \in NrmMod)$
3		oveq12	$⊢ (s = S \land t = T) \to s LMHom t = S LMHom T$
4		oveq12	$⊢ (s = S \land t = T) \to s NGHom t = S NGHom T$
5	3 4	ineq12d	$⊢ (s = S \land t = T) \to (s LMHom t) \cap (s NGHom t) = (S LMHom T) \cap (S NGHom T)$
6		ovex	$⊢ S LMHom T \in V$
7	6	inex1	$⊢ (S LMHom T) \cap (S NGHom T) \in V$
8	5 1 7	ovmpoa	$⊢ (S \in NrmMod \land T \in NrmMod) \to S NMHom T = (S LMHom T) \cap (S NGHom T)$
9	8	eleq2d	$⊢ (S \in NrmMod \land T \in NrmMod) \to (F \in (S NMHom T) \leftrightarrow F \in ((S LMHom T) \cap (S NGHom T)))$
10		elin	$⊢ F \in ((S LMHom T) \cap (S NGHom T)) \leftrightarrow (F \in (S LMHom T) \land F \in (S NGHom T))$
11	9 10	bitrdi	$⊢ (S \in NrmMod \land T \in NrmMod) \to (F \in (S NMHom T) \leftrightarrow (F \in (S LMHom T) \land F \in (S NGHom T)))$
12	2 11	biadanii	$⊢ F \in (S NMHom T) \leftrightarrow ((S \in NrmMod \land T \in NrmMod) \land (F \in (S LMHom T) \land F \in (S NGHom T)))$