islmhm2

Description: A one-equation proof of linearity of a left module homomorphism, similar to df-lss . (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	islmhm2.b	$⊢ B = {Base}_{S}$
	islmhm2.c	$⊢ C = {Base}_{T}$
	islmhm2.k	$⊢ K = Scalar (S)$
	islmhm2.l	$⊢ L = Scalar (T)$
	islmhm2.e	$⊢ E = {Base}_{K}$
	islmhm2.p	$⊢ \underset{˙}{+} = +_{S}$
	islmhm2.q	$⊢ \underset{˙}{⨣} = +_{T}$
	islmhm2.m	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	islmhm2.n	$⊢ \underset{˙}{\times} = \cdot_{T}$
Assertion	islmhm2	$⊢ (S \in LMod \land T \in LMod) \to (F \in (S LMHom T) \leftrightarrow (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z)))$

Proof

Step	Hyp	Ref	Expression
1		islmhm2.b	$⊢ B = {Base}_{S}$
2		islmhm2.c	$⊢ C = {Base}_{T}$
3		islmhm2.k	$⊢ K = Scalar (S)$
4		islmhm2.l	$⊢ L = Scalar (T)$
5		islmhm2.e	$⊢ E = {Base}_{K}$
6		islmhm2.p	$⊢ \underset{˙}{+} = +_{S}$
7		islmhm2.q	$⊢ \underset{˙}{⨣} = +_{T}$
8		islmhm2.m	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
9		islmhm2.n	$⊢ \underset{˙}{\times} = \cdot_{T}$
10	1 2	lmhmf	$⊢ F \in (S LMHom T) \to F : B ⟶ C$
11	3 4	lmhmsca	$⊢ F \in (S LMHom T) \to L = K$
12		lmghm	$⊢ F \in (S LMHom T) \to F \in (S GrpHom T)$
13	12	adantr	$⊢ (F \in (S LMHom T) \land (x \in E \land y \in B \land z \in B)) \to F \in (S GrpHom T)$
14		lmhmlmod1	$⊢ F \in (S LMHom T) \to S \in LMod$
15	14	adantr	$⊢ (F \in (S LMHom T) \land (x \in E \land y \in B \land z \in B)) \to S \in LMod$
16		simpr1	$⊢ (F \in (S LMHom T) \land (x \in E \land y \in B \land z \in B)) \to x \in E$
17		simpr2	$⊢ (F \in (S LMHom T) \land (x \in E \land y \in B \land z \in B)) \to y \in B$
18	1 3 8 5	lmodvscl	$⊢ (S \in LMod \land x \in E \land y \in B) \to x \underset{˙}{\cdot} y \in B$
19	15 16 17 18	syl3anc	$⊢ (F \in (S LMHom T) \land (x \in E \land y \in B \land z \in B)) \to x \underset{˙}{\cdot} y \in B$
20		simpr3	$⊢ (F \in (S LMHom T) \land (x \in E \land y \in B \land z \in B)) \to z \in B$
21	1 6 7	ghmlin	$⊢ (F \in (S GrpHom T) \land x \underset{˙}{\cdot} y \in B \land z \in B) \to F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = F (x \underset{˙}{\cdot} y) \underset{˙}{⨣} F (z)$
22	13 19 20 21	syl3anc	$⊢ (F \in (S LMHom T) \land (x \in E \land y \in B \land z \in B)) \to F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = F (x \underset{˙}{\cdot} y) \underset{˙}{⨣} F (z)$
23	3 5 1 8 9	lmhmlin	$⊢ (F \in (S LMHom T) \land x \in E \land y \in B) \to F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)$
24	23	3adant3r3	$⊢ (F \in (S LMHom T) \land (x \in E \land y \in B \land z \in B)) \to F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)$
25	24	oveq1d	$⊢ (F \in (S LMHom T) \land (x \in E \land y \in B \land z \in B)) \to F (x \underset{˙}{\cdot} y) \underset{˙}{⨣} F (z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z)$
26	22 25	eqtrd	$⊢ (F \in (S LMHom T) \land (x \in E \land y \in B \land z \in B)) \to F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z)$
27	26	ralrimivvva	$⊢ F \in (S LMHom T) \to \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z)$
28	10 11 27	3jca	$⊢ F \in (S LMHom T) \to (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))$
29	28	adantl	$⊢ ((S \in LMod \land T \in LMod) \land F \in (S LMHom T)) \to (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))$
30		lmodgrp	$⊢ S \in LMod \to S \in Grp$
31		lmodgrp	$⊢ T \in LMod \to T \in Grp$
32	30 31	anim12i	$⊢ (S \in LMod \land T \in LMod) \to (S \in Grp \land T \in Grp)$
33	32	adantr	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))) \to (S \in Grp \land T \in Grp)$
34		simpr1	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))) \to F : B ⟶ C$
35	3	lmodring	$⊢ S \in LMod \to K \in Ring$
36	35	ad2antrr	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \to K \in Ring$
37		eqid	$⊢ 1_{K} = 1_{K}$
38	5 37	ringidcl	$⊢ K \in Ring \to 1_{K} \in E$
39		oveq1	$⊢ x = 1_{K} \to x \underset{˙}{\cdot} y = 1_{K} \underset{˙}{\cdot} y$
40	39	fvoveq1d	$⊢ x = 1_{K} \to F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = F ((1_{K} \underset{˙}{\cdot} y) \underset{˙}{+} z)$
41		oveq1	$⊢ x = 1_{K} \to x \underset{˙}{\times} F (y) = 1_{K} \underset{˙}{\times} F (y)$
42	41	oveq1d	$⊢ x = 1_{K} \to (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) = (1_{K} \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z)$
43	40 42	eqeq12d	$⊢ x = 1_{K} \to (F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \leftrightarrow F ((1_{K} \underset{˙}{\cdot} y) \underset{˙}{+} z) = (1_{K} \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))$
44	43	2ralbidv	$⊢ x = 1_{K} \to (\forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \leftrightarrow \forall y \in B \forall z \in B F ((1_{K} \underset{˙}{\cdot} y) \underset{˙}{+} z) = (1_{K} \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))$
45	44	rspcv	$⊢ 1_{K} \in E \to (\forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \to \forall y \in B \forall z \in B F ((1_{K} \underset{˙}{\cdot} y) \underset{˙}{+} z) = (1_{K} \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))$
46	36 38 45	3syl	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \to (\forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \to \forall y \in B \forall z \in B F ((1_{K} \underset{˙}{\cdot} y) \underset{˙}{+} z) = (1_{K} \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))$
47		simplll	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to S \in LMod$
48		simprl	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to y \in B$
49	1 3 8 37	lmodvs1	$⊢ (S \in LMod \land y \in B) \to 1_{K} \underset{˙}{\cdot} y = y$
50	47 48 49	syl2anc	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to 1_{K} \underset{˙}{\cdot} y = y$
51	50	fvoveq1d	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to F ((1_{K} \underset{˙}{\cdot} y) \underset{˙}{+} z) = F (y \underset{˙}{+} z)$
52		simplrr	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to L = K$
53	52	fveq2d	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to 1_{L} = 1_{K}$
54	53	oveq1d	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to 1_{L} \underset{˙}{\times} F (y) = 1_{K} \underset{˙}{\times} F (y)$
55		simpllr	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to T \in LMod$
56		simplrl	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to F : B ⟶ C$
57	56 48	ffvelcdmd	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to F (y) \in C$
58		eqid	$⊢ 1_{L} = 1_{L}$
59	2 4 9 58	lmodvs1	$⊢ (T \in LMod \land F (y) \in C) \to 1_{L} \underset{˙}{\times} F (y) = F (y)$
60	55 57 59	syl2anc	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to 1_{L} \underset{˙}{\times} F (y) = F (y)$
61	54 60	eqtr3d	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to 1_{K} \underset{˙}{\times} F (y) = F (y)$
62	61	oveq1d	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to (1_{K} \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) = F (y) \underset{˙}{⨣} F (z)$
63	51 62	eqeq12d	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \land (y \in B \land z \in B)) \to (F ((1_{K} \underset{˙}{\cdot} y) \underset{˙}{+} z) = (1_{K} \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \leftrightarrow F (y \underset{˙}{+} z) = F (y) \underset{˙}{⨣} F (z))$
64	63	2ralbidva	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \to (\forall y \in B \forall z \in B F ((1_{K} \underset{˙}{\cdot} y) \underset{˙}{+} z) = (1_{K} \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \leftrightarrow \forall y \in B \forall z \in B F (y \underset{˙}{+} z) = F (y) \underset{˙}{⨣} F (z))$
65	46 64	sylibd	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K)) \to (\forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \to \forall y \in B \forall z \in B F (y \underset{˙}{+} z) = F (y) \underset{˙}{⨣} F (z))$
66	65	exp32	$⊢ (S \in LMod \land T \in LMod) \to (F : B ⟶ C \to (L = K \to (\forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \to \forall y \in B \forall z \in B F (y \underset{˙}{+} z) = F (y) \underset{˙}{⨣} F (z))))$
67	66	3imp2	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))) \to \forall y \in B \forall z \in B F (y \underset{˙}{+} z) = F (y) \underset{˙}{⨣} F (z)$
68	34 67	jca	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))) \to (F : B ⟶ C \land \forall y \in B \forall z \in B F (y \underset{˙}{+} z) = F (y) \underset{˙}{⨣} F (z))$
69	1 2 6 7	isghm	$⊢ F \in (S GrpHom T) \leftrightarrow ((S \in Grp \land T \in Grp) \land (F : B ⟶ C \land \forall y \in B \forall z \in B F (y \underset{˙}{+} z) = F (y) \underset{˙}{⨣} F (z)))$
70	33 68 69	sylanbrc	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))) \to F \in (S GrpHom T)$
71		simpr2	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))) \to L = K$
72		eqid	$⊢ 0_{S} = 0_{S}$
73		eqid	$⊢ 0_{T} = 0_{T}$
74	72 73	ghmid	$⊢ F \in (S GrpHom T) \to F (0_{S}) = 0_{T}$
75	70 74	syl	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))) \to F (0_{S}) = 0_{T}$
76	30	ad3antrrr	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to S \in Grp$
77	1 72	grpidcl	$⊢ S \in Grp \to 0_{S} \in B$
78		oveq2	$⊢ z = 0_{S} \to (x \underset{˙}{\cdot} y) \underset{˙}{+} z = (x \underset{˙}{\cdot} y) \underset{˙}{+} 0_{S}$
79	78	fveq2d	$⊢ z = 0_{S} \to F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = F ((x \underset{˙}{\cdot} y) \underset{˙}{+} 0_{S})$
80		fveq2	$⊢ z = 0_{S} \to F (z) = F (0_{S})$
81	80	oveq2d	$⊢ z = 0_{S} \to (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (0_{S})$
82	79 81	eqeq12d	$⊢ z = 0_{S} \to (F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \leftrightarrow F ((x \underset{˙}{\cdot} y) \underset{˙}{+} 0_{S}) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (0_{S}))$
83	82	rspcv	$⊢ 0_{S} \in B \to (\forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \to F ((x \underset{˙}{\cdot} y) \underset{˙}{+} 0_{S}) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (0_{S}))$
84	76 77 83	3syl	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to (\forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \to F ((x \underset{˙}{\cdot} y) \underset{˙}{+} 0_{S}) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (0_{S}))$
85		simplll	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to S \in LMod$
86		simprl	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to x \in E$
87		simprr	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to y \in B$
88	85 86 87 18	syl3anc	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to x \underset{˙}{\cdot} y \in B$
89	1 6 72	grprid	$⊢ (S \in Grp \land x \underset{˙}{\cdot} y \in B) \to (x \underset{˙}{\cdot} y) \underset{˙}{+} 0_{S} = x \underset{˙}{\cdot} y$
90	76 88 89	syl2anc	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to (x \underset{˙}{\cdot} y) \underset{˙}{+} 0_{S} = x \underset{˙}{\cdot} y$
91	90	fveq2d	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to F ((x \underset{˙}{\cdot} y) \underset{˙}{+} 0_{S}) = F (x \underset{˙}{\cdot} y)$
92		simplr3	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to F (0_{S}) = 0_{T}$
93	92	oveq2d	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (0_{S}) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} 0_{T}$
94		simpllr	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to T \in LMod$
95	94 31	syl	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to T \in Grp$
96		simplr2	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to L = K$
97	96	fveq2d	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to {Base}_{L} = {Base}_{K}$
98	97 5	eqtr4di	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to {Base}_{L} = E$
99	86 98	eleqtrrd	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to x \in {Base}_{L}$
100		simplr1	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to F : B ⟶ C$
101	100 87	ffvelcdmd	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to F (y) \in C$
102		eqid	$⊢ {Base}_{L} = {Base}_{L}$
103	2 4 9 102	lmodvscl	$⊢ (T \in LMod \land x \in {Base}_{L} \land F (y) \in C) \to x \underset{˙}{\times} F (y) \in C$
104	94 99 101 103	syl3anc	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to x \underset{˙}{\times} F (y) \in C$
105	2 7 73	grprid	$⊢ (T \in Grp \land x \underset{˙}{\times} F (y) \in C) \to (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} 0_{T} = x \underset{˙}{\times} F (y)$
106	95 104 105	syl2anc	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} 0_{T} = x \underset{˙}{\times} F (y)$
107	93 106	eqtrd	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (0_{S}) = x \underset{˙}{\times} F (y)$
108	91 107	eqeq12d	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to (F ((x \underset{˙}{\cdot} y) \underset{˙}{+} 0_{S}) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (0_{S}) \leftrightarrow F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y))$
109	84 108	sylibd	$⊢ (((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \land (x \in E \land y \in B)) \to (\forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \to F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y))$
110	109	ralimdvva	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land F (0_{S}) = 0_{T})) \to (\forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \to \forall x \in E \forall y \in B F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y))$
111	110	3exp2	$⊢ (S \in LMod \land T \in LMod) \to (F : B ⟶ C \to (L = K \to (F (0_{S}) = 0_{T} \to (\forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \to \forall x \in E \forall y \in B F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))))$
112	111	com45	$⊢ (S \in LMod \land T \in LMod) \to (F : B ⟶ C \to (L = K \to (\forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z) \to (F (0_{S}) = 0_{T} \to \forall x \in E \forall y \in B F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))))$
113	112	3imp2	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))) \to (F (0_{S}) = 0_{T} \to \forall x \in E \forall y \in B F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y))$
114	75 113	mpd	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))) \to \forall x \in E \forall y \in B F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)$
115	3 4 5 1 8 9	islmhm3	$⊢ (S \in LMod \land T \in LMod) \to (F \in (S LMHom T) \leftrightarrow (F \in (S GrpHom T) \land L = K \land \forall x \in E \forall y \in B F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))$
116	115	adantr	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))) \to (F \in (S LMHom T) \leftrightarrow (F \in (S GrpHom T) \land L = K \land \forall x \in E \forall y \in B F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))$
117	70 71 114 116	mpbir3and	$⊢ ((S \in LMod \land T \in LMod) \land (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z))) \to F \in (S LMHom T)$
118	29 117	impbida	$⊢ (S \in LMod \land T \in LMod) \to (F \in (S LMHom T) \leftrightarrow (F : B ⟶ C \land L = K \land \forall x \in E \forall y \in B \forall z \in B F ((x \underset{˙}{\cdot} y) \underset{˙}{+} z) = (x \underset{˙}{\times} F (y)) \underset{˙}{⨣} F (z)))$

Metamath Proof Explorer

Theorem islmhm2

Proof