reslmhm

Description: Restriction of a homomorphism to a subspace. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Hypotheses	reslmhm.u	$⊢ U = LSubSp (S)$
	reslmhm.r	$⊢ R = S ↾_{𝑠} X$
Assertion	reslmhm	$⊢ (F \in (S LMHom T) \land X \in U) \to {F ↾}_{X} \in (R LMHom T)$

Proof

Step	Hyp	Ref	Expression
1		reslmhm.u	$⊢ U = LSubSp (S)$
2		reslmhm.r	$⊢ R = S ↾_{𝑠} X$
3		lmhmlmod1	$⊢ F \in (S LMHom T) \to S \in LMod$
4	2 1	lsslmod	$⊢ (S \in LMod \land X \in U) \to R \in LMod$
5	3 4	sylan	$⊢ (F \in (S LMHom T) \land X \in U) \to R \in LMod$
6		lmhmlmod2	$⊢ F \in (S LMHom T) \to T \in LMod$
7	6	adantr	$⊢ (F \in (S LMHom T) \land X \in U) \to T \in LMod$
8		lmghm	$⊢ F \in (S LMHom T) \to F \in (S GrpHom T)$
9	1	lsssubg	$⊢ (S \in LMod \land X \in U) \to X \in SubGrp (S)$
10	3 9	sylan	$⊢ (F \in (S LMHom T) \land X \in U) \to X \in SubGrp (S)$
11	2	resghm	$⊢ (F \in (S GrpHom T) \land X \in SubGrp (S)) \to {F ↾}_{X} \in (R GrpHom T)$
12	8 10 11	syl2an2r	$⊢ (F \in (S LMHom T) \land X \in U) \to {F ↾}_{X} \in (R GrpHom T)$
13		eqid	$⊢ Scalar (S) = Scalar (S)$
14		eqid	$⊢ Scalar (T) = Scalar (T)$
15	13 14	lmhmsca	$⊢ F \in (S LMHom T) \to Scalar (T) = Scalar (S)$
16	2 13	resssca	$⊢ X \in U \to Scalar (S) = Scalar (R)$
17	15 16	sylan9eq	$⊢ (F \in (S LMHom T) \land X \in U) \to Scalar (T) = Scalar (R)$
18		simpll	$⊢ ((F \in (S LMHom T) \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in {Base}_{R})) \to F \in (S LMHom T)$
19		simprl	$⊢ ((F \in (S LMHom T) \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in {Base}_{R})) \to a \in {Base}_{Scalar (S)}$
20		eqid	$⊢ {Base}_{S} = {Base}_{S}$
21	20 1	lssss	$⊢ X \in U \to X \subseteq {Base}_{S}$
22	21	adantl	$⊢ (F \in (S LMHom T) \land X \in U) \to X \subseteq {Base}_{S}$
23	22	adantr	$⊢ ((F \in (S LMHom T) \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in {Base}_{R})) \to X \subseteq {Base}_{S}$
24	2 20	ressbas2	$⊢ X \subseteq {Base}_{S} \to X = {Base}_{R}$
25	22 24	syl	$⊢ (F \in (S LMHom T) \land X \in U) \to X = {Base}_{R}$
26	25	eleq2d	$⊢ (F \in (S LMHom T) \land X \in U) \to (b \in X \leftrightarrow b \in {Base}_{R})$
27	26	biimpar	$⊢ ((F \in (S LMHom T) \land X \in U) \land b \in {Base}_{R}) \to b \in X$
28	27	adantrl	$⊢ ((F \in (S LMHom T) \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in {Base}_{R})) \to b \in X$
29	23 28	sseldd	$⊢ ((F \in (S LMHom T) \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in {Base}_{R})) \to b \in {Base}_{S}$
30		eqid	$⊢ {Base}_{Scalar (S)} = {Base}_{Scalar (S)}$
31		eqid	$⊢ \cdot_{S} = \cdot_{S}$
32		eqid	$⊢ \cdot_{T} = \cdot_{T}$
33	13 30 20 31 32	lmhmlin	$⊢ (F \in (S LMHom T) \land a \in {Base}_{Scalar (S)} \land b \in {Base}_{S}) \to F (a \cdot_{S} b) = a \cdot_{T} F (b)$
34	18 19 29 33	syl3anc	$⊢ ((F \in (S LMHom T) \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in {Base}_{R})) \to F (a \cdot_{S} b) = a \cdot_{T} F (b)$
35	3	adantr	$⊢ (F \in (S LMHom T) \land X \in U) \to S \in LMod$
36	35	adantr	$⊢ ((F \in (S LMHom T) \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in {Base}_{R})) \to S \in LMod$
37		simplr	$⊢ ((F \in (S LMHom T) \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in {Base}_{R})) \to X \in U$
38	13 31 30 1	lssvscl	$⊢ ((S \in LMod \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in X)) \to a \cdot_{S} b \in X$
39	36 37 19 28 38	syl22anc	$⊢ ((F \in (S LMHom T) \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in {Base}_{R})) \to a \cdot_{S} b \in X$
40	39	fvresd	$⊢ ((F \in (S LMHom T) \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in {Base}_{R})) \to ({F ↾}_{X}) (a \cdot_{S} b) = F (a \cdot_{S} b)$
41		fvres	$⊢ b \in X \to ({F ↾}_{X}) (b) = F (b)$
42	41	oveq2d	$⊢ b \in X \to a \cdot_{T} ({F ↾}_{X}) (b) = a \cdot_{T} F (b)$
43	28 42	syl	$⊢ ((F \in (S LMHom T) \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in {Base}_{R})) \to a \cdot_{T} ({F ↾}_{X}) (b) = a \cdot_{T} F (b)$
44	34 40 43	3eqtr4d	$⊢ ((F \in (S LMHom T) \land X \in U) \land (a \in {Base}_{Scalar (S)} \land b \in {Base}_{R})) \to ({F ↾}_{X}) (a \cdot_{S} b) = a \cdot_{T} ({F ↾}_{X}) (b)$
45	44	ralrimivva	$⊢ (F \in (S LMHom T) \land X \in U) \to \forall a \in {Base}_{Scalar (S)} \forall b \in {Base}_{R} ({F ↾}_{X}) (a \cdot_{S} b) = a \cdot_{T} ({F ↾}_{X}) (b)$
46	16	adantl	$⊢ (F \in (S LMHom T) \land X \in U) \to Scalar (S) = Scalar (R)$
47	46	fveq2d	$⊢ (F \in (S LMHom T) \land X \in U) \to {Base}_{Scalar (S)} = {Base}_{Scalar (R)}$
48	2 31	ressvsca	$⊢ X \in U \to \cdot_{S} = \cdot_{R}$
49	48	adantl	$⊢ (F \in (S LMHom T) \land X \in U) \to \cdot_{S} = \cdot_{R}$
50	49	oveqd	$⊢ (F \in (S LMHom T) \land X \in U) \to a \cdot_{S} b = a \cdot_{R} b$
51	50	fveqeq2d	$⊢ (F \in (S LMHom T) \land X \in U) \to (({F ↾}_{X}) (a \cdot_{S} b) = a \cdot_{T} ({F ↾}_{X}) (b) \leftrightarrow ({F ↾}_{X}) (a \cdot_{R} b) = a \cdot_{T} ({F ↾}_{X}) (b))$
52	51	ralbidv	$⊢ (F \in (S LMHom T) \land X \in U) \to (\forall b \in {Base}_{R} ({F ↾}_{X}) (a \cdot_{S} b) = a \cdot_{T} ({F ↾}_{X}) (b) \leftrightarrow \forall b \in {Base}_{R} ({F ↾}_{X}) (a \cdot_{R} b) = a \cdot_{T} ({F ↾}_{X}) (b))$
53	47 52	raleqbidv	$⊢ (F \in (S LMHom T) \land X \in U) \to (\forall a \in {Base}_{Scalar (S)} \forall b \in {Base}_{R} ({F ↾}_{X}) (a \cdot_{S} b) = a \cdot_{T} ({F ↾}_{X}) (b) \leftrightarrow \forall a \in {Base}_{Scalar (R)} \forall b \in {Base}_{R} ({F ↾}_{X}) (a \cdot_{R} b) = a \cdot_{T} ({F ↾}_{X}) (b))$
54	45 53	mpbid	$⊢ (F \in (S LMHom T) \land X \in U) \to \forall a \in {Base}_{Scalar (R)} \forall b \in {Base}_{R} ({F ↾}_{X}) (a \cdot_{R} b) = a \cdot_{T} ({F ↾}_{X}) (b)$
55	12 17 54	3jca	$⊢ (F \in (S LMHom T) \land X \in U) \to ({F ↾}_{X} \in (R GrpHom T) \land Scalar (T) = Scalar (R) \land \forall a \in {Base}_{Scalar (R)} \forall b \in {Base}_{R} ({F ↾}_{X}) (a \cdot_{R} b) = a \cdot_{T} ({F ↾}_{X}) (b))$
56		eqid	$⊢ Scalar (R) = Scalar (R)$
57		eqid	$⊢ {Base}_{Scalar (R)} = {Base}_{Scalar (R)}$
58		eqid	$⊢ {Base}_{R} = {Base}_{R}$
59		eqid	$⊢ \cdot_{R} = \cdot_{R}$
60	56 14 57 58 59 32	islmhm	$⊢ {F ↾}_{X} \in (R LMHom T) \leftrightarrow ((R \in LMod \land T \in LMod) \land ({F ↾}_{X} \in (R GrpHom T) \land Scalar (T) = Scalar (R) \land \forall a \in {Base}_{Scalar (R)} \forall b \in {Base}_{R} ({F ↾}_{X}) (a \cdot_{R} b) = a \cdot_{T} ({F ↾}_{X}) (b)))$
61	5 7 55 60	syl21anbrc	$⊢ (F \in (S LMHom T) \land X \in U) \to {F ↾}_{X} \in (R LMHom T)$

Metamath Proof Explorer

Theorem reslmhm

Proof