reslmhm2b

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	reslmhm2b	$⊢ (T \in LMod \land X \in L \land ran F \subseteq X) \to (F \in (S LMHom T) \leftrightarrow F \in (S LMHom U))$

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_{U} = \cdot_{U}$
6		eqid	$⊢ Scalar (S) = Scalar (S)$
7		eqid	$⊢ Scalar (U) = Scalar (U)$
8		eqid	$⊢ {Base}_{Scalar (S)} = {Base}_{Scalar (S)}$
9		lmhmlmod1	$⊢ F \in (S LMHom T) \to S \in LMod$
10	9	adantl	$⊢ ((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom T)) \to S \in LMod$
11		simpl1	$⊢ ((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom T)) \to T \in LMod$
12		simpl2	$⊢ ((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom T)) \to X \in L$
13	1 2	lsslmod	$⊢ (T \in LMod \land X \in L) \to U \in LMod$
14	11 12 13	syl2anc	$⊢ ((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom T)) \to U \in LMod$
15		eqid	$⊢ Scalar (T) = Scalar (T)$
16	1 15	resssca	$⊢ X \in L \to Scalar (T) = Scalar (U)$
17	16	3ad2ant2	$⊢ (T \in LMod \land X \in L \land ran F \subseteq X) \to Scalar (T) = Scalar (U)$
18	6 15	lmhmsca	$⊢ F \in (S LMHom T) \to Scalar (T) = Scalar (S)$
19	17 18	sylan9req	$⊢ ((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom T)) \to Scalar (U) = Scalar (S)$
20		lmghm	$⊢ F \in (S LMHom T) \to F \in (S GrpHom T)$
21	2	lsssubg	$⊢ (T \in LMod \land X \in L) \to X \in SubGrp (T)$
22	1	resghm2b	$⊢ (X \in SubGrp (T) \land ran F \subseteq X) \to (F \in (S GrpHom T) \leftrightarrow F \in (S GrpHom U))$
23	21 22	stoic3	$⊢ (T \in LMod \land X \in L \land ran F \subseteq X) \to (F \in (S GrpHom T) \leftrightarrow F \in (S GrpHom U))$
24	23	biimpa	$⊢ ((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S GrpHom T)) \to F \in (S GrpHom U)$
25	20 24	sylan2	$⊢ ((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom T)) \to F \in (S GrpHom U)$
26		eqid	$⊢ \cdot_{T} = \cdot_{T}$
27	6 8 3 4 26	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)$
28	27	3expb	$⊢ (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)$
29	28	adantll	$⊢ (((T \in LMod \land X \in L \land ran F \subseteq X) \land 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)$
30		simpll2	$⊢ (((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom T)) \land (x \in {Base}_{Scalar (S)} \land y \in {Base}_{S})) \to X \in L$
31	1 26	ressvsca	$⊢ X \in L \to \cdot_{T} = \cdot_{U}$
32	31	oveqd	$⊢ X \in L \to x \cdot_{T} F (y) = x \cdot_{U} F (y)$
33	30 32	syl	$⊢ (((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom T)) \land (x \in {Base}_{Scalar (S)} \land y \in {Base}_{S})) \to x \cdot_{T} F (y) = x \cdot_{U} F (y)$
34	29 33	eqtrd	$⊢ (((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom T)) \land (x \in {Base}_{Scalar (S)} \land y \in {Base}_{S})) \to F (x \cdot_{S} y) = x \cdot_{U} F (y)$
35	3 4 5 6 7 8 10 14 19 25 34	islmhmd	$⊢ ((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom T)) \to F \in (S LMHom U)$
36		simpr	$⊢ ((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom U)) \to F \in (S LMHom U)$
37		simpl1	$⊢ ((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom U)) \to T \in LMod$
38		simpl2	$⊢ ((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom U)) \to X \in L$
39	1 2	reslmhm2	$⊢ (F \in (S LMHom U) \land T \in LMod \land X \in L) \to F \in (S LMHom T)$
40	36 37 38 39	syl3anc	$⊢ ((T \in LMod \land X \in L \land ran F \subseteq X) \land F \in (S LMHom U)) \to F \in (S LMHom T)$
41	35 40	impbida	$⊢ (T \in LMod \land X \in L \land ran F \subseteq X) \to (F \in (S LMHom T) \leftrightarrow F \in (S LMHom U))$

Metamath Proof Explorer

Theorem reslmhm2b

Proof