islmhm

Description: Property of being a homomorphism of left modules. (Contributed by Stefan O'Rear, 1-Jan-2015) (Proof shortened by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	islmhm.k	$⊢ K = Scalar (S)$
	islmhm.l	$⊢ L = Scalar (T)$
	islmhm.b	$⊢ B = {Base}_{K}$
	islmhm.e	$⊢ E = {Base}_{S}$
	islmhm.m	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	islmhm.n	$⊢ \underset{˙}{\times} = \cdot_{T}$
Assertion	islmhm	$⊢ F \in (S LMHom T) \leftrightarrow ((S \in LMod \land T \in LMod) \land (F \in (S GrpHom T) \land L = K \land \forall x \in B \forall y \in E F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))$

Proof

Step	Hyp	Ref	Expression
1		islmhm.k	$⊢ K = Scalar (S)$
2		islmhm.l	$⊢ L = Scalar (T)$
3		islmhm.b	$⊢ B = {Base}_{K}$
4		islmhm.e	$⊢ E = {Base}_{S}$
5		islmhm.m	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
6		islmhm.n	$⊢ \underset{˙}{\times} = \cdot_{T}$
7		df-lmhm	$⊢ LMHom = (s \in LMod, t \in LMod ⟼ \{f \in (s GrpHom t) \| \underset{˙}{[} Scalar (s) / w \underset{˙}{]} (Scalar (t) = w \land \forall x \in {Base}_{w} \forall y \in {Base}_{s} f (x \cdot_{s} y) = x \cdot_{t} f (y))\})$
8	7	elmpocl	$⊢ F \in (S LMHom T) \to (S \in LMod \land T \in LMod)$
9		oveq12	$⊢ (s = S \land t = T) \to s GrpHom t = S GrpHom T$
10		fvexd	$⊢ (s = S \land t = T) \to Scalar (s) \in V$
11		simplr	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to t = T$
12	11	fveq2d	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to Scalar (t) = Scalar (T)$
13	12 2	eqtr4di	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to Scalar (t) = L$
14		simpr	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to w = Scalar (s)$
15		simpll	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to s = S$
16	15	fveq2d	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to Scalar (s) = Scalar (S)$
17	14 16	eqtrd	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to w = Scalar (S)$
18	17 1	eqtr4di	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to w = K$
19	13 18	eqeq12d	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to (Scalar (t) = w \leftrightarrow L = K)$
20	18	fveq2d	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to {Base}_{w} = {Base}_{K}$
21	20 3	eqtr4di	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to {Base}_{w} = B$
22	15	fveq2d	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to {Base}_{s} = {Base}_{S}$
23	22 4	eqtr4di	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to {Base}_{s} = E$
24	15	fveq2d	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to \cdot_{s} = \cdot_{S}$
25	24 5	eqtr4di	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to \cdot_{s} = \underset{˙}{\cdot}$
26	25	oveqd	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to x \cdot_{s} y = x \underset{˙}{\cdot} y$
27	26	fveq2d	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to f (x \cdot_{s} y) = f (x \underset{˙}{\cdot} y)$
28	11	fveq2d	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to \cdot_{t} = \cdot_{T}$
29	28 6	eqtr4di	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to \cdot_{t} = \underset{˙}{\times}$
30	29	oveqd	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to x \cdot_{t} f (y) = x \underset{˙}{\times} f (y)$
31	27 30	eqeq12d	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to (f (x \cdot_{s} y) = x \cdot_{t} f (y) \leftrightarrow f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y))$
32	23 31	raleqbidv	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to (\forall y \in {Base}_{s} f (x \cdot_{s} y) = x \cdot_{t} f (y) \leftrightarrow \forall y \in E f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y))$
33	21 32	raleqbidv	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to (\forall x \in {Base}_{w} \forall y \in {Base}_{s} f (x \cdot_{s} y) = x \cdot_{t} f (y) \leftrightarrow \forall x \in B \forall y \in E f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y))$
34	19 33	anbi12d	$⊢ ((s = S \land t = T) \land w = Scalar (s)) \to ((Scalar (t) = w \land \forall x \in {Base}_{w} \forall y \in {Base}_{s} f (x \cdot_{s} y) = x \cdot_{t} f (y)) \leftrightarrow (L = K \land \forall x \in B \forall y \in E f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y)))$
35	10 34	sbcied	$⊢ (s = S \land t = T) \to (\underset{˙}{[} Scalar (s) / w \underset{˙}{]} (Scalar (t) = w \land \forall x \in {Base}_{w} \forall y \in {Base}_{s} f (x \cdot_{s} y) = x \cdot_{t} f (y)) \leftrightarrow (L = K \land \forall x \in B \forall y \in E f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y)))$
36	9 35	rabeqbidv	$⊢ (s = S \land t = T) \to \{f \in (s GrpHom t) \| \underset{˙}{[} Scalar (s) / w \underset{˙}{]} (Scalar (t) = w \land \forall x \in {Base}_{w} \forall y \in {Base}_{s} f (x \cdot_{s} y) = x \cdot_{t} f (y))\} = \{f \in (S GrpHom T) \| (L = K \land \forall x \in B \forall y \in E f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y))\}$
37		ovex	$⊢ S GrpHom T \in V$
38	37	rabex	$⊢ \{f \in (S GrpHom T) \| (L = K \land \forall x \in B \forall y \in E f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y))\} \in V$
39	36 7 38	ovmpoa	$⊢ (S \in LMod \land T \in LMod) \to S LMHom T = \{f \in (S GrpHom T) \| (L = K \land \forall x \in B \forall y \in E f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y))\}$
40	39	eleq2d	$⊢ (S \in LMod \land T \in LMod) \to (F \in (S LMHom T) \leftrightarrow F \in \{f \in (S GrpHom T) \| (L = K \land \forall x \in B \forall y \in E f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y))\})$
41		fveq1	$⊢ f = F \to f (x \underset{˙}{\cdot} y) = F (x \underset{˙}{\cdot} y)$
42		fveq1	$⊢ f = F \to f (y) = F (y)$
43	42	oveq2d	$⊢ f = F \to x \underset{˙}{\times} f (y) = x \underset{˙}{\times} F (y)$
44	41 43	eqeq12d	$⊢ f = F \to (f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y) \leftrightarrow F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y))$
45	44	2ralbidv	$⊢ f = F \to (\forall x \in B \forall y \in E f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y) \leftrightarrow \forall x \in B \forall y \in E F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y))$
46	45	anbi2d	$⊢ f = F \to ((L = K \land \forall x \in B \forall y \in E f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y)) \leftrightarrow (L = K \land \forall x \in B \forall y \in E F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))$
47	46	elrab	$⊢ F \in \{f \in (S GrpHom T) \| (L = K \land \forall x \in B \forall y \in E f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y))\} \leftrightarrow (F \in (S GrpHom T) \land (L = K \land \forall x \in B \forall y \in E F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))$
48		3anass	$⊢ (F \in (S GrpHom T) \land L = K \land \forall x \in B \forall y \in E F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)) \leftrightarrow (F \in (S GrpHom T) \land (L = K \land \forall x \in B \forall y \in E F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))$
49	47 48	bitr4i	$⊢ F \in \{f \in (S GrpHom T) \| (L = K \land \forall x \in B \forall y \in E f (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} f (y))\} \leftrightarrow (F \in (S GrpHom T) \land L = K \land \forall x \in B \forall y \in E F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y))$
50	40 49	bitrdi	$⊢ (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 B \forall y \in E F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))$
51	8 50	biadanii	$⊢ F \in (S LMHom T) \leftrightarrow ((S \in LMod \land T \in LMod) \land (F \in (S GrpHom T) \land L = K \land \forall x \in B \forall y \in E F (x \underset{˙}{\cdot} y) = x \underset{˙}{\times} F (y)))$

Metamath Proof Explorer

Theorem islmhm

Proof