lmhmima

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

	Ref	Expression
Hypotheses	lmhmima.x	$⊢ X = LSubSp (S)$
	lmhmima.y	$⊢ Y = LSubSp (T)$
Assertion	lmhmima	$⊢ (F \in (S LMHom T) \land U \in X) \to F [U] \in Y$

Proof

Step	Hyp	Ref	Expression
1		lmhmima.x	$⊢ X = LSubSp (S)$
2		lmhmima.y	$⊢ Y = LSubSp (T)$
3		lmghm	$⊢ F \in (S LMHom T) \to F \in (S GrpHom T)$
4		lmhmlmod1	$⊢ F \in (S LMHom T) \to S \in LMod$
5		simpr	$⊢ (F \in (S LMHom T) \land U \in X) \to U \in X$
6	1	lsssubg	$⊢ (S \in LMod \land U \in X) \to U \in SubGrp (S)$
7	4 5 6	syl2an2r	$⊢ (F \in (S LMHom T) \land U \in X) \to U \in SubGrp (S)$
8		ghmima	$⊢ (F \in (S GrpHom T) \land U \in SubGrp (S)) \to F [U] \in SubGrp (T)$
9	3 7 8	syl2an2r	$⊢ (F \in (S LMHom T) \land U \in X) \to F [U] \in SubGrp (T)$
10		eqid	$⊢ {Base}_{S} = {Base}_{S}$
11		eqid	$⊢ {Base}_{T} = {Base}_{T}$
12	10 11	lmhmf	$⊢ F \in (S LMHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
13	12	adantr	$⊢ (F \in (S LMHom T) \land U \in X) \to F : {Base}_{S} ⟶ {Base}_{T}$
14		ffn	$⊢ F : {Base}_{S} ⟶ {Base}_{T} \to F Fn {Base}_{S}$
15	13 14	syl	$⊢ (F \in (S LMHom T) \land U \in X) \to F Fn {Base}_{S}$
16	10 1	lssss	$⊢ U \in X \to U \subseteq {Base}_{S}$
17	5 16	syl	$⊢ (F \in (S LMHom T) \land U \in X) \to U \subseteq {Base}_{S}$
18	15 17	fvelimabd	$⊢ (F \in (S LMHom T) \land U \in X) \to (b \in F [U] \leftrightarrow \exists c \in U F (c) = b)$
19	18	adantr	$⊢ ((F \in (S LMHom T) \land U \in X) \land a \in {Base}_{Scalar (T)}) \to (b \in F [U] \leftrightarrow \exists c \in U F (c) = b)$
20		simpll	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land c \in U)) \to F \in (S LMHom T)$
21		eqid	$⊢ Scalar (S) = Scalar (S)$
22		eqid	$⊢ Scalar (T) = Scalar (T)$
23	21 22	lmhmsca	$⊢ F \in (S LMHom T) \to Scalar (T) = Scalar (S)$
24	23	adantr	$⊢ (F \in (S LMHom T) \land U \in X) \to Scalar (T) = Scalar (S)$
25	24	fveq2d	$⊢ (F \in (S LMHom T) \land U \in X) \to {Base}_{Scalar (T)} = {Base}_{Scalar (S)}$
26	25	eleq2d	$⊢ (F \in (S LMHom T) \land U \in X) \to (a \in {Base}_{Scalar (T)} \leftrightarrow a \in {Base}_{Scalar (S)})$
27	26	biimpa	$⊢ ((F \in (S LMHom T) \land U \in X) \land a \in {Base}_{Scalar (T)}) \to a \in {Base}_{Scalar (S)}$
28	27	adantrr	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land c \in U)) \to a \in {Base}_{Scalar (S)}$
29	17	sselda	$⊢ ((F \in (S LMHom T) \land U \in X) \land c \in U) \to c \in {Base}_{S}$
30	29	adantrl	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land c \in U)) \to c \in {Base}_{S}$
31		eqid	$⊢ {Base}_{Scalar (S)} = {Base}_{Scalar (S)}$
32		eqid	$⊢ \cdot_{S} = \cdot_{S}$
33		eqid	$⊢ \cdot_{T} = \cdot_{T}$
34	21 31 10 32 33	lmhmlin	$⊢ (F \in (S LMHom T) \land a \in {Base}_{Scalar (S)} \land c \in {Base}_{S}) \to F (a \cdot_{S} c) = a \cdot_{T} F (c)$
35	20 28 30 34	syl3anc	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land c \in U)) \to F (a \cdot_{S} c) = a \cdot_{T} F (c)$
36	20 12 14	3syl	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land c \in U)) \to F Fn {Base}_{S}$
37		simplr	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land c \in U)) \to U \in X$
38	37 16	syl	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land c \in U)) \to U \subseteq {Base}_{S}$
39	4	adantr	$⊢ (F \in (S LMHom T) \land U \in X) \to S \in LMod$
40	39	adantr	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land c \in U)) \to S \in LMod$
41		simprr	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land c \in U)) \to c \in U$
42	21 32 31 1	lssvscl	$⊢ ((S \in LMod \land U \in X) \land (a \in {Base}_{Scalar (S)} \land c \in U)) \to a \cdot_{S} c \in U$
43	40 37 28 41 42	syl22anc	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land c \in U)) \to a \cdot_{S} c \in U$
44		fnfvima	$⊢ (F Fn {Base}_{S} \land U \subseteq {Base}_{S} \land a \cdot_{S} c \in U) \to F (a \cdot_{S} c) \in F [U]$
45	36 38 43 44	syl3anc	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land c \in U)) \to F (a \cdot_{S} c) \in F [U]$
46	35 45	eqeltrrd	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land c \in U)) \to a \cdot_{T} F (c) \in F [U]$
47	46	anassrs	$⊢ (((F \in (S LMHom T) \land U \in X) \land a \in {Base}_{Scalar (T)}) \land c \in U) \to a \cdot_{T} F (c) \in F [U]$
48		oveq2	$⊢ F (c) = b \to a \cdot_{T} F (c) = a \cdot_{T} b$
49	48	eleq1d	$⊢ F (c) = b \to (a \cdot_{T} F (c) \in F [U] \leftrightarrow a \cdot_{T} b \in F [U])$
50	47 49	syl5ibcom	$⊢ (((F \in (S LMHom T) \land U \in X) \land a \in {Base}_{Scalar (T)}) \land c \in U) \to (F (c) = b \to a \cdot_{T} b \in F [U])$
51	50	rexlimdva	$⊢ ((F \in (S LMHom T) \land U \in X) \land a \in {Base}_{Scalar (T)}) \to (\exists c \in U F (c) = b \to a \cdot_{T} b \in F [U])$
52	19 51	sylbid	$⊢ ((F \in (S LMHom T) \land U \in X) \land a \in {Base}_{Scalar (T)}) \to (b \in F [U] \to a \cdot_{T} b \in F [U])$
53	52	impr	$⊢ ((F \in (S LMHom T) \land U \in X) \land (a \in {Base}_{Scalar (T)} \land b \in F [U])) \to a \cdot_{T} b \in F [U]$
54	53	ralrimivva	$⊢ (F \in (S LMHom T) \land U \in X) \to \forall a \in {Base}_{Scalar (T)} \forall b \in F [U] a \cdot_{T} b \in F [U]$
55		lmhmlmod2	$⊢ F \in (S LMHom T) \to T \in LMod$
56	55	adantr	$⊢ (F \in (S LMHom T) \land U \in X) \to T \in LMod$
57		eqid	$⊢ {Base}_{Scalar (T)} = {Base}_{Scalar (T)}$
58	22 57 11 33 2	islss4	$⊢ T \in LMod \to (F [U] \in Y \leftrightarrow (F [U] \in SubGrp (T) \land \forall a \in {Base}_{Scalar (T)} \forall b \in F [U] a \cdot_{T} b \in F [U]))$
59	56 58	syl	$⊢ (F \in (S LMHom T) \land U \in X) \to (F [U] \in Y \leftrightarrow (F [U] \in SubGrp (T) \land \forall a \in {Base}_{Scalar (T)} \forall b \in F [U] a \cdot_{T} b \in F [U]))$
60	9 54 59	mpbir2and	$⊢ (F \in (S LMHom T) \land U \in X) \to F [U] \in Y$

Metamath Proof Explorer

Theorem lmhmima

Proof