Theorem reslmhm

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

	Ref	Expression
Hypotheses	reslmhm.u	⊢ 𝑈 = ( LSubSp ‘ 𝑆 )
	reslmhm.r	⊢ 𝑅 = ( 𝑆 ↾s 𝑋 )
Assertion	reslmhm	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 LMHom 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		reslmhm.u	⊢ 𝑈 = ( LSubSp ‘ 𝑆 )
2		reslmhm.r	⊢ 𝑅 = ( 𝑆 ↾s 𝑋 )
3		lmhmlmod1	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
4	2 1	lsslmod	⊢ ( ( 𝑆 ∈ LMod ∧ 𝑋 ∈ 𝑈 ) → 𝑅 ∈ LMod )
5	3 4	sylan	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑅 ∈ LMod )
6		lmhmlmod2	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
7	6	adantr	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑇 ∈ LMod )
8		lmghm	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
9	1	lsssubg	⊢ ( ( 𝑆 ∈ LMod ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( SubGrp ‘ 𝑆 ) )
10	3 9	sylan	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( SubGrp ‘ 𝑆 ) )
11	2	resghm	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ ( SubGrp ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 GrpHom 𝑇 ) )
12	8 10 11	syl2an2r	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 GrpHom 𝑇 ) )
13		eqid	⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
14		eqid	⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
15	13 14	lmhmsca	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑆 ) )
16	2 13	resssca	⊢ ( 𝑋 ∈ 𝑈 → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑅 ) )
17	15 16	sylan9eq	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑅 ) )
18		simpll	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
19		simprl	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
20		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
21	20 1	lssss	⊢ ( 𝑋 ∈ 𝑈 → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
22	21	adantl	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
23	22	adantr	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
24	2 20	ressbas2	⊢ ( 𝑋 ⊆ ( Base ‘ 𝑆 ) → 𝑋 = ( Base ‘ 𝑅 ) )
25	22 24	syl	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑋 = ( Base ‘ 𝑅 ) )
26	25	eleq2d	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝑏 ∈ 𝑋 ↔ 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
27	26	biimpar	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → 𝑏 ∈ 𝑋 )
28	27	adantrl	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑏 ∈ 𝑋 )
29	23 28	sseldd	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑆 ) )
30		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
31		eqid	⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
32		eqid	⊢ ( ·𝑠 ‘ 𝑇 ) = ( ·𝑠 ‘ 𝑇 )
33	13 30 20 31 32	lmhmlin	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) )
34	18 19 29 33	syl3anc	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) )
35	3	adantr	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑆 ∈ LMod )
36	35	adantr	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑆 ∈ LMod )
37		simplr	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑋 ∈ 𝑈 )
38	13 31 30 1	lssvscl	⊢ ( ( ( 𝑆 ∈ LMod ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ 𝑋 )
39	36 37 19 28 38	syl22anc	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ∈ 𝑋 )
40	39	fvresd	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) )
41		fvres	⊢ ( 𝑏 ∈ 𝑋 → ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) = ( 𝐹 ‘ 𝑏 ) )
42	41	oveq2d	⊢ ( 𝑏 ∈ 𝑋 → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) )
43	28 42	syl	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝑏 ) ) )
44	34 40 43	3eqtr4d	⊢ ( ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) )
45	44	ralrimivva	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) )
46	16	adantl	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑅 ) )
47	46	fveq2d	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑅 ) ) )
48	2 31	ressvsca	⊢ ( 𝑋 ∈ 𝑈 → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑅 ) )
49	48	adantl	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑅 ) )
50	49	oveqd	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) = ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) )
51	50	fveqeq2d	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ↔ ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ) )
52	51	ralbidv	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ↔ ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ) )
53	47 52	raleqbidv	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑆 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ) )
54	45 53	mpbid	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) )
55	12 17 54	3jca	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 GrpHom 𝑇 ) ∧ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ) )
56		eqid	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
57		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑅 ) ) = ( Base ‘ ( Scalar ‘ 𝑅 ) )
58		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
59		eqid	⊢ ( ·𝑠 ‘ 𝑅 ) = ( ·𝑠 ‘ 𝑅 )
60	56 14 57 58 59 32	islmhm	⊢ ( ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 LMHom 𝑇 ) ↔ ( ( 𝑅 ∈ LMod ∧ 𝑇 ∈ LMod ) ∧ ( ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 GrpHom 𝑇 ) ∧ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑅 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑎 ( ·𝑠 ‘ 𝑅 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑏 ) ) ) ) )
61	5 7 55 60	syl21anbrc	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑅 LMHom 𝑇 ) )