reslmhm2

Description: Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

	Ref	Expression
Hypotheses	reslmhm2.u	$⊢ U = T ↾_{𝑠} X$
	reslmhm2.l	$⊢ L = LSubSp (T)$
Assertion	reslmhm2	$⊢ (F \in (S LMHom U) \land T \in LMod \land X \in L) \to F \in (S LMHom T)$

Proof

Step	Hyp	Ref	Expression
1		reslmhm2.u	$⊢ U = T ↾_{𝑠} X$
2		reslmhm2.l	$⊢ L = LSubSp (T)$
3		eqid	$⊢ {Base}_{S} = {Base}_{S}$
4		eqid	$⊢ \cdot_{S} = \cdot_{S}$
5		eqid	$⊢ \cdot_{T} = \cdot_{T}$
6		eqid	$⊢ Scalar (S) = Scalar (S)$
7		eqid	$⊢ Scalar (T) = Scalar (T)$
8		eqid	$⊢ {Base}_{Scalar (S)} = {Base}_{Scalar (S)}$
9		lmhmlmod1	$⊢ F \in (S LMHom U) \to S \in LMod$
10	9	3ad2ant1	$⊢ (F \in (S LMHom U) \land T \in LMod \land X \in L) \to S \in LMod$
11		simp2	$⊢ (F \in (S LMHom U) \land T \in LMod \land X \in L) \to T \in LMod$
12	1 7	resssca	$⊢ X \in L \to Scalar (T) = Scalar (U)$
13	12	3ad2ant3	$⊢ (F \in (S LMHom U) \land T \in LMod \land X \in L) \to Scalar (T) = Scalar (U)$
14		eqid	$⊢ Scalar (U) = Scalar (U)$
15	6 14	lmhmsca	$⊢ F \in (S LMHom U) \to Scalar (U) = Scalar (S)$
16	15	3ad2ant1	$⊢ (F \in (S LMHom U) \land T \in LMod \land X \in L) \to Scalar (U) = Scalar (S)$
17	13 16	eqtrd	$⊢ (F \in (S LMHom U) \land T \in LMod \land X \in L) \to Scalar (T) = Scalar (S)$
18		lmghm	$⊢ F \in (S LMHom U) \to F \in (S GrpHom U)$
19	18	3ad2ant1	$⊢ (F \in (S LMHom U) \land T \in LMod \land X \in L) \to F \in (S GrpHom U)$
20	2	lsssubg	$⊢ (T \in LMod \land X \in L) \to X \in SubGrp (T)$
21	20	3adant1	$⊢ (F \in (S LMHom U) \land T \in LMod \land X \in L) \to X \in SubGrp (T)$
22	1	resghm2	$⊢ (F \in (S GrpHom U) \land X \in SubGrp (T)) \to F \in (S GrpHom T)$
23	19 21 22	syl2anc	$⊢ (F \in (S LMHom U) \land T \in LMod \land X \in L) \to F \in (S GrpHom T)$
24		eqid	$⊢ \cdot_{U} = \cdot_{U}$
25	6 8 3 4 24	lmhmlin	$⊢ (F \in (S LMHom U) \land x \in {Base}_{Scalar (S)} \land y \in {Base}_{S}) \to F (x \cdot_{S} y) = x \cdot_{U} F (y)$
26	25	3expb	$⊢ (F \in (S LMHom U) \land (x \in {Base}_{Scalar (S)} \land y \in {Base}_{S})) \to F (x \cdot_{S} y) = x \cdot_{U} F (y)$
27	26	3ad2antl1	$⊢ ((F \in (S LMHom U) \land T \in LMod \land X \in L) \land (x \in {Base}_{Scalar (S)} \land y \in {Base}_{S})) \to F (x \cdot_{S} y) = x \cdot_{U} F (y)$
28		simpl3	$⊢ ((F \in (S LMHom U) \land T \in LMod \land X \in L) \land (x \in {Base}_{Scalar (S)} \land y \in {Base}_{S})) \to X \in L$
29	1 5	ressvsca	$⊢ X \in L \to \cdot_{T} = \cdot_{U}$
30	29	oveqd	$⊢ X \in L \to x \cdot_{T} F (y) = x \cdot_{U} F (y)$
31	28 30	syl	$⊢ ((F \in (S LMHom U) \land T \in LMod \land X \in L) \land (x \in {Base}_{Scalar (S)} \land y \in {Base}_{S})) \to x \cdot_{T} F (y) = x \cdot_{U} F (y)$
32	27 31	eqtr4d	$⊢ ((F \in (S LMHom U) \land T \in LMod \land X \in L) \land (x \in {Base}_{Scalar (S)} \land y \in {Base}_{S})) \to F (x \cdot_{S} y) = x \cdot_{T} F (y)$
33	3 4 5 6 7 8 10 11 17 23 32	islmhmd	$⊢ (F \in (S LMHom U) \land T \in LMod \land X \in L) \to F \in (S LMHom T)$

Metamath Proof Explorer

Theorem reslmhm2

Proof