Metamath Proof Explorer

Theorem lmhmlem

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

Ref Expression
Hypotheses lmhmlem.k ⊢ K = Scalar ⁡ S
lmhmlem.l ⊢ L = Scalar ⁡ T
Assertion lmhmlem ⊢ F ∈ S LMHom T → S ∈ LMod ∧ T ∈ LMod ∧ F ∈ S GrpHom T ∧ L = K

Proof

Step Hyp Ref Expression
1 lmhmlem.k ⊢ K = Scalar ⁡ S
2 lmhmlem.l ⊢ L = Scalar ⁡ T
3 eqid ⊢ Base K = Base K
4 eqid ⊢ Base S = Base S
5 eqid ⊢ ⋅ S = ⋅ S
6 eqid ⊢ ⋅ T = ⋅ T
7 1 2 3 4 5 6 islmhm ⊢ F ∈ S LMHom T ↔ S ∈ LMod ∧ T ∈ LMod ∧ F ∈ S GrpHom T ∧ L = K ∧ ∀ a ∈ Base K ∀ b ∈ Base S F ⁡ a ⋅ S b = a ⋅ T F ⁡ b
8 3simpa ⊢ F ∈ S GrpHom T ∧ L = K ∧ ∀ a ∈ Base K ∀ b ∈ Base S F ⁡ a ⋅ S b = a ⋅ T F ⁡ b → F ∈ S GrpHom T ∧ L = K
9 8 anim2i ⊢ S ∈ LMod ∧ T ∈ LMod ∧ F ∈ S GrpHom T ∧ L = K ∧ ∀ a ∈ Base K ∀ b ∈ Base S F ⁡ a ⋅ S b = a ⋅ T F ⁡ b → S ∈ LMod ∧ T ∈ LMod ∧ F ∈ S GrpHom T ∧ L = K
10 7 9 sylbi ⊢ F ∈ S LMHom T → S ∈ LMod ∧ T ∈ LMod ∧ F ∈ S GrpHom T ∧ L = K