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	⊢ ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) ↔ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) ∧ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-nmhm	⊢ NMHom = ( 𝑠 ∈ NrmMod , 𝑡 ∈ NrmMod ↦ ( ( 𝑠 LMHom 𝑡 ) ∩ ( 𝑠 NGHom 𝑡 ) ) )
2	1	elmpocl	⊢ ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) → ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) )
3		oveq12	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑠 LMHom 𝑡 ) = ( 𝑆 LMHom 𝑇 ) )
4		oveq12	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑠 NGHom 𝑡 ) = ( 𝑆 NGHom 𝑇 ) )
5	3 4	ineq12d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( 𝑠 LMHom 𝑡 ) ∩ ( 𝑠 NGHom 𝑡 ) ) = ( ( 𝑆 LMHom 𝑇 ) ∩ ( 𝑆 NGHom 𝑇 ) ) )
6		ovex	⊢ ( 𝑆 LMHom 𝑇 ) ∈ V
7	6	inex1	⊢ ( ( 𝑆 LMHom 𝑇 ) ∩ ( 𝑆 NGHom 𝑇 ) ) ∈ V
8	5 1 7	ovmpoa	⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) → ( 𝑆 NMHom 𝑇 ) = ( ( 𝑆 LMHom 𝑇 ) ∩ ( 𝑆 NGHom 𝑇 ) ) )
9	8	eleq2d	⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) → ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) ↔ 𝐹 ∈ ( ( 𝑆 LMHom 𝑇 ) ∩ ( 𝑆 NGHom 𝑇 ) ) ) )
10		elin	⊢ ( 𝐹 ∈ ( ( 𝑆 LMHom 𝑇 ) ∩ ( 𝑆 NGHom 𝑇 ) ) ↔ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ) )
11	9 10	bitrdi	⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) → ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) ↔ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ) ) )
12	2 11	biadanii	⊢ ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) ↔ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) ∧ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ) ) )