lmhmeql

Description: The equalizer of two module homomorphisms is a subspace. (Contributed by Stefan O'Rear, 7-Mar-2015)

		Ref	Expression
	Hypothesis	lmhmeql.u	$⊢ U = LSubSp (S)$
	Assertion	lmhmeql	$⊢ (F \in (S LMHom T) \land G \in (S LMHom T)) \to dom (F \cap G) \in U$

Proof

Step	Hyp	Ref	Expression
1		lmhmeql.u	$⊢ U = LSubSp (S)$
2		lmghm	$⊢ F \in (S LMHom T) \to F \in (S GrpHom T)$
3		lmghm	$⊢ G \in (S LMHom T) \to G \in (S GrpHom T)$
4		ghmeql	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to dom (F \cap G) \in SubGrp (S)$
5	2 3 4	syl2an	$⊢ (F \in (S LMHom T) \land G \in (S LMHom T)) \to dom (F \cap G) \in SubGrp (S)$
6		fveq2	$⊢ z = x \cdot_{S} y \to F (z) = F (x \cdot_{S} y)$
7		fveq2	$⊢ z = x \cdot_{S} y \to G (z) = G (x \cdot_{S} y)$
8	6 7	eqeq12d	$⊢ z = x \cdot_{S} y \to (F (z) = G (z) \leftrightarrow F (x \cdot_{S} y) = G (x \cdot_{S} y))$
9		lmhmlmod1	$⊢ F \in (S LMHom T) \to S \in LMod$
10	9	adantr	$⊢ (F \in (S LMHom T) \land G \in (S LMHom T)) \to S \in LMod$
11	10	ad2antrr	$⊢ (((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \land (y \in {Base}_{S} \land F (y) = G (y))) \to S \in LMod$
12		simplr	$⊢ (((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \land (y \in {Base}_{S} \land F (y) = G (y))) \to x \in {Base}_{Scalar (S)}$
13		simprl	$⊢ (((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \land (y \in {Base}_{S} \land F (y) = G (y))) \to y \in {Base}_{S}$
14		eqid	$⊢ {Base}_{S} = {Base}_{S}$
15		eqid	$⊢ Scalar (S) = Scalar (S)$
16		eqid	$⊢ \cdot_{S} = \cdot_{S}$
17		eqid	$⊢ {Base}_{Scalar (S)} = {Base}_{Scalar (S)}$
18	14 15 16 17	lmodvscl	$⊢ (S \in LMod \land x \in {Base}_{Scalar (S)} \land y \in {Base}_{S}) \to x \cdot_{S} y \in {Base}_{S}$
19	11 12 13 18	syl3anc	$⊢ (((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \land (y \in {Base}_{S} \land F (y) = G (y))) \to x \cdot_{S} y \in {Base}_{S}$
20		oveq2	$⊢ F (y) = G (y) \to x \cdot_{T} F (y) = x \cdot_{T} G (y)$
21	20	ad2antll	$⊢ (((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \land (y \in {Base}_{S} \land F (y) = G (y))) \to x \cdot_{T} F (y) = x \cdot_{T} G (y)$
22		simplll	$⊢ (((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \land (y \in {Base}_{S} \land F (y) = G (y))) \to F \in (S LMHom T)$
23		eqid	$⊢ \cdot_{T} = \cdot_{T}$
24	15 17 14 16 23	lmhmlin	$⊢ (F \in (S LMHom T) \land x \in {Base}_{Scalar (S)} \land y \in {Base}_{S}) \to F (x \cdot_{S} y) = x \cdot_{T} F (y)$
25	22 12 13 24	syl3anc	$⊢ (((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \land (y \in {Base}_{S} \land F (y) = G (y))) \to F (x \cdot_{S} y) = x \cdot_{T} F (y)$
26		simpllr	$⊢ (((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \land (y \in {Base}_{S} \land F (y) = G (y))) \to G \in (S LMHom T)$
27	15 17 14 16 23	lmhmlin	$⊢ (G \in (S LMHom T) \land x \in {Base}_{Scalar (S)} \land y \in {Base}_{S}) \to G (x \cdot_{S} y) = x \cdot_{T} G (y)$
28	26 12 13 27	syl3anc	$⊢ (((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \land (y \in {Base}_{S} \land F (y) = G (y))) \to G (x \cdot_{S} y) = x \cdot_{T} G (y)$
29	21 25 28	3eqtr4d	$⊢ (((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \land (y \in {Base}_{S} \land F (y) = G (y))) \to F (x \cdot_{S} y) = G (x \cdot_{S} y)$
30	8 19 29	elrabd	$⊢ (((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \land (y \in {Base}_{S} \land F (y) = G (y))) \to x \cdot_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\}$
31	30	expr	$⊢ (((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \land y \in {Base}_{S}) \to (F (y) = G (y) \to x \cdot_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\})$
32	31	ralrimiva	$⊢ ((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \to \forall y \in {Base}_{S} (F (y) = G (y) \to x \cdot_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\})$
33		eqid	$⊢ {Base}_{T} = {Base}_{T}$
34	14 33	lmhmf	$⊢ F \in (S LMHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
35	34	ffnd	$⊢ F \in (S LMHom T) \to F Fn {Base}_{S}$
36	14 33	lmhmf	$⊢ G \in (S LMHom T) \to G : {Base}_{S} ⟶ {Base}_{T}$
37	36	ffnd	$⊢ G \in (S LMHom T) \to G Fn {Base}_{S}$
38		fndmin	$⊢ (F Fn {Base}_{S} \land G Fn {Base}_{S}) \to dom (F \cap G) = \{z \in {Base}_{S} \| F (z) = G (z)\}$
39	35 37 38	syl2an	$⊢ (F \in (S LMHom T) \land G \in (S LMHom T)) \to dom (F \cap G) = \{z \in {Base}_{S} \| F (z) = G (z)\}$
40	39	adantr	$⊢ ((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \to dom (F \cap G) = \{z \in {Base}_{S} \| F (z) = G (z)\}$
41		eleq2	$⊢ dom (F \cap G) = \{z \in {Base}_{S} \| F (z) = G (z)\} \to (x \cdot_{S} y \in dom (F \cap G) \leftrightarrow x \cdot_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\})$
42	41	raleqbi1dv	$⊢ dom (F \cap G) = \{z \in {Base}_{S} \| F (z) = G (z)\} \to (\forall y \in dom (F \cap G) x \cdot_{S} y \in dom (F \cap G) \leftrightarrow \forall y \in \{z \in {Base}_{S} \| F (z) = G (z)\} x \cdot_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\})$
43		fveq2	$⊢ z = y \to F (z) = F (y)$
44		fveq2	$⊢ z = y \to G (z) = G (y)$
45	43 44	eqeq12d	$⊢ z = y \to (F (z) = G (z) \leftrightarrow F (y) = G (y))$
46	45	ralrab	$⊢ \forall y \in \{z \in {Base}_{S} \| F (z) = G (z)\} x \cdot_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\} \leftrightarrow \forall y \in {Base}_{S} (F (y) = G (y) \to x \cdot_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\})$
47	42 46	bitrdi	$⊢ dom (F \cap G) = \{z \in {Base}_{S} \| F (z) = G (z)\} \to (\forall y \in dom (F \cap G) x \cdot_{S} y \in dom (F \cap G) \leftrightarrow \forall y \in {Base}_{S} (F (y) = G (y) \to x \cdot_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\}))$
48	40 47	syl	$⊢ ((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \to (\forall y \in dom (F \cap G) x \cdot_{S} y \in dom (F \cap G) \leftrightarrow \forall y \in {Base}_{S} (F (y) = G (y) \to x \cdot_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\}))$
49	32 48	mpbird	$⊢ ((F \in (S LMHom T) \land G \in (S LMHom T)) \land x \in {Base}_{Scalar (S)}) \to \forall y \in dom (F \cap G) x \cdot_{S} y \in dom (F \cap G)$
50	49	ralrimiva	$⊢ (F \in (S LMHom T) \land G \in (S LMHom T)) \to \forall x \in {Base}_{Scalar (S)} \forall y \in dom (F \cap G) x \cdot_{S} y \in dom (F \cap G)$
51	15 17 14 16 1	islss4	$⊢ S \in LMod \to (dom (F \cap G) \in U \leftrightarrow (dom (F \cap G) \in SubGrp (S) \land \forall x \in {Base}_{Scalar (S)} \forall y \in dom (F \cap G) x \cdot_{S} y \in dom (F \cap G)))$
52	10 51	syl	$⊢ (F \in (S LMHom T) \land G \in (S LMHom T)) \to (dom (F \cap G) \in U \leftrightarrow (dom (F \cap G) \in SubGrp (S) \land \forall x \in {Base}_{Scalar (S)} \forall y \in dom (F \cap G) x \cdot_{S} y \in dom (F \cap G)))$
53	5 50 52	mpbir2and	$⊢ (F \in (S LMHom T) \land G \in (S LMHom T)) \to dom (F \cap G) \in U$

Metamath Proof Explorer

Theorem lmhmeql

Proof