frlmup2

Description: The evaluation map has the intended behavior on the unit vectors. (Contributed by Stefan O'Rear, 7-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

	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.y	$⊢ φ \to Y \in I$
	frlmup.u	$⊢ U = R unitVec I$
Assertion	frlmup2	$⊢ φ \to E (U (Y)) = A (Y)$

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.y	$⊢ φ \to Y \in I$
11		frlmup.u	$⊢ U = R unitVec I$
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	11 1 2	uvcff	$⊢ (R \in Ring \land I \in X) \to U : I ⟶ B$
17	15 7 16	syl2anc	$⊢ φ \to U : I ⟶ B$
18	17 10	ffvelcdmd	$⊢ φ \to U (Y) \in B$
19		oveq1	$⊢ x = U (Y) \to x {\underset{˙}{\cdot}}_{f} A = U (Y) {\underset{˙}{\cdot}}_{f} A$
20	19	oveq2d	$⊢ x = U (Y) \to \sum_{T} (x {\underset{˙}{\cdot}}_{f} A) = \sum_{T} (U (Y) {\underset{˙}{\cdot}}_{f} A)$
21		ovex	$⊢ \sum_{T} (U (Y) {\underset{˙}{\cdot}}_{f} A) \in V$
22	20 5 21	fvmpt	$⊢ U (Y) \in B \to E (U (Y)) = \sum_{T} (U (Y) {\underset{˙}{\cdot}}_{f} A)$
23	18 22	syl	$⊢ φ \to E (U (Y)) = \sum_{T} (U (Y) {\underset{˙}{\cdot}}_{f} A)$
24		eqid	$⊢ 0_{T} = 0_{T}$
25		lmodcmn	$⊢ T \in LMod \to T \in CMnd$
26		cmnmnd	$⊢ T \in CMnd \to T \in Mnd$
27	6 25 26	3syl	$⊢ φ \to T \in Mnd$
28		eqid	$⊢ {Base}_{Scalar (T)} = {Base}_{Scalar (T)}$
29		eqid	$⊢ {Base}_{R} = {Base}_{R}$
30	1 29 2	frlmbasf	$⊢ (I \in X \land U (Y) \in B) \to U (Y) : I ⟶ {Base}_{R}$
31	7 18 30	syl2anc	$⊢ φ \to U (Y) : I ⟶ {Base}_{R}$
32	8	fveq2d	$⊢ φ \to {Base}_{R} = {Base}_{Scalar (T)}$
33	32	feq3d	$⊢ φ \to (U (Y) : I ⟶ {Base}_{R} \leftrightarrow U (Y) : I ⟶ {Base}_{Scalar (T)})$
34	31 33	mpbid	$⊢ φ \to U (Y) : I ⟶ {Base}_{Scalar (T)}$
35	12 28 4 3 6 34 9 7	lcomf	$⊢ φ \to (U (Y) {\underset{˙}{\cdot}}_{f} A) : I ⟶ C$
36	31	ffnd	$⊢ φ \to U (Y) Fn I$
37	36	adantr	$⊢ (φ \land x \in (I ∖ \{Y\})) \to U (Y) Fn I$
38	9	ffnd	$⊢ φ \to A Fn I$
39	38	adantr	$⊢ (φ \land x \in (I ∖ \{Y\})) \to A Fn I$
40	7	adantr	$⊢ (φ \land x \in (I ∖ \{Y\})) \to I \in X$
41		eldifi	$⊢ x \in (I ∖ \{Y\}) \to x \in I$
42	41	adantl	$⊢ (φ \land x \in (I ∖ \{Y\})) \to x \in I$
43		fnfvof	$⊢ ((U (Y) Fn I \land A Fn I) \land (I \in X \land x \in I)) \to (U (Y) {\underset{˙}{\cdot}}_{f} A) (x) = U (Y) (x) \underset{˙}{\cdot} A (x)$
44	37 39 40 42 43	syl22anc	$⊢ (φ \land x \in (I ∖ \{Y\})) \to (U (Y) {\underset{˙}{\cdot}}_{f} A) (x) = U (Y) (x) \underset{˙}{\cdot} A (x)$
45	15	adantr	$⊢ (φ \land x \in (I ∖ \{Y\})) \to R \in Ring$
46	10	adantr	$⊢ (φ \land x \in (I ∖ \{Y\})) \to Y \in I$
47		eldifsni	$⊢ x \in (I ∖ \{Y\}) \to x \neq Y$
48	47	necomd	$⊢ x \in (I ∖ \{Y\}) \to Y \neq x$
49	48	adantl	$⊢ (φ \land x \in (I ∖ \{Y\})) \to Y \neq x$
50		eqid	$⊢ 0_{R} = 0_{R}$
51	11 45 40 46 42 49 50	uvcvv0	$⊢ (φ \land x \in (I ∖ \{Y\})) \to U (Y) (x) = 0_{R}$
52	8	fveq2d	$⊢ φ \to 0_{R} = 0_{Scalar (T)}$
53	52	adantr	$⊢ (φ \land x \in (I ∖ \{Y\})) \to 0_{R} = 0_{Scalar (T)}$
54	51 53	eqtrd	$⊢ (φ \land x \in (I ∖ \{Y\})) \to U (Y) (x) = 0_{Scalar (T)}$
55	54	oveq1d	$⊢ (φ \land x \in (I ∖ \{Y\})) \to U (Y) (x) \underset{˙}{\cdot} A (x) = 0_{Scalar (T)} \underset{˙}{\cdot} A (x)$
56	6	adantr	$⊢ (φ \land x \in (I ∖ \{Y\})) \to T \in LMod$
57		ffvelcdm	$⊢ (A : I ⟶ C \land x \in I) \to A (x) \in C$
58	9 41 57	syl2an	$⊢ (φ \land x \in (I ∖ \{Y\})) \to A (x) \in C$
59		eqid	$⊢ 0_{Scalar (T)} = 0_{Scalar (T)}$
60	3 12 4 59 24	lmod0vs	$⊢ (T \in LMod \land A (x) \in C) \to 0_{Scalar (T)} \underset{˙}{\cdot} A (x) = 0_{T}$
61	56 58 60	syl2anc	$⊢ (φ \land x \in (I ∖ \{Y\})) \to 0_{Scalar (T)} \underset{˙}{\cdot} A (x) = 0_{T}$
62	44 55 61	3eqtrd	$⊢ (φ \land x \in (I ∖ \{Y\})) \to (U (Y) {\underset{˙}{\cdot}}_{f} A) (x) = 0_{T}$
63	35 62	suppss	$⊢ φ \to (U (Y) {\underset{˙}{\cdot}}_{f} A) supp 0_{T} \subseteq \{Y\}$
64	3 24 27 7 10 35 63	gsumpt	$⊢ φ \to \sum_{T} (U (Y) {\underset{˙}{\cdot}}_{f} A) = (U (Y) {\underset{˙}{\cdot}}_{f} A) (Y)$
65		fnfvof	$⊢ ((U (Y) Fn I \land A Fn I) \land (I \in X \land Y \in I)) \to (U (Y) {\underset{˙}{\cdot}}_{f} A) (Y) = U (Y) (Y) \underset{˙}{\cdot} A (Y)$
66	36 38 7 10 65	syl22anc	$⊢ φ \to (U (Y) {\underset{˙}{\cdot}}_{f} A) (Y) = U (Y) (Y) \underset{˙}{\cdot} A (Y)$
67		eqid	$⊢ 1_{R} = 1_{R}$
68	11 15 7 10 67	uvcvv1	$⊢ φ \to U (Y) (Y) = 1_{R}$
69	8	fveq2d	$⊢ φ \to 1_{R} = 1_{Scalar (T)}$
70	68 69	eqtrd	$⊢ φ \to U (Y) (Y) = 1_{Scalar (T)}$
71	70	oveq1d	$⊢ φ \to U (Y) (Y) \underset{˙}{\cdot} A (Y) = 1_{Scalar (T)} \underset{˙}{\cdot} A (Y)$
72	9 10	ffvelcdmd	$⊢ φ \to A (Y) \in C$
73		eqid	$⊢ 1_{Scalar (T)} = 1_{Scalar (T)}$
74	3 12 4 73	lmodvs1	$⊢ (T \in LMod \land A (Y) \in C) \to 1_{Scalar (T)} \underset{˙}{\cdot} A (Y) = A (Y)$
75	6 72 74	syl2anc	$⊢ φ \to 1_{Scalar (T)} \underset{˙}{\cdot} A (Y) = A (Y)$
76	66 71 75	3eqtrd	$⊢ φ \to (U (Y) {\underset{˙}{\cdot}}_{f} A) (Y) = A (Y)$
77	23 64 76	3eqtrd	$⊢ φ \to E (U (Y)) = A (Y)$

Metamath Proof Explorer

Theorem frlmup2

Proof