uvcresum

Description: Any element of a free module can be expressed as a finite linear combination of unit vectors. (Contributed by Stefan O'Rear, 3-Feb-2015) (Proof shortened by Mario Carneiro, 5-Jul-2015)

	Ref	Expression
Hypotheses	uvcresum.u	$⊢ U = R unitVec I$
	uvcresum.y	$⊢ Y = R freeLMod I$
	uvcresum.b	$⊢ B = {Base}_{Y}$
	uvcresum.v	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
Assertion	uvcresum	$⊢ (R \in Ring \land I \in W \land X \in B) \to X = \sum_{Y} (X {\underset{˙}{\cdot}}_{f} U)$

Proof

Step	Hyp	Ref	Expression
1		uvcresum.u	$⊢ U = R unitVec I$
2		uvcresum.y	$⊢ Y = R freeLMod I$
3		uvcresum.b	$⊢ B = {Base}_{Y}$
4		uvcresum.v	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	2 5 3	frlmbasf	$⊢ (I \in W \land X \in B) \to X : I ⟶ {Base}_{R}$
7	6	3adant1	$⊢ (R \in Ring \land I \in W \land X \in B) \to X : I ⟶ {Base}_{R}$
8	7	feqmptd	$⊢ (R \in Ring \land I \in W \land X \in B) \to X = (a \in I ⟼ X (a))$
9		eqid	$⊢ 0_{R} = 0_{R}$
10		simpl1	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to R \in Ring$
11		ringmnd	$⊢ R \in Ring \to R \in Mnd$
12	10 11	syl	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to R \in Mnd$
13		simpl2	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to I \in W$
14		simpr	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to a \in I$
15		simpl2	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to I \in W$
16	7	ffvelrnda	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to X (b) \in {Base}_{R}$
17	1 2 3	uvcff	$⊢ (R \in Ring \land I \in W) \to U : I ⟶ B$
18	17	3adant3	$⊢ (R \in Ring \land I \in W \land X \in B) \to U : I ⟶ B$
19	18	ffvelrnda	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to U (b) \in B$
20		eqid	$⊢ \cdot_{R} = \cdot_{R}$
21	2 3 5 15 16 19 4 20	frlmvscafval	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to X (b) \underset{˙}{\cdot} U (b) = (I \times \{X (b)\}) {\cdot_{R}}_{f} U (b)$
22	16	adantr	$⊢ (((R \in Ring \land I \in W \land X \in B) \land b \in I) \land a \in I) \to X (b) \in {Base}_{R}$
23	2 5 3	frlmbasf	$⊢ (I \in W \land U (b) \in B) \to U (b) : I ⟶ {Base}_{R}$
24	15 19 23	syl2anc	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to U (b) : I ⟶ {Base}_{R}$
25	24	ffvelrnda	$⊢ (((R \in Ring \land I \in W \land X \in B) \land b \in I) \land a \in I) \to U (b) (a) \in {Base}_{R}$
26		fconstmpt	$⊢ I \times \{X (b)\} = (a \in I ⟼ X (b))$
27	26	a1i	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to I \times \{X (b)\} = (a \in I ⟼ X (b))$
28	24	feqmptd	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to U (b) = (a \in I ⟼ U (b) (a))$
29	15 22 25 27 28	offval2	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to (I \times \{X (b)\}) {\cdot_{R}}_{f} U (b) = (a \in I ⟼ X (b) \cdot_{R} U (b) (a))$
30	21 29	eqtrd	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to X (b) \underset{˙}{\cdot} U (b) = (a \in I ⟼ X (b) \cdot_{R} U (b) (a))$
31	2	frlmlmod	$⊢ (R \in Ring \land I \in W) \to Y \in LMod$
32	31	3adant3	$⊢ (R \in Ring \land I \in W \land X \in B) \to Y \in LMod$
33	32	adantr	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to Y \in LMod$
34	2	frlmsca	$⊢ (R \in Ring \land I \in W) \to R = Scalar (Y)$
35	34	3adant3	$⊢ (R \in Ring \land I \in W \land X \in B) \to R = Scalar (Y)$
36	35	fveq2d	$⊢ (R \in Ring \land I \in W \land X \in B) \to {Base}_{R} = {Base}_{Scalar (Y)}$
37	36	adantr	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to {Base}_{R} = {Base}_{Scalar (Y)}$
38	16 37	eleqtrd	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to X (b) \in {Base}_{Scalar (Y)}$
39		eqid	$⊢ Scalar (Y) = Scalar (Y)$
40		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
41	3 39 4 40	lmodvscl	$⊢ (Y \in LMod \land X (b) \in {Base}_{Scalar (Y)} \land U (b) \in B) \to X (b) \underset{˙}{\cdot} U (b) \in B$
42	33 38 19 41	syl3anc	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to X (b) \underset{˙}{\cdot} U (b) \in B$
43	30 42	eqeltrrd	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to (a \in I ⟼ X (b) \cdot_{R} U (b) (a)) \in B$
44	2 5 3	frlmbasf	$⊢ (I \in W \land (a \in I ⟼ X (b) \cdot_{R} U (b) (a)) \in B) \to (a \in I ⟼ X (b) \cdot_{R} U (b) (a)) : I ⟶ {Base}_{R}$
45	15 43 44	syl2anc	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in I) \to (a \in I ⟼ X (b) \cdot_{R} U (b) (a)) : I ⟶ {Base}_{R}$
46	45	fvmptelrn	$⊢ (((R \in Ring \land I \in W \land X \in B) \land b \in I) \land a \in I) \to X (b) \cdot_{R} U (b) (a) \in {Base}_{R}$
47	46	an32s	$⊢ (((R \in Ring \land I \in W \land X \in B) \land a \in I) \land b \in I) \to X (b) \cdot_{R} U (b) (a) \in {Base}_{R}$
48	47	fmpttd	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to (b \in I ⟼ X (b) \cdot_{R} U (b) (a)) : I ⟶ {Base}_{R}$
49	10	3ad2ant1	$⊢ (((R \in Ring \land I \in W \land X \in B) \land a \in I) \land b \in I \land b \neq a) \to R \in Ring$
50	13	3ad2ant1	$⊢ (((R \in Ring \land I \in W \land X \in B) \land a \in I) \land b \in I \land b \neq a) \to I \in W$
51		simp2	$⊢ (((R \in Ring \land I \in W \land X \in B) \land a \in I) \land b \in I \land b \neq a) \to b \in I$
52	14	3ad2ant1	$⊢ (((R \in Ring \land I \in W \land X \in B) \land a \in I) \land b \in I \land b \neq a) \to a \in I$
53		simp3	$⊢ (((R \in Ring \land I \in W \land X \in B) \land a \in I) \land b \in I \land b \neq a) \to b \neq a$
54	1 49 50 51 52 53 9	uvcvv0	$⊢ (((R \in Ring \land I \in W \land X \in B) \land a \in I) \land b \in I \land b \neq a) \to U (b) (a) = 0_{R}$
55	54	oveq2d	$⊢ (((R \in Ring \land I \in W \land X \in B) \land a \in I) \land b \in I \land b \neq a) \to X (b) \cdot_{R} U (b) (a) = X (b) \cdot_{R} 0_{R}$
56	16	adantlr	$⊢ (((R \in Ring \land I \in W \land X \in B) \land a \in I) \land b \in I) \to X (b) \in {Base}_{R}$
57	56	3adant3	$⊢ (((R \in Ring \land I \in W \land X \in B) \land a \in I) \land b \in I \land b \neq a) \to X (b) \in {Base}_{R}$
58	5 20 9	ringrz	$⊢ (R \in Ring \land X (b) \in {Base}_{R}) \to X (b) \cdot_{R} 0_{R} = 0_{R}$
59	49 57 58	syl2anc	$⊢ (((R \in Ring \land I \in W \land X \in B) \land a \in I) \land b \in I \land b \neq a) \to X (b) \cdot_{R} 0_{R} = 0_{R}$
60	55 59	eqtrd	$⊢ (((R \in Ring \land I \in W \land X \in B) \land a \in I) \land b \in I \land b \neq a) \to X (b) \cdot_{R} U (b) (a) = 0_{R}$
61	60 13	suppsssn	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to (b \in I ⟼ X (b) \cdot_{R} U (b) (a)) supp 0_{R} \subseteq \{a\}$
62	5 9 12 13 14 48 61	gsumpt	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to \underset{b \in I}{\sum_{R}} (X (b) \cdot_{R} U (b) (a)) = (b \in I ⟼ X (b) \cdot_{R} U (b) (a)) (a)$
63		fveq2	$⊢ b = a \to X (b) = X (a)$
64		fveq2	$⊢ b = a \to U (b) = U (a)$
65	64	fveq1d	$⊢ b = a \to U (b) (a) = U (a) (a)$
66	63 65	oveq12d	$⊢ b = a \to X (b) \cdot_{R} U (b) (a) = X (a) \cdot_{R} U (a) (a)$
67		eqid	$⊢ (b \in I ⟼ X (b) \cdot_{R} U (b) (a)) = (b \in I ⟼ X (b) \cdot_{R} U (b) (a))$
68		ovex	$⊢ X (a) \cdot_{R} U (a) (a) \in V$
69	66 67 68	fvmpt	$⊢ a \in I \to (b \in I ⟼ X (b) \cdot_{R} U (b) (a)) (a) = X (a) \cdot_{R} U (a) (a)$
70	69	adantl	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to (b \in I ⟼ X (b) \cdot_{R} U (b) (a)) (a) = X (a) \cdot_{R} U (a) (a)$
71		eqid	$⊢ 1_{R} = 1_{R}$
72	1 10 13 14 71	uvcvv1	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to U (a) (a) = 1_{R}$
73	72	oveq2d	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to X (a) \cdot_{R} U (a) (a) = X (a) \cdot_{R} 1_{R}$
74	7	ffvelrnda	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to X (a) \in {Base}_{R}$
75	5 20 71	ringridm	$⊢ (R \in Ring \land X (a) \in {Base}_{R}) \to X (a) \cdot_{R} 1_{R} = X (a)$
76	10 74 75	syl2anc	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to X (a) \cdot_{R} 1_{R} = X (a)$
77	73 76	eqtrd	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to X (a) \cdot_{R} U (a) (a) = X (a)$
78	70 77	eqtrd	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to (b \in I ⟼ X (b) \cdot_{R} U (b) (a)) (a) = X (a)$
79	62 78	eqtrd	$⊢ ((R \in Ring \land I \in W \land X \in B) \land a \in I) \to \underset{b \in I}{\sum_{R}} (X (b) \cdot_{R} U (b) (a)) = X (a)$
80	79	mpteq2dva	$⊢ (R \in Ring \land I \in W \land X \in B) \to (a \in I ⟼ \underset{b \in I}{\sum_{R}} (X (b) \cdot_{R} U (b) (a))) = (a \in I ⟼ X (a))$
81	8 80	eqtr4d	$⊢ (R \in Ring \land I \in W \land X \in B) \to X = (a \in I ⟼ \underset{b \in I}{\sum_{R}} (X (b) \cdot_{R} U (b) (a)))$
82		eqid	$⊢ 0_{Y} = 0_{Y}$
83		simp2	$⊢ (R \in Ring \land I \in W \land X \in B) \to I \in W$
84		simp1	$⊢ (R \in Ring \land I \in W \land X \in B) \to R \in Ring$
85		mptexg	$⊢ I \in W \to (b \in I ⟼ (a \in I ⟼ X (b) \cdot_{R} U (b) (a))) \in V$
86	85	3ad2ant2	$⊢ (R \in Ring \land I \in W \land X \in B) \to (b \in I ⟼ (a \in I ⟼ X (b) \cdot_{R} U (b) (a))) \in V$
87		funmpt	$⊢ Fun (b \in I ⟼ (a \in I ⟼ X (b) \cdot_{R} U (b) (a)))$
88	87	a1i	$⊢ (R \in Ring \land I \in W \land X \in B) \to Fun (b \in I ⟼ (a \in I ⟼ X (b) \cdot_{R} U (b) (a)))$
89		fvexd	$⊢ (R \in Ring \land I \in W \land X \in B) \to 0_{Y} \in V$
90	2 9 3	frlmbasfsupp	$⊢ (I \in W \land X \in B) \to {finSupp}_{0_{R}} (X)$
91	90	3adant1	$⊢ (R \in Ring \land I \in W \land X \in B) \to {finSupp}_{0_{R}} (X)$
92	91	fsuppimpd	$⊢ (R \in Ring \land I \in W \land X \in B) \to X supp 0_{R} \in Fin$
93	35	eqcomd	$⊢ (R \in Ring \land I \in W \land X \in B) \to Scalar (Y) = R$
94	93	fveq2d	$⊢ (R \in Ring \land I \in W \land X \in B) \to 0_{Scalar (Y)} = 0_{R}$
95	94	oveq2d	$⊢ (R \in Ring \land I \in W \land X \in B) \to X supp 0_{Scalar (Y)} = X supp 0_{R}$
96		ssid	$⊢ X supp 0_{R} \subseteq X supp 0_{R}$
97	95 96	eqsstrdi	$⊢ (R \in Ring \land I \in W \land X \in B) \to X supp 0_{Scalar (Y)} \subseteq X supp 0_{R}$
98		fvexd	$⊢ (R \in Ring \land I \in W \land X \in B) \to 0_{Scalar (Y)} \in V$
99	7 97 83 98	suppssr	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in (I ∖ {supp}_{0_{R}} (X))) \to X (b) = 0_{Scalar (Y)}$
100	99	oveq1d	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in (I ∖ {supp}_{0_{R}} (X))) \to X (b) \underset{˙}{\cdot} U (b) = 0_{Scalar (Y)} \underset{˙}{\cdot} U (b)$
101		eldifi	$⊢ b \in (I ∖ {supp}_{0_{R}} (X)) \to b \in I$
102	101 30	sylan2	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in (I ∖ {supp}_{0_{R}} (X))) \to X (b) \underset{˙}{\cdot} U (b) = (a \in I ⟼ X (b) \cdot_{R} U (b) (a))$
103	32	adantr	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in (I ∖ {supp}_{0_{R}} (X))) \to Y \in LMod$
104	101 19	sylan2	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in (I ∖ {supp}_{0_{R}} (X))) \to U (b) \in B$
105		eqid	$⊢ 0_{Scalar (Y)} = 0_{Scalar (Y)}$
106	3 39 4 105 82	lmod0vs	$⊢ (Y \in LMod \land U (b) \in B) \to 0_{Scalar (Y)} \underset{˙}{\cdot} U (b) = 0_{Y}$
107	103 104 106	syl2anc	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in (I ∖ {supp}_{0_{R}} (X))) \to 0_{Scalar (Y)} \underset{˙}{\cdot} U (b) = 0_{Y}$
108	100 102 107	3eqtr3d	$⊢ ((R \in Ring \land I \in W \land X \in B) \land b \in (I ∖ {supp}_{0_{R}} (X))) \to (a \in I ⟼ X (b) \cdot_{R} U (b) (a)) = 0_{Y}$
109	108 83	suppss2	$⊢ (R \in Ring \land I \in W \land X \in B) \to (b \in I ⟼ (a \in I ⟼ X (b) \cdot_{R} U (b) (a))) supp 0_{Y} \subseteq X supp 0_{R}$
110		suppssfifsupp	$⊢ (((b \in I ⟼ (a \in I ⟼ X (b) \cdot_{R} U (b) (a))) \in V \land Fun (b \in I ⟼ (a \in I ⟼ X (b) \cdot_{R} U (b) (a))) \land 0_{Y} \in V) \land (X supp 0_{R} \in Fin \land (b \in I ⟼ (a \in I ⟼ X (b) \cdot_{R} U (b) (a))) supp 0_{Y} \subseteq X supp 0_{R})) \to {finSupp}_{0_{Y}} ((b \in I ⟼ (a \in I ⟼ X (b) \cdot_{R} U (b) (a))))$
111	86 88 89 92 109 110	syl32anc	$⊢ (R \in Ring \land I \in W \land X \in B) \to {finSupp}_{0_{Y}} ((b \in I ⟼ (a \in I ⟼ X (b) \cdot_{R} U (b) (a))))$
112	2 3 82 83 83 84 43 111	frlmgsum	$⊢ (R \in Ring \land I \in W \land X \in B) \to \underset{b \in I}{\sum_{Y}} (a \in I ⟼ X (b) \cdot_{R} U (b) (a)) = (a \in I ⟼ \underset{b \in I}{\sum_{R}} (X (b) \cdot_{R} U (b) (a)))$
113	81 112	eqtr4d	$⊢ (R \in Ring \land I \in W \land X \in B) \to X = \underset{b \in I}{\sum_{Y}} (a \in I ⟼ X (b) \cdot_{R} U (b) (a))$
114	7	feqmptd	$⊢ (R \in Ring \land I \in W \land X \in B) \to X = (b \in I ⟼ X (b))$
115	18	feqmptd	$⊢ (R \in Ring \land I \in W \land X \in B) \to U = (b \in I ⟼ U (b))$
116	83 16 19 114 115	offval2	$⊢ (R \in Ring \land I \in W \land X \in B) \to X {\underset{˙}{\cdot}}_{f} U = (b \in I ⟼ X (b) \underset{˙}{\cdot} U (b))$
117	30	mpteq2dva	$⊢ (R \in Ring \land I \in W \land X \in B) \to (b \in I ⟼ X (b) \underset{˙}{\cdot} U (b)) = (b \in I ⟼ (a \in I ⟼ X (b) \cdot_{R} U (b) (a)))$
118	116 117	eqtrd	$⊢ (R \in Ring \land I \in W \land X \in B) \to X {\underset{˙}{\cdot}}_{f} U = (b \in I ⟼ (a \in I ⟼ X (b) \cdot_{R} U (b) (a)))$
119	118	oveq2d	$⊢ (R \in Ring \land I \in W \land X \in B) \to \sum_{Y} (X {\underset{˙}{\cdot}}_{f} U) = \underset{b \in I}{\sum_{Y}} (a \in I ⟼ X (b) \cdot_{R} U (b) (a))$
120	113 119	eqtr4d	$⊢ (R \in Ring \land I \in W \land X \in B) \to X = \sum_{Y} (X {\underset{˙}{\cdot}}_{f} U)$

Metamath Proof Explorer

Theorem uvcresum

Proof