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 ( 𝐹 ∈ ( 𝑆 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 𝑇 ) ) ) )