This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑇 ) ) ) )