frlmup3

Description: The range of such an evaluation map is the finite linear combinations of the target vectors and also the span of the target vectors. (Contributed by Stefan O'Rear, 6-Feb-2015)

	Ref	Expression
Hypotheses	frlmup.f	$⊢ F = R freeLMod I$
	frlmup.b	$⊢ B = {Base}_{F}$
	frlmup.c	$⊢ C = {Base}_{T}$
	frlmup.v	$⊢ \underset{˙}{\cdot} = \cdot_{T}$
	frlmup.e	$⊢ E = (x \in B ⟼ \sum_{T} (x {\underset{˙}{\cdot}}_{f} A))$
	frlmup.t	$⊢ φ \to T \in LMod$
	frlmup.i	$⊢ φ \to I \in X$
	frlmup.r	$⊢ φ \to R = Scalar (T)$
	frlmup.a	$⊢ φ \to A : I ⟶ C$
	frlmup.k	$⊢ K = LSpan (T)$
Assertion	frlmup3	$⊢ φ \to ran E = K (ran A)$

Proof

Step	Hyp	Ref	Expression
1		frlmup.f	$⊢ F = R freeLMod I$
2		frlmup.b	$⊢ B = {Base}_{F}$
3		frlmup.c	$⊢ C = {Base}_{T}$
4		frlmup.v	$⊢ \underset{˙}{\cdot} = \cdot_{T}$
5		frlmup.e	$⊢ E = (x \in B ⟼ \sum_{T} (x {\underset{˙}{\cdot}}_{f} A))$
6		frlmup.t	$⊢ φ \to T \in LMod$
7		frlmup.i	$⊢ φ \to I \in X$
8		frlmup.r	$⊢ φ \to R = Scalar (T)$
9		frlmup.a	$⊢ φ \to A : I ⟶ C$
10		frlmup.k	$⊢ K = LSpan (T)$
11	1 2 3 4 5 6 7 8 9	frlmup1	$⊢ φ \to E \in (F LMHom T)$
12		eqid	$⊢ Scalar (T) = Scalar (T)$
13	12	lmodring	$⊢ T \in LMod \to Scalar (T) \in Ring$
14	6 13	syl	$⊢ φ \to Scalar (T) \in Ring$
15	8 14	eqeltrd	$⊢ φ \to R \in Ring$
16		eqid	$⊢ R unitVec I = R unitVec I$
17	16 1 2	uvcff	$⊢ (R \in Ring \land I \in X) \to (R unitVec I) : I ⟶ B$
18	15 7 17	syl2anc	$⊢ φ \to (R unitVec I) : I ⟶ B$
19	18	frnd	$⊢ φ \to ran (R unitVec I) \subseteq B$
20		eqid	$⊢ LSpan (F) = LSpan (F)$
21	2 20 10	lmhmlsp	$⊢ (E \in (F LMHom T) \land ran (R unitVec I) \subseteq B) \to E [LSpan (F) (ran (R unitVec I))] = K (E [ran (R unitVec I)])$
22	11 19 21	syl2anc	$⊢ φ \to E [LSpan (F) (ran (R unitVec I))] = K (E [ran (R unitVec I)])$
23	2 3	lmhmf	$⊢ E \in (F LMHom T) \to E : B ⟶ C$
24	11 23	syl	$⊢ φ \to E : B ⟶ C$
25	24	ffnd	$⊢ φ \to E Fn B$
26		fnima	$⊢ E Fn B \to E [B] = ran E$
27	25 26	syl	$⊢ φ \to E [B] = ran E$
28		eqid	$⊢ LBasis (F) = LBasis (F)$
29	1 16 28	frlmlbs	$⊢ (R \in Ring \land I \in X) \to ran (R unitVec I) \in LBasis (F)$
30	15 7 29	syl2anc	$⊢ φ \to ran (R unitVec I) \in LBasis (F)$
31	2 28 20	lbssp	$⊢ ran (R unitVec I) \in LBasis (F) \to LSpan (F) (ran (R unitVec I)) = B$
32	30 31	syl	$⊢ φ \to LSpan (F) (ran (R unitVec I)) = B$
33	32	eqcomd	$⊢ φ \to B = LSpan (F) (ran (R unitVec I))$
34	33	imaeq2d	$⊢ φ \to E [B] = E [LSpan (F) (ran (R unitVec I))]$
35	27 34	eqtr3d	$⊢ φ \to ran E = E [LSpan (F) (ran (R unitVec I))]$
36		imaco	$⊢ (E \circ (R unitVec I)) [I] = E [(R unitVec I) [I]]$
37	9	ffnd	$⊢ φ \to A Fn I$
38	18	ffnd	$⊢ φ \to (R unitVec I) Fn I$
39		fnco	$⊢ (E Fn B \land (R unitVec I) Fn I \land ran (R unitVec I) \subseteq B) \to (E \circ (R unitVec I)) Fn I$
40	25 38 19 39	syl3anc	$⊢ φ \to (E \circ (R unitVec I)) Fn I$
41		fvco2	$⊢ ((R unitVec I) Fn I \land u \in I) \to (E \circ (R unitVec I)) (u) = E ((R unitVec I) (u))$
42	38 41	sylan	$⊢ (φ \land u \in I) \to (E \circ (R unitVec I)) (u) = E ((R unitVec I) (u))$
43	6	adantr	$⊢ (φ \land u \in I) \to T \in LMod$
44	7	adantr	$⊢ (φ \land u \in I) \to I \in X$
45	8	adantr	$⊢ (φ \land u \in I) \to R = Scalar (T)$
46	9	adantr	$⊢ (φ \land u \in I) \to A : I ⟶ C$
47		simpr	$⊢ (φ \land u \in I) \to u \in I$
48	1 2 3 4 5 43 44 45 46 47 16	frlmup2	$⊢ (φ \land u \in I) \to E ((R unitVec I) (u)) = A (u)$
49	42 48	eqtr2d	$⊢ (φ \land u \in I) \to A (u) = (E \circ (R unitVec I)) (u)$
50	37 40 49	eqfnfvd	$⊢ φ \to A = E \circ (R unitVec I)$
51	50	imaeq1d	$⊢ φ \to A [I] = (E \circ (R unitVec I)) [I]$
52		fnima	$⊢ A Fn I \to A [I] = ran A$
53	37 52	syl	$⊢ φ \to A [I] = ran A$
54	51 53	eqtr3d	$⊢ φ \to (E \circ (R unitVec I)) [I] = ran A$
55		fnima	$⊢ (R unitVec I) Fn I \to (R unitVec I) [I] = ran (R unitVec I)$
56	38 55	syl	$⊢ φ \to (R unitVec I) [I] = ran (R unitVec I)$
57	56	imaeq2d	$⊢ φ \to E [(R unitVec I) [I]] = E [ran (R unitVec I)]$
58	36 54 57	3eqtr3a	$⊢ φ \to ran A = E [ran (R unitVec I)]$
59	58	fveq2d	$⊢ φ \to K (ran A) = K (E [ran (R unitVec I)])$
60	22 35 59	3eqtr4d	$⊢ φ \to ran E = K (ran A)$

Metamath Proof Explorer

Theorem frlmup3

Proof