islmhmd

Description: Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015)

	Ref	Expression
Hypotheses	islmhmd.x	$⊢ X = {Base}_{S}$
	islmhmd.a	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	islmhmd.b	$⊢ \underset{˙}{\times} = \cdot_{T}$
	islmhmd.k	$⊢ K = Scalar (S)$
	islmhmd.j	$⊢ J = Scalar (T)$
	islmhmd.n	$⊢ N = {Base}_{K}$
	islmhmd.s	$⊢ φ \to S \in LMod$
	islmhmd.t	$⊢ φ \to T \in LMod$
	islmhmd.c	$⊢ φ \to J = K$
	islmhmd.f	$⊢ φ \to F \in (S GrpHom T)$
	islmhmd.l	$⊢ (φ \land (x \in N \land y \in X)) \to F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)$
Assertion	islmhmd	$⊢ φ \to F \in (S LMHom T)$

Step	Hyp	Ref	Expression
1		islmhmd.x	$⊢ X = {Base}_{S}$
2		islmhmd.a	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
3		islmhmd.b	$⊢ \underset{˙}{\times} = \cdot_{T}$
4		islmhmd.k	$⊢ K = Scalar (S)$
5		islmhmd.j	$⊢ J = Scalar (T)$
6		islmhmd.n	$⊢ N = {Base}_{K}$
7		islmhmd.s	$⊢ φ \to S \in LMod$
8		islmhmd.t	$⊢ φ \to T \in LMod$
9		islmhmd.c	$⊢ φ \to J = K$
10		islmhmd.f	$⊢ φ \to F \in (S GrpHom T)$
11		islmhmd.l	$⊢ (φ \land (x \in N \land y \in X)) \to F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)$
12	11	ralrimivva	$⊢ φ \to \forall x \in N \forall y \in X F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)$
13	10 9 12	3jca	$⊢ φ \to (F \in (S GrpHom T) \land J = K \land \forall x \in N \forall y \in X F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y))$
14	4 5 6 1 2 3	islmhm	$⊢ F \in (S LMHom T) \leftrightarrow ((S \in LMod \land T \in LMod) \land (F \in (S GrpHom T) \land J = K \land \forall x \in N \forall y \in X F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))$
15	7 8 13 14	syl21anbrc	$⊢ φ \to F \in (S LMHom T)$

Metamath Proof Explorer