Theorem lmhmlem

Description: Non-quantified consequences of a left module homomorphism. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Hypotheses	lmhmlem.k	⊢ 𝐾 = ( Scalar ‘ 𝑆 )
	lmhmlem.l	⊢ 𝐿 = ( Scalar ‘ 𝑇 )
Assertion	lmhmlem	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmhmlem.k	⊢ 𝐾 = ( Scalar ‘ 𝑆 )
2		lmhmlem.l	⊢ 𝐿 = ( Scalar ‘ 𝑇 )
3		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
4		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
5		eqid	⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
6		eqid	⊢ ( ·𝑠 ‘ 𝑇 ) = ( ·𝑠 ‘ 𝑇 )
7	1 2 3 4 5 6	islmhm	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ↔ ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ∀ 𝑏 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) ) ) )
8		3simpa	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ∀ 𝑏 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ) )
9	8	anim2i	⊢ ( ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ∀ 𝑏 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) ) ) → ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ) ) )
10	7 9	sylbi	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐿 = 𝐾 ) ) )