fedgmullem2

	Ref	Expression
Hypotheses	fedgmul.a	$⊢ A = subringAlg (E) (V)$
	fedgmul.b	$⊢ B = subringAlg (E) (U)$
	fedgmul.c	$⊢ C = subringAlg (F) (V)$
	fedgmul.f	$⊢ F = E ↾_{𝑠} U$
	fedgmul.k	$⊢ K = E ↾_{𝑠} V$
	fedgmul.1	$⊢ φ \to E \in DivRing$
	fedgmul.2	$⊢ φ \to F \in DivRing$
	fedgmul.3	$⊢ φ \to K \in DivRing$
	fedgmul.4	$⊢ φ \to U \in SubRing (E)$
	fedgmul.5	$⊢ φ \to V \in SubRing (F)$
	fedgmullem.d	$⊢ D = (j \in Y, i \in X ⟼ i \cdot_{E} j)$
	fedgmullem.h	$⊢ H = (j \in Y, i \in X ⟼ G (j) (i))$
	fedgmullem.x	$⊢ φ \to X \in LBasis (C)$
	fedgmullem.y	$⊢ φ \to Y \in LBasis (B)$
	fedgmullem2.1	$⊢ φ \to W \in {Base}_{(Scalar (A) freeLMod (Y \times X))}$
	fedgmullem2.2	$⊢ φ \to \sum_{A} (W {\cdot_{A}}_{f} D) = 0_{A}$
Assertion	fedgmullem2	$⊢ φ \to W = (Y \times X) \times \{0_{Scalar (A)}\}$

Proof

Step	Hyp	Ref	Expression
1		fedgmul.a	$⊢ A = subringAlg (E) (V)$
2		fedgmul.b	$⊢ B = subringAlg (E) (U)$
3		fedgmul.c	$⊢ C = subringAlg (F) (V)$
4		fedgmul.f	$⊢ F = E ↾_{𝑠} U$
5		fedgmul.k	$⊢ K = E ↾_{𝑠} V$
6		fedgmul.1	$⊢ φ \to E \in DivRing$
7		fedgmul.2	$⊢ φ \to F \in DivRing$
8		fedgmul.3	$⊢ φ \to K \in DivRing$
9		fedgmul.4	$⊢ φ \to U \in SubRing (E)$
10		fedgmul.5	$⊢ φ \to V \in SubRing (F)$
11		fedgmullem.d	$⊢ D = (j \in Y, i \in X ⟼ i \cdot_{E} j)$
12		fedgmullem.h	$⊢ H = (j \in Y, i \in X ⟼ G (j) (i))$
13		fedgmullem.x	$⊢ φ \to X \in LBasis (C)$
14		fedgmullem.y	$⊢ φ \to Y \in LBasis (B)$
15		fedgmullem2.1	$⊢ φ \to W \in {Base}_{(Scalar (A) freeLMod (Y \times X))}$
16		fedgmullem2.2	$⊢ φ \to \sum_{A} (W {\cdot_{A}}_{f} D) = 0_{A}$
17	4	subsubrg	$⊢ U \in SubRing (E) \to (V \in SubRing (F) \leftrightarrow (V \in SubRing (E) \land V \subseteq U))$
18	17	biimpa	$⊢ (U \in SubRing (E) \land V \in SubRing (F)) \to (V \in SubRing (E) \land V \subseteq U)$
19	9 10 18	syl2anc	$⊢ φ \to (V \in SubRing (E) \land V \subseteq U)$
20	19	simpld	$⊢ φ \to V \in SubRing (E)$
21	1 5	sralvec	$⊢ (E \in DivRing \land K \in DivRing \land V \in SubRing (E)) \to A \in LVec$
22	6 8 20 21	syl3anc	$⊢ φ \to A \in LVec$
23		lveclmod	$⊢ A \in LVec \to A \in LMod$
24	22 23	syl	$⊢ φ \to A \in LMod$
25		eqid	$⊢ {Base}_{C} = {Base}_{C}$
26		eqid	$⊢ LBasis (C) = LBasis (C)$
27	25 26	lbsss	$⊢ X \in LBasis (C) \to X \subseteq {Base}_{C}$
28	13 27	syl	$⊢ φ \to X \subseteq {Base}_{C}$
29		eqid	$⊢ {Base}_{E} = {Base}_{E}$
30	29	subrgss	$⊢ U \in SubRing (E) \to U \subseteq {Base}_{E}$
31	9 30	syl	$⊢ φ \to U \subseteq {Base}_{E}$
32	4 29	ressbas2	$⊢ U \subseteq {Base}_{E} \to U = {Base}_{F}$
33	31 32	syl	$⊢ φ \to U = {Base}_{F}$
34	3	a1i	$⊢ φ \to C = subringAlg (F) (V)$
35		eqid	$⊢ {Base}_{F} = {Base}_{F}$
36	35	subrgss	$⊢ V \in SubRing (F) \to V \subseteq {Base}_{F}$
37	10 36	syl	$⊢ φ \to V \subseteq {Base}_{F}$
38	34 37	srabase	$⊢ φ \to {Base}_{F} = {Base}_{C}$
39	33 38	eqtrd	$⊢ φ \to U = {Base}_{C}$
40	39 31	eqsstrrd	$⊢ φ \to {Base}_{C} \subseteq {Base}_{E}$
41	1	a1i	$⊢ φ \to A = subringAlg (E) (V)$
42	29	subrgss	$⊢ V \in SubRing (E) \to V \subseteq {Base}_{E}$
43	20 42	syl	$⊢ φ \to V \subseteq {Base}_{E}$
44	41 43	srabase	$⊢ φ \to {Base}_{E} = {Base}_{A}$
45	40 44	sseqtrd	$⊢ φ \to {Base}_{C} \subseteq {Base}_{A}$
46	28 45	sstrd	$⊢ φ \to X \subseteq {Base}_{A}$
47	41 9 43	srasubrg	$⊢ φ \to U \in SubRing (A)$
48		subrgsubg	$⊢ U \in SubRing (A) \to U \in SubGrp (A)$
49	47 48	syl	$⊢ φ \to U \in SubGrp (A)$
50	1 6 20	drgextvsca	$⊢ φ \to \cdot_{E} = \cdot_{A}$
51	50	oveqdr	$⊢ (φ \land (x \in {Base}_{Scalar (A)} \land y \in U)) \to x \cdot_{E} y = x \cdot_{A} y$
52	9	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (A)} \land y \in U)) \to U \in SubRing (E)$
53	19	simprd	$⊢ φ \to V \subseteq U$
54	53	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (A)} \land y \in U)) \to V \subseteq U$
55		simprl	$⊢ (φ \land (x \in {Base}_{Scalar (A)} \land y \in U)) \to x \in {Base}_{Scalar (A)}$
56		ressabs	$⊢ (U \in SubRing (E) \land V \subseteq U) \to (E ↾_{𝑠} U) ↾_{𝑠} V = E ↾_{𝑠} V$
57	9 53 56	syl2anc	$⊢ φ \to (E ↾_{𝑠} U) ↾_{𝑠} V = E ↾_{𝑠} V$
58	4	oveq1i	$⊢ F ↾_{𝑠} V = (E ↾_{𝑠} U) ↾_{𝑠} V$
59	57 58 5	3eqtr4g	$⊢ φ \to F ↾_{𝑠} V = K$
60	34 37	srasca	$⊢ φ \to F ↾_{𝑠} V = Scalar (C)$
61	59 60	eqtr3d	$⊢ φ \to K = Scalar (C)$
62	61	fveq2d	$⊢ φ \to {Base}_{K} = {Base}_{Scalar (C)}$
63	5 29	ressbas2	$⊢ V \subseteq {Base}_{E} \to V = {Base}_{K}$
64	43 63	syl	$⊢ φ \to V = {Base}_{K}$
65	41 43	srasca	$⊢ φ \to E ↾_{𝑠} V = Scalar (A)$
66	5 65	syl5eq	$⊢ φ \to K = Scalar (A)$
67	59 60 66	3eqtr3rd	$⊢ φ \to Scalar (A) = Scalar (C)$
68	67	fveq2d	$⊢ φ \to {Base}_{Scalar (A)} = {Base}_{Scalar (C)}$
69	62 64 68	3eqtr4d	$⊢ φ \to V = {Base}_{Scalar (A)}$
70	69	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (A)} \land y \in U)) \to V = {Base}_{Scalar (A)}$
71	55 70	eleqtrrd	$⊢ (φ \land (x \in {Base}_{Scalar (A)} \land y \in U)) \to x \in V$
72	54 71	sseldd	$⊢ (φ \land (x \in {Base}_{Scalar (A)} \land y \in U)) \to x \in U$
73		simprr	$⊢ (φ \land (x \in {Base}_{Scalar (A)} \land y \in U)) \to y \in U$
74		eqid	$⊢ \cdot_{E} = \cdot_{E}$
75	74	subrgmcl	$⊢ (U \in SubRing (E) \land x \in U \land y \in U) \to x \cdot_{E} y \in U$
76	52 72 73 75	syl3anc	$⊢ (φ \land (x \in {Base}_{Scalar (A)} \land y \in U)) \to x \cdot_{E} y \in U$
77	51 76	eqeltrrd	$⊢ (φ \land (x \in {Base}_{Scalar (A)} \land y \in U)) \to x \cdot_{A} y \in U$
78	77	ralrimivva	$⊢ φ \to \forall x \in {Base}_{Scalar (A)} \forall y \in U x \cdot_{A} y \in U$
79		eqid	$⊢ Scalar (A) = Scalar (A)$
80		eqid	$⊢ {Base}_{Scalar (A)} = {Base}_{Scalar (A)}$
81		eqid	$⊢ {Base}_{A} = {Base}_{A}$
82		eqid	$⊢ \cdot_{A} = \cdot_{A}$
83		eqid	$⊢ LSubSp (A) = LSubSp (A)$
84	79 80 81 82 83	islss4	$⊢ A \in LMod \to (U \in LSubSp (A) \leftrightarrow (U \in SubGrp (A) \land \forall x \in {Base}_{Scalar (A)} \forall y \in U x \cdot_{A} y \in U))$
85	84	biimpar	$⊢ (A \in LMod \land (U \in SubGrp (A) \land \forall x \in {Base}_{Scalar (A)} \forall y \in U x \cdot_{A} y \in U)) \to U \in LSubSp (A)$
86	24 49 78 85	syl12anc	$⊢ φ \to U \in LSubSp (A)$
87	28 39	sseqtrrd	$⊢ φ \to X \subseteq U$
88	26	lbslinds	$⊢ LBasis (C) \subseteq LIndS (C)$
89	88 13	sseldi	$⊢ φ \to X \in LIndS (C)$
90	31 44	sseqtrd	$⊢ φ \to U \subseteq {Base}_{A}$
91		eqid	$⊢ A ↾_{𝑠} U = A ↾_{𝑠} U$
92	91 81	ressbas2	$⊢ U \subseteq {Base}_{A} \to U = {Base}_{(A ↾_{𝑠} U)}$
93	90 92	syl	$⊢ φ \to U = {Base}_{(A ↾_{𝑠} U)}$
94	33 93 38	3eqtr3rd	$⊢ φ \to {Base}_{C} = {Base}_{(A ↾_{𝑠} U)}$
95	91 79	resssca	$⊢ U \in SubRing (E) \to Scalar (A) = Scalar (A ↾_{𝑠} U)$
96	9 95	syl	$⊢ φ \to Scalar (A) = Scalar (A ↾_{𝑠} U)$
97	67 96	eqtr3d	$⊢ φ \to Scalar (C) = Scalar (A ↾_{𝑠} U)$
98	97	fveq2d	$⊢ φ \to {Base}_{Scalar (C)} = {Base}_{Scalar (A ↾_{𝑠} U)}$
99	97	fveq2d	$⊢ φ \to 0_{Scalar (C)} = 0_{Scalar (A ↾_{𝑠} U)}$
100		eqid	$⊢ +_{E} = +_{E}$
101	4 100	ressplusg	$⊢ U \in SubRing (E) \to +_{E} = +_{F}$
102	9 101	syl	$⊢ φ \to +_{E} = +_{F}$
103	41 43	sraaddg	$⊢ φ \to +_{E} = +_{A}$
104	34 37	sraaddg	$⊢ φ \to +_{F} = +_{C}$
105	102 103 104	3eqtr3rd	$⊢ φ \to +_{C} = +_{A}$
106		eqid	$⊢ +_{A} = +_{A}$
107	91 106	ressplusg	$⊢ U \in SubRing (E) \to +_{A} = +_{(A ↾_{𝑠} U)}$
108	9 107	syl	$⊢ φ \to +_{A} = +_{(A ↾_{𝑠} U)}$
109	105 108	eqtrd	$⊢ φ \to +_{C} = +_{(A ↾_{𝑠} U)}$
110	109	oveqdr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x +_{C} y = x +_{(A ↾_{𝑠} U)} y$
111	59 8	eqeltrd	$⊢ φ \to F ↾_{𝑠} V \in DivRing$
112		eqid	$⊢ F ↾_{𝑠} V = F ↾_{𝑠} V$
113	3 112	sralvec	$⊢ (F \in DivRing \land F ↾_{𝑠} V \in DivRing \land V \in SubRing (F)) \to C \in LVec$
114	7 111 10 113	syl3anc	$⊢ φ \to C \in LVec$
115		lveclmod	$⊢ C \in LVec \to C \in LMod$
116	114 115	syl	$⊢ φ \to C \in LMod$
117		eqid	$⊢ Scalar (C) = Scalar (C)$
118		eqid	$⊢ \cdot_{C} = \cdot_{C}$
119		eqid	$⊢ {Base}_{Scalar (C)} = {Base}_{Scalar (C)}$
120	25 117 118 119	lmodvscl	$⊢ (C \in LMod \land x \in {Base}_{Scalar (C)} \land y \in {Base}_{C}) \to x \cdot_{C} y \in {Base}_{C}$
121	120	3expb	$⊢ (C \in LMod \land (x \in {Base}_{Scalar (C)} \land y \in {Base}_{C})) \to x \cdot_{C} y \in {Base}_{C}$
122	116 121	sylan	$⊢ (φ \land (x \in {Base}_{Scalar (C)} \land y \in {Base}_{C})) \to x \cdot_{C} y \in {Base}_{C}$
123	2 6 9	drgextvsca	$⊢ φ \to \cdot_{E} = \cdot_{B}$
124	50 123	eqtr3d	$⊢ φ \to \cdot_{A} = \cdot_{B}$
125	91 82	ressvsca	$⊢ U \in SubRing (E) \to \cdot_{A} = \cdot_{(A ↾_{𝑠} U)}$
126	9 125	syl	$⊢ φ \to \cdot_{A} = \cdot_{(A ↾_{𝑠} U)}$
127	4 74	ressmulr	$⊢ U \in SubRing (E) \to \cdot_{E} = \cdot_{F}$
128	9 127	syl	$⊢ φ \to \cdot_{E} = \cdot_{F}$
129	3 7 10	drgextvsca	$⊢ φ \to \cdot_{F} = \cdot_{C}$
130	128 123 129	3eqtr3d	$⊢ φ \to \cdot_{B} = \cdot_{C}$
131	124 126 130	3eqtr3rd	$⊢ φ \to \cdot_{C} = \cdot_{(A ↾_{𝑠} U)}$
132	131	oveqdr	$⊢ (φ \land (x \in {Base}_{Scalar (C)} \land y \in {Base}_{C})) \to x \cdot_{C} y = x \cdot_{(A ↾_{𝑠} U)} y$
133		ovexd	$⊢ φ \to A ↾_{𝑠} U \in V$
134	94 98 99 110 122 132 114 133	lindspropd	$⊢ φ \to LIndS (C) = LIndS (A ↾_{𝑠} U)$
135	89 134	eleqtrd	$⊢ φ \to X \in LIndS (A ↾_{𝑠} U)$
136	83 91	lsslinds	$⊢ (A \in LMod \land U \in LSubSp (A) \land X \subseteq U) \to (X \in LIndS (A ↾_{𝑠} U) \leftrightarrow X \in LIndS (A))$
137	136	biimpa	$⊢ ((A \in LMod \land U \in LSubSp (A) \land X \subseteq U) \land X \in LIndS (A ↾_{𝑠} U)) \to X \in LIndS (A)$
138	24 86 87 135 137	syl31anc	$⊢ φ \to X \in LIndS (A)$
139		eqid	$⊢ 0_{A} = 0_{A}$
140		eqid	$⊢ 0_{Scalar (A)} = 0_{Scalar (A)}$
141	81 80 79 82 139 140	islinds5	$⊢ (A \in LMod \land X \subseteq {Base}_{A}) \to (X \in LIndS (A) \leftrightarrow \forall w \in ({Base}_{Scalar (A)}^{X}) (({finSupp}_{0_{Scalar (A)}} (w) \land \underset{i \in X}{\sum_{A}} (w (i) \cdot_{A} i) = 0_{A}) \to w = X \times \{0_{Scalar (A)}\}))$
142	141	biimpa	$⊢ ((A \in LMod \land X \subseteq {Base}_{A}) \land X \in LIndS (A)) \to \forall w \in ({Base}_{Scalar (A)}^{X}) (({finSupp}_{0_{Scalar (A)}} (w) \land \underset{i \in X}{\sum_{A}} (w (i) \cdot_{A} i) = 0_{A}) \to w = X \times \{0_{Scalar (A)}\})$
143	24 46 138 142	syl21anc	$⊢ φ \to \forall w \in ({Base}_{Scalar (A)}^{X}) (({finSupp}_{0_{Scalar (A)}} (w) \land \underset{i \in X}{\sum_{A}} (w (i) \cdot_{A} i) = 0_{A}) \to w = X \times \{0_{Scalar (A)}\})$
144	143	adantr	$⊢ (φ \land j \in Y) \to \forall w \in ({Base}_{Scalar (A)}^{X}) (({finSupp}_{0_{Scalar (A)}} (w) \land \underset{i \in X}{\sum_{A}} (w (i) \cdot_{A} i) = 0_{A}) \to w = X \times \{0_{Scalar (A)}\})$
145		eqid	$⊢ (i \in X ⟼ j W i) = (i \in X ⟼ j W i)$
146		fvexd	$⊢ (φ \land j \in Y) \to 0_{F} \in V$
147	14	adantr	$⊢ (φ \land j \in Y) \to Y \in LBasis (B)$
148	13	adantr	$⊢ (φ \land j \in Y) \to X \in LBasis (C)$
149		fvexd	$⊢ φ \to Scalar (A) \in V$
150	14 13	xpexd	$⊢ φ \to Y \times X \in V$
151		eqid	$⊢ Scalar (A) freeLMod (Y \times X) = Scalar (A) freeLMod (Y \times X)$
152		eqid	$⊢ {Base}_{(Scalar (A) freeLMod (Y \times X))} = {Base}_{(Scalar (A) freeLMod (Y \times X))}$
153	151 80 140 152	frlmelbas	$⊢ (Scalar (A) \in V \land Y \times X \in V) \to (W \in {Base}_{(Scalar (A) freeLMod (Y \times X))} \leftrightarrow (W \in ({Base}_{Scalar (A)}^{(Y \times X)}) \land {finSupp}_{0_{Scalar (A)}} (W)))$
154	149 150 153	syl2anc	$⊢ φ \to (W \in {Base}_{(Scalar (A) freeLMod (Y \times X))} \leftrightarrow (W \in ({Base}_{Scalar (A)}^{(Y \times X)}) \land {finSupp}_{0_{Scalar (A)}} (W)))$
155	15 154	mpbid	$⊢ φ \to (W \in ({Base}_{Scalar (A)}^{(Y \times X)}) \land {finSupp}_{0_{Scalar (A)}} (W))$
156	155	simpld	$⊢ φ \to W \in ({Base}_{Scalar (A)}^{(Y \times X)})$
157		fvexd	$⊢ φ \to {Base}_{Scalar (A)} \in V$
158	157 150	elmapd	$⊢ φ \to (W \in ({Base}_{Scalar (A)}^{(Y \times X)}) \leftrightarrow W : Y \times X ⟶ {Base}_{Scalar (A)})$
159	156 158	mpbid	$⊢ φ \to W : Y \times X ⟶ {Base}_{Scalar (A)}$
160	159	ffnd	$⊢ φ \to W Fn (Y \times X)$
161	160	adantr	$⊢ (φ \land j \in Y) \to W Fn (Y \times X)$
162		simpr	$⊢ (φ \land j \in Y) \to j \in Y$
163	155	simprd	$⊢ φ \to {finSupp}_{0_{Scalar (A)}} (W)$
164		drngring	$⊢ E \in DivRing \to E \in Ring$
165	6 164	syl	$⊢ φ \to E \in Ring$
166		ringmnd	$⊢ E \in Ring \to E \in Mnd$
167	165 166	syl	$⊢ φ \to E \in Mnd$
168		subrgsubg	$⊢ V \in SubRing (E) \to V \in SubGrp (E)$
169	20 168	syl	$⊢ φ \to V \in SubGrp (E)$
170		eqid	$⊢ 0_{E} = 0_{E}$
171	170	subg0cl	$⊢ V \in SubGrp (E) \to 0_{E} \in V$
172	169 171	syl	$⊢ φ \to 0_{E} \in V$
173	53 172	sseldd	$⊢ φ \to 0_{E} \in U$
174	4 29 170	ress0g	$⊢ (E \in Mnd \land 0_{E} \in U \land U \subseteq {Base}_{E}) \to 0_{E} = 0_{F}$
175	167 173 31 174	syl3anc	$⊢ φ \to 0_{E} = 0_{F}$
176	61	fveq2d	$⊢ φ \to 0_{K} = 0_{Scalar (C)}$
177	5 170	subrg0	$⊢ V \in SubRing (E) \to 0_{E} = 0_{K}$
178	20 177	syl	$⊢ φ \to 0_{E} = 0_{K}$
179	67	fveq2d	$⊢ φ \to 0_{Scalar (A)} = 0_{Scalar (C)}$
180	176 178 179	3eqtr4d	$⊢ φ \to 0_{E} = 0_{Scalar (A)}$
181	175 180	eqtr3d	$⊢ φ \to 0_{F} = 0_{Scalar (A)}$
182	163 181	breqtrrd	$⊢ φ \to {finSupp}_{0_{F}} (W)$
183	182	adantr	$⊢ (φ \land j \in Y) \to {finSupp}_{0_{F}} (W)$
184	145 146 147 148 161 162 183	fsuppcurry1	$⊢ (φ \land j \in Y) \to {finSupp}_{0_{F}} ((i \in X ⟼ j W i))$
185	181	adantr	$⊢ (φ \land j \in Y) \to 0_{F} = 0_{Scalar (A)}$
186	184 185	breqtrd	$⊢ (φ \land j \in Y) \to {finSupp}_{0_{Scalar (A)}} ((i \in X ⟼ j W i))$
187		eqidd	$⊢ (φ \land j \in Y) \to (i \in X ⟼ j W i) = (i \in X ⟼ j W i)$
188	159	fovrnda	$⊢ (φ \land (j \in Y \land i \in X)) \to j W i \in {Base}_{Scalar (A)}$
189	188	anassrs	$⊢ ((φ \land j \in Y) \land i \in X) \to j W i \in {Base}_{Scalar (A)}$
190	187 189	fvmpt2d	$⊢ ((φ \land j \in Y) \land i \in X) \to (i \in X ⟼ j W i) (i) = j W i$
191	190	oveq1d	$⊢ ((φ \land j \in Y) \land i \in X) \to (i \in X ⟼ j W i) (i) \cdot_{A} i = (j W i) \cdot_{A} i$
192	124	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to \cdot_{A} = \cdot_{B}$
193	192	oveqd	$⊢ ((φ \land j \in Y) \land i \in X) \to (j W i) \cdot_{A} i = (j W i) \cdot_{B} i$
194	191 193	eqtrd	$⊢ ((φ \land j \in Y) \land i \in X) \to (i \in X ⟼ j W i) (i) \cdot_{A} i = (j W i) \cdot_{B} i$
195	194	mpteq2dva	$⊢ (φ \land j \in Y) \to (i \in X ⟼ (i \in X ⟼ j W i) (i) \cdot_{A} i) = (i \in X ⟼ (j W i) \cdot_{B} i)$
196	195	oveq2d	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{A}} ((i \in X ⟼ j W i) (i) \cdot_{A} i) = \underset{i \in X}{\sum_{A}} ((j W i) \cdot_{B} i)$
197	6	adantr	$⊢ (φ \land j \in Y) \to E \in DivRing$
198	20	adantr	$⊢ (φ \land j \in Y) \to V \in SubRing (E)$
199	8	adantr	$⊢ (φ \land j \in Y) \to K \in DivRing$
200	1 197 198 5 199 148	drgextgsum	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} ((j W i) \cdot_{B} i) = \underset{i \in X}{\sum_{A}} ((j W i) \cdot_{B} i)$
201	9	adantr	$⊢ (φ \land j \in Y) \to U \in SubRing (E)$
202	7	adantr	$⊢ (φ \land j \in Y) \to F \in DivRing$
203	2 197 201 4 202 148	drgextgsum	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} ((j W i) \cdot_{B} i) = \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)$
204	200 203	eqtr3d	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{A}} ((j W i) \cdot_{B} i) = \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)$
205	196 204	eqtrd	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{A}} ((i \in X ⟼ j W i) (i) \cdot_{A} i) = \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)$
206	14	mptexd	$⊢ φ \to (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \in V$
207		eqid	$⊢ 0_{B} = 0_{B}$
208	2 4	sralvec	$⊢ (E \in DivRing \land F \in DivRing \land U \in SubRing (E)) \to B \in LVec$
209	6 7 9 208	syl3anc	$⊢ φ \to B \in LVec$
210		lveclmod	$⊢ B \in LVec \to B \in LMod$
211	209 210	syl	$⊢ φ \to B \in LMod$
212	211	adantr	$⊢ (φ \land j \in Y) \to B \in LMod$
213		lmodabl	$⊢ B \in LMod \to B \in Abel$
214	212 213	syl	$⊢ (φ \land j \in Y) \to B \in Abel$
215	2	a1i	$⊢ φ \to B = subringAlg (E) (U)$
216	215 9 31	srasubrg	$⊢ φ \to U \in SubRing (B)$
217		subrgsubg	$⊢ U \in SubRing (B) \to U \in SubGrp (B)$
218	216 217	syl	$⊢ φ \to U \in SubGrp (B)$
219	218	adantr	$⊢ (φ \land j \in Y) \to U \in SubGrp (B)$
220	116	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to C \in LMod$
221	68	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to {Base}_{Scalar (A)} = {Base}_{Scalar (C)}$
222	189 221	eleqtrd	$⊢ ((φ \land j \in Y) \land i \in X) \to j W i \in {Base}_{Scalar (C)}$
223	28	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to X \subseteq {Base}_{C}$
224		simpr	$⊢ ((φ \land j \in Y) \land i \in X) \to i \in X$
225	223 224	sseldd	$⊢ ((φ \land j \in Y) \land i \in X) \to i \in {Base}_{C}$
226	25 117 118 119	lmodvscl	$⊢ (C \in LMod \land j W i \in {Base}_{Scalar (C)} \land i \in {Base}_{C}) \to (j W i) \cdot_{C} i \in {Base}_{C}$
227	220 222 225 226	syl3anc	$⊢ ((φ \land j \in Y) \land i \in X) \to (j W i) \cdot_{C} i \in {Base}_{C}$
228	130	oveqd	$⊢ φ \to (j W i) \cdot_{B} i = (j W i) \cdot_{C} i$
229	228	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to (j W i) \cdot_{B} i = (j W i) \cdot_{C} i$
230	39	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to U = {Base}_{C}$
231	227 229 230	3eltr4d	$⊢ ((φ \land j \in Y) \land i \in X) \to (j W i) \cdot_{B} i \in U$
232	231	fmpttd	$⊢ (φ \land j \in Y) \to (i \in X ⟼ (j W i) \cdot_{B} i) : X ⟶ U$
233	215 31	srasca	$⊢ φ \to E ↾_{𝑠} U = Scalar (B)$
234	4 233	syl5eq	$⊢ φ \to F = Scalar (B)$
235	234	adantr	$⊢ (φ \land j \in Y) \to F = Scalar (B)$
236		eqid	$⊢ {Base}_{B} = {Base}_{B}$
237		ovexd	$⊢ ((φ \land j \in Y) \land i \in X) \to j W i \in V$
238	28 40	sstrd	$⊢ φ \to X \subseteq {Base}_{E}$
239	238	adantr	$⊢ (φ \land (j \in Y \land i \in X)) \to X \subseteq {Base}_{E}$
240		simprr	$⊢ (φ \land (j \in Y \land i \in X)) \to i \in X$
241	239 240	sseldd	$⊢ (φ \land (j \in Y \land i \in X)) \to i \in {Base}_{E}$
242	241	anassrs	$⊢ ((φ \land j \in Y) \land i \in X) \to i \in {Base}_{E}$
243	215 31	srabase	$⊢ φ \to {Base}_{E} = {Base}_{B}$
244	243	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to {Base}_{E} = {Base}_{B}$
245	242 244	eleqtrd	$⊢ ((φ \land j \in Y) \land i \in X) \to i \in {Base}_{B}$
246		eqid	$⊢ 0_{F} = 0_{F}$
247		eqid	$⊢ \cdot_{B} = \cdot_{B}$
248	148 212 235 236 237 245 207 246 247 184	mptscmfsupp0	$⊢ (φ \land j \in Y) \to {finSupp}_{0_{B}} ((i \in X ⟼ (j W i) \cdot_{B} i))$
249	207 214 148 219 232 248	gsumsubgcl	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i) \in U$
250	234	fveq2d	$⊢ φ \to {Base}_{F} = {Base}_{Scalar (B)}$
251	33 250	eqtrd	$⊢ φ \to U = {Base}_{Scalar (B)}$
252	251	adantr	$⊢ (φ \land j \in Y) \to U = {Base}_{Scalar (B)}$
253	249 252	eleqtrd	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i) \in {Base}_{Scalar (B)}$
254	253	fmpttd	$⊢ φ \to (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) : Y ⟶ {Base}_{Scalar (B)}$
255	254	ffund	$⊢ φ \to Fun (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i))$
256		fvexd	$⊢ φ \to 0_{Scalar (B)} \in V$
257		fconstmpt	$⊢ X \times \{0_{Scalar (A)}\} = (i \in X ⟼ 0_{Scalar (A)})$
258	257	eqeq2i	$⊢ (i \in X ⟼ k W i) = X \times \{0_{Scalar (A)}\} \leftrightarrow (i \in X ⟼ k W i) = (i \in X ⟼ 0_{Scalar (A)})$
259		ovex	$⊢ k W i \in V$
260	259	rgenw	$⊢ \forall i \in X k W i \in V$
261		mpteqb	$⊢ \forall i \in X k W i \in V \to ((i \in X ⟼ k W i) = (i \in X ⟼ 0_{Scalar (A)}) \leftrightarrow \forall i \in X k W i = 0_{Scalar (A)})$
262	260 261	ax-mp	$⊢ (i \in X ⟼ k W i) = (i \in X ⟼ 0_{Scalar (A)}) \leftrightarrow \forall i \in X k W i = 0_{Scalar (A)}$
263	258 262	bitri	$⊢ (i \in X ⟼ k W i) = X \times \{0_{Scalar (A)}\} \leftrightarrow \forall i \in X k W i = 0_{Scalar (A)}$
264	263	necon3abii	$⊢ (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\} \leftrightarrow \neg \forall i \in X k W i = 0_{Scalar (A)}$
265		df-ov	$⊢ k W i = W (⟨k, i⟩)$
266	265	eqcomi	$⊢ W (⟨k, i⟩) = k W i$
267	266	a1i	$⊢ ((φ \land k \in Y) \land i \in X) \to W (⟨k, i⟩) = k W i$
268	267	eqeq1d	$⊢ ((φ \land k \in Y) \land i \in X) \to (W (⟨k, i⟩) = 0_{Scalar (A)} \leftrightarrow k W i = 0_{Scalar (A)})$
269	268	necon3abid	$⊢ ((φ \land k \in Y) \land i \in X) \to (W (⟨k, i⟩) \neq 0_{Scalar (A)} \leftrightarrow \neg k W i = 0_{Scalar (A)})$
270	269	rexbidva	$⊢ (φ \land k \in Y) \to (\exists i \in X W (⟨k, i⟩) \neq 0_{Scalar (A)} \leftrightarrow \exists i \in X \neg k W i = 0_{Scalar (A)})$
271		rexnal	$⊢ \exists i \in X \neg k W i = 0_{Scalar (A)} \leftrightarrow \neg \forall i \in X k W i = 0_{Scalar (A)}$
272	270 271	bitr2di	$⊢ (φ \land k \in Y) \to (\neg \forall i \in X k W i = 0_{Scalar (A)} \leftrightarrow \exists i \in X W (⟨k, i⟩) \neq 0_{Scalar (A)})$
273	264 272	syl5bb	$⊢ (φ \land k \in Y) \to ((i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\} \leftrightarrow \exists i \in X W (⟨k, i⟩) \neq 0_{Scalar (A)})$
274	273	rabbidva	$⊢ φ \to \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\} = \{k \in Y \| \exists i \in X W (⟨k, i⟩) \neq 0_{Scalar (A)}\}$
275		fveq2	$⊢ z = ⟨k, i⟩ \to W (z) = W (⟨k, i⟩)$
276	275	neeq1d	$⊢ z = ⟨k, i⟩ \to (W (z) \neq 0_{Scalar (A)} \leftrightarrow W (⟨k, i⟩) \neq 0_{Scalar (A)})$
277	276	dmrab	$⊢ dom \{z \in (Y \times X) \| W (z) \neq 0_{Scalar (A)}\} = \{k \in Y \| \exists i \in X W (⟨k, i⟩) \neq 0_{Scalar (A)}\}$
278	274 277	eqtr4di	$⊢ φ \to \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\} = dom \{z \in (Y \times X) \| W (z) \neq 0_{Scalar (A)}\}$
279		fvexd	$⊢ φ \to 0_{Scalar (A)} \in V$
280		suppvalfn	$⊢ (W Fn (Y \times X) \land Y \times X \in V \land 0_{Scalar (A)} \in V) \to W supp 0_{Scalar (A)} = \{z \in (Y \times X) \| W (z) \neq 0_{Scalar (A)}\}$
281	160 150 279 280	syl3anc	$⊢ φ \to W supp 0_{Scalar (A)} = \{z \in (Y \times X) \| W (z) \neq 0_{Scalar (A)}\}$
282	163	fsuppimpd	$⊢ φ \to W supp 0_{Scalar (A)} \in Fin$
283	281 282	eqeltrrd	$⊢ φ \to \{z \in (Y \times X) \| W (z) \neq 0_{Scalar (A)}\} \in Fin$
284		dmfi	$⊢ \{z \in (Y \times X) \| W (z) \neq 0_{Scalar (A)}\} \in Fin \to dom \{z \in (Y \times X) \| W (z) \neq 0_{Scalar (A)}\} \in Fin$
285	283 284	syl	$⊢ φ \to dom \{z \in (Y \times X) \| W (z) \neq 0_{Scalar (A)}\} \in Fin$
286	278 285	eqeltrd	$⊢ φ \to \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\} \in Fin$
287		nfv	$⊢ Ⅎ i φ$
288		nfcv	$⊢ \underline{Ⅎ} i Y$
289		nfmpt1	$⊢ \underline{Ⅎ} i (i \in X ⟼ k W i)$
290		nfcv	$⊢ \underline{Ⅎ} i (X \times \{0_{Scalar (A)}\})$
291	289 290	nfne	$⊢ Ⅎ i (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}$
292	291 288	nfrabw	$⊢ \underline{Ⅎ} i \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\}$
293	288 292	nfdif	$⊢ \underline{Ⅎ} i (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})$
294	293	nfcri	$⊢ Ⅎ i j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})$
295	287 294	nfan	$⊢ Ⅎ i (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\}))$
296		simpr	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})$
297	296	eldifad	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to j \in Y$
298	296	eldifbd	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to \neg j \in \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\}$
299		oveq1	$⊢ k = j \to k W i = j W i$
300	299	mpteq2dv	$⊢ k = j \to (i \in X ⟼ k W i) = (i \in X ⟼ j W i)$
301	300	neeq1d	$⊢ k = j \to ((i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\} \leftrightarrow (i \in X ⟼ j W i) \neq X \times \{0_{Scalar (A)}\})$
302	301	elrab	$⊢ j \in \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\} \leftrightarrow (j \in Y \land (i \in X ⟼ j W i) \neq X \times \{0_{Scalar (A)}\})$
303	298 302	sylnib	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to \neg (j \in Y \land (i \in X ⟼ j W i) \neq X \times \{0_{Scalar (A)}\})$
304	297 303	mpnanrd	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to \neg (i \in X ⟼ j W i) \neq X \times \{0_{Scalar (A)}\}$
305		nne	$⊢ \neg (i \in X ⟼ j W i) \neq X \times \{0_{Scalar (A)}\} \leftrightarrow (i \in X ⟼ j W i) = X \times \{0_{Scalar (A)}\}$
306	304 305	sylib	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to (i \in X ⟼ j W i) = X \times \{0_{Scalar (A)}\}$
307	306 257	eqtrdi	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to (i \in X ⟼ j W i) = (i \in X ⟼ 0_{Scalar (A)})$
308		ovex	$⊢ j W i \in V$
309	308	rgenw	$⊢ \forall i \in X j W i \in V$
310		mpteqb	$⊢ \forall i \in X j W i \in V \to ((i \in X ⟼ j W i) = (i \in X ⟼ 0_{Scalar (A)}) \leftrightarrow \forall i \in X j W i = 0_{Scalar (A)})$
311	309 310	ax-mp	$⊢ (i \in X ⟼ j W i) = (i \in X ⟼ 0_{Scalar (A)}) \leftrightarrow \forall i \in X j W i = 0_{Scalar (A)}$
312	307 311	sylib	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to \forall i \in X j W i = 0_{Scalar (A)}$
313	312	r19.21bi	$⊢ ((φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \land i \in X) \to j W i = 0_{Scalar (A)}$
314	313	oveq1d	$⊢ ((φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \land i \in X) \to (j W i) \cdot_{B} i = 0_{Scalar (A)} \cdot_{B} i$
315	2 6 9	drgext0g	$⊢ φ \to 0_{E} = 0_{B}$
316	2 6 9	drgext0gsca	$⊢ φ \to 0_{B} = 0_{Scalar (B)}$
317	315 180 316	3eqtr3d	$⊢ φ \to 0_{Scalar (A)} = 0_{Scalar (B)}$
318	317	ad2antrr	$⊢ ((φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \land i \in X) \to 0_{Scalar (A)} = 0_{Scalar (B)}$
319	318	oveq1d	$⊢ ((φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \land i \in X) \to 0_{Scalar (A)} \cdot_{B} i = 0_{Scalar (B)} \cdot_{B} i$
320	211	ad2antrr	$⊢ ((φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \land i \in X) \to B \in LMod$
321	297 245	syldanl	$⊢ ((φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \land i \in X) \to i \in {Base}_{B}$
322		eqid	$⊢ Scalar (B) = Scalar (B)$
323		eqid	$⊢ 0_{Scalar (B)} = 0_{Scalar (B)}$
324	236 322 247 323 207	lmod0vs	$⊢ (B \in LMod \land i \in {Base}_{B}) \to 0_{Scalar (B)} \cdot_{B} i = 0_{B}$
325	320 321 324	syl2anc	$⊢ ((φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \land i \in X) \to 0_{Scalar (B)} \cdot_{B} i = 0_{B}$
326	314 319 325	3eqtrd	$⊢ ((φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \land i \in X) \to (j W i) \cdot_{B} i = 0_{B}$
327	295 326	mpteq2da	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to (i \in X ⟼ (j W i) \cdot_{B} i) = (i \in X ⟼ 0_{B})$
328	327	oveq2d	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i) = \underset{i \in X}{\sum_{B}} 0_{B}$
329	211 213	syl	$⊢ φ \to B \in Abel$
330		ablgrp	$⊢ B \in Abel \to B \in Grp$
331		grpmnd	$⊢ B \in Grp \to B \in Mnd$
332	329 330 331	3syl	$⊢ φ \to B \in Mnd$
333	207	gsumz	$⊢ (B \in Mnd \land X \in LBasis (C)) \to \underset{i \in X}{\sum_{B}} 0_{B} = 0_{B}$
334	332 13 333	syl2anc	$⊢ φ \to \underset{i \in X}{\sum_{B}} 0_{B} = 0_{B}$
335	334	adantr	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to \underset{i \in X}{\sum_{B}} 0_{B} = 0_{B}$
336	316	adantr	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to 0_{B} = 0_{Scalar (B)}$
337	328 335 336	3eqtrd	$⊢ (φ \land j \in (Y ∖ \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i) = 0_{Scalar (B)}$
338	337 14	suppss2	$⊢ φ \to (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) supp 0_{Scalar (B)} \subseteq \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\}$
339		suppssfifsupp	$⊢ (((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \in V \land Fun (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \land 0_{Scalar (B)} \in V) \land (\{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\} \in Fin \land (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) supp 0_{Scalar (B)} \subseteq \{k \in Y \| (i \in X ⟼ k W i) \neq X \times \{0_{Scalar (A)}\}\})) \to {finSupp}_{0_{Scalar (B)}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)))$
340	206 255 256 286 338 339	syl32anc	$⊢ φ \to {finSupp}_{0_{Scalar (B)}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)))$
341		eqidd	$⊢ φ \to (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i))$
342		ovexd	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i) \in V$
343	341 342	fvmpt2d	$⊢ (φ \land j \in Y) \to (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) = \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)$
344	343	oveq1d	$⊢ (φ \land j \in Y) \to (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) \cdot_{B} j = (\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j$
345	344	mpteq2dva	$⊢ φ \to (j \in Y ⟼ (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) \cdot_{B} j) = (j \in Y ⟼ (\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j)$
346	345	oveq2d	$⊢ φ \to \underset{j \in Y}{\sum_{B}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) \cdot_{B} j) = \underset{j \in Y}{\sum_{B}} ((\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j)$
347	124	adantr	$⊢ (φ \land j \in Y) \to \cdot_{A} = \cdot_{B}$
348	50	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to \cdot_{E} = \cdot_{A}$
349	348	oveqd	$⊢ ((φ \land j \in Y) \land i \in X) \to (j W i) \cdot_{E} i = (j W i) \cdot_{A} i$
350	349	mpteq2dva	$⊢ (φ \land j \in Y) \to (i \in X ⟼ (j W i) \cdot_{E} i) = (i \in X ⟼ (j W i) \cdot_{A} i)$
351	123	adantr	$⊢ (φ \land j \in Y) \to \cdot_{E} = \cdot_{B}$
352	351	oveqd	$⊢ (φ \land j \in Y) \to (j W i) \cdot_{E} i = (j W i) \cdot_{B} i$
353	352	mpteq2dv	$⊢ (φ \land j \in Y) \to (i \in X ⟼ (j W i) \cdot_{E} i) = (i \in X ⟼ (j W i) \cdot_{B} i)$
354	350 353	eqtr3d	$⊢ (φ \land j \in Y) \to (i \in X ⟼ (j W i) \cdot_{A} i) = (i \in X ⟼ (j W i) \cdot_{B} i)$
355	354	oveq2d	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{A}} ((j W i) \cdot_{A} i) = \underset{i \in X}{\sum_{A}} ((j W i) \cdot_{B} i)$
356		eqidd	$⊢ (φ \land j \in Y) \to j = j$
357	347 355 356	oveq123d	$⊢ (φ \land j \in Y) \to (\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{A} i)) \cdot_{A} j = (\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{B} i)) \cdot_{B} j$
358	204	oveq1d	$⊢ (φ \land j \in Y) \to (\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{B} i)) \cdot_{B} j = (\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j$
359	357 358	eqtrd	$⊢ (φ \land j \in Y) \to (\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{A} i)) \cdot_{A} j = (\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j$
360	359	mpteq2dva	$⊢ φ \to (j \in Y ⟼ (\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{A} i)) \cdot_{A} j) = (j \in Y ⟼ (\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j)$
361	360	oveq2d	$⊢ φ \to \underset{j \in Y}{\sum_{A}} ((\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{A} i)) \cdot_{A} j) = \underset{j \in Y}{\sum_{A}} ((\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j)$
362	1 29	sraring	$⊢ (E \in Ring \land V \subseteq {Base}_{E}) \to A \in Ring$
363	165 43 362	syl2anc	$⊢ φ \to A \in Ring$
364		ringcmn	$⊢ A \in Ring \to A \in CMnd$
365	363 364	syl	$⊢ φ \to A \in CMnd$
366	165	adantr	$⊢ (φ \land (j \in Y \land i \in X)) \to E \in Ring$
367		eqid	$⊢ LBasis (B) = LBasis (B)$
368	236 367	lbsss	$⊢ Y \in LBasis (B) \to Y \subseteq {Base}_{B}$
369	14 368	syl	$⊢ φ \to Y \subseteq {Base}_{B}$
370	369 243	sseqtrrd	$⊢ φ \to Y \subseteq {Base}_{E}$
371	370	adantr	$⊢ (φ \land (j \in Y \land i \in X)) \to Y \subseteq {Base}_{E}$
372		simprl	$⊢ (φ \land (j \in Y \land i \in X)) \to j \in Y$
373	371 372	sseldd	$⊢ (φ \land (j \in Y \land i \in X)) \to j \in {Base}_{E}$
374	29 74	ringcl	$⊢ (E \in Ring \land i \in {Base}_{E} \land j \in {Base}_{E}) \to i \cdot_{E} j \in {Base}_{E}$
375	366 241 373 374	syl3anc	$⊢ (φ \land (j \in Y \land i \in X)) \to i \cdot_{E} j \in {Base}_{E}$
376	44	adantr	$⊢ (φ \land (j \in Y \land i \in X)) \to {Base}_{E} = {Base}_{A}$
377	375 376	eleqtrd	$⊢ (φ \land (j \in Y \land i \in X)) \to i \cdot_{E} j \in {Base}_{A}$
378	377	ralrimivva	$⊢ φ \to \forall j \in Y \forall i \in X i \cdot_{E} j \in {Base}_{A}$
379	11	fmpo	$⊢ \forall j \in Y \forall i \in X i \cdot_{E} j \in {Base}_{A} \leftrightarrow D : Y \times X ⟶ {Base}_{A}$
380	378 379	sylib	$⊢ φ \to D : Y \times X ⟶ {Base}_{A}$
381	79 80 82 81 24 159 380 150	lcomf	$⊢ φ \to (W {\cdot_{A}}_{f} D) : Y \times X ⟶ {Base}_{A}$
382	79 80 82 81 24 159 380 150 139 140 163	lcomfsupp	$⊢ φ \to {finSupp}_{0_{A}} ((W {\cdot_{A}}_{f} D))$
383	81 139 365 14 13 381 382	gsumxp	$⊢ φ \to \sum_{A} (W {\cdot_{A}}_{f} D) = \underset{j \in Y}{\sum_{A}} (\underset{i \in X}{\sum_{A}}, (j (W {\cdot_{A}}_{f} D) i))$
384	165	3ad2ant1	$⊢ (φ \land j \in Y \land i \in X) \to E \in Ring$
385	159	3ad2ant1	$⊢ (φ \land j \in Y \land i \in X) \to W : Y \times X ⟶ {Base}_{Scalar (A)}$
386	64 62	eqtrd	$⊢ φ \to V = {Base}_{Scalar (C)}$
387	386 43	eqsstrrd	$⊢ φ \to {Base}_{Scalar (C)} \subseteq {Base}_{E}$
388	68 387	eqsstrd	$⊢ φ \to {Base}_{Scalar (A)} \subseteq {Base}_{E}$
389	388 44	sseqtrd	$⊢ φ \to {Base}_{Scalar (A)} \subseteq {Base}_{A}$
390	389	3ad2ant1	$⊢ (φ \land j \in Y \land i \in X) \to {Base}_{Scalar (A)} \subseteq {Base}_{A}$
391	385 390	fssd	$⊢ (φ \land j \in Y \land i \in X) \to W : Y \times X ⟶ {Base}_{A}$
392		simp2	$⊢ (φ \land j \in Y \land i \in X) \to j \in Y$
393		simp3	$⊢ (φ \land j \in Y \land i \in X) \to i \in X$
394	391 392 393	fovrnd	$⊢ (φ \land j \in Y \land i \in X) \to j W i \in {Base}_{A}$
395	44	3ad2ant1	$⊢ (φ \land j \in Y \land i \in X) \to {Base}_{E} = {Base}_{A}$
396	394 395	eleqtrrd	$⊢ (φ \land j \in Y \land i \in X) \to j W i \in {Base}_{E}$
397	241	3impb	$⊢ (φ \land j \in Y \land i \in X) \to i \in {Base}_{E}$
398	373	3impb	$⊢ (φ \land j \in Y \land i \in X) \to j \in {Base}_{E}$
399	29 74	ringass	$⊢ (E \in Ring \land (j W i \in {Base}_{E} \land i \in {Base}_{E} \land j \in {Base}_{E})) \to ((j W i) \cdot_{E} i) \cdot_{E} j = (j W i) \cdot_{E} (i \cdot_{E} j)$
400	384 396 397 398 399	syl13anc	$⊢ (φ \land j \in Y \land i \in X) \to ((j W i) \cdot_{E} i) \cdot_{E} j = (j W i) \cdot_{E} (i \cdot_{E} j)$
401	400	mpoeq3dva	$⊢ φ \to (j \in Y, i \in X ⟼ ((j W i) \cdot_{E} i) \cdot_{E} j) = (j \in Y, i \in X ⟼ (j W i) \cdot_{E} (i \cdot_{E} j))$
402		ovexd	$⊢ (φ \land j \in Y \land i \in X) \to j W i \in V$
403		ovexd	$⊢ (φ \land j \in Y \land i \in X) \to i \cdot_{E} j \in V$
404		fnov	$⊢ W Fn (Y \times X) \leftrightarrow W = (j \in Y, i \in X ⟼ j W i)$
405	160 404	sylib	$⊢ φ \to W = (j \in Y, i \in X ⟼ j W i)$
406	11	a1i	$⊢ φ \to D = (j \in Y, i \in X ⟼ i \cdot_{E} j)$
407	14 13 402 403 405 406	offval22	$⊢ φ \to W {\cdot_{E}}_{f} D = (j \in Y, i \in X ⟼ (j W i) \cdot_{E} (i \cdot_{E} j))$
408		ofeq	$⊢ \cdot_{E} = \cdot_{A} \to \circ_{f} \cdot_{E} = \circ_{f} \cdot_{A}$
409	50 408	syl	$⊢ φ \to \circ_{f} \cdot_{E} = \circ_{f} \cdot_{A}$
410	409	oveqd	$⊢ φ \to W {\cdot_{E}}_{f} D = W {\cdot_{A}}_{f} D$
411	401 407 410	3eqtr2rd	$⊢ φ \to W {\cdot_{A}}_{f} D = (j \in Y, i \in X ⟼ ((j W i) \cdot_{E} i) \cdot_{E} j)$
412	411	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to W {\cdot_{A}}_{f} D = (j \in Y, i \in X ⟼ ((j W i) \cdot_{E} i) \cdot_{E} j)$
413	412	oveqd	$⊢ ((φ \land j \in Y) \land i \in X) \to j (W {\cdot_{A}}_{f} D) i = j (j \in Y, i \in X ⟼ ((j W i) \cdot_{E} i) \cdot_{E} j) i$
414		simplr	$⊢ ((φ \land j \in Y) \land i \in X) \to j \in Y$
415		ovexd	$⊢ ((φ \land j \in Y) \land i \in X) \to ((j W i) \cdot_{E} i) \cdot_{E} j \in V$
416		eqid	$⊢ (j \in Y, i \in X ⟼ ((j W i) \cdot_{E} i) \cdot_{E} j) = (j \in Y, i \in X ⟼ ((j W i) \cdot_{E} i) \cdot_{E} j)$
417	416	ovmpt4g	$⊢ (j \in Y \land i \in X \land ((j W i) \cdot_{E} i) \cdot_{E} j \in V) \to j (j \in Y, i \in X ⟼ ((j W i) \cdot_{E} i) \cdot_{E} j) i = ((j W i) \cdot_{E} i) \cdot_{E} j$
418	414 224 415 417	syl3anc	$⊢ ((φ \land j \in Y) \land i \in X) \to j (j \in Y, i \in X ⟼ ((j W i) \cdot_{E} i) \cdot_{E} j) i = ((j W i) \cdot_{E} i) \cdot_{E} j$
419	413 418	eqtrd	$⊢ ((φ \land j \in Y) \land i \in X) \to j (W {\cdot_{A}}_{f} D) i = ((j W i) \cdot_{E} i) \cdot_{E} j$
420	419	mpteq2dva	$⊢ (φ \land j \in Y) \to (i \in X ⟼ j (W {\cdot_{A}}_{f} D) i) = (i \in X ⟼ ((j W i) \cdot_{E} i) \cdot_{E} j)$
421	420	oveq2d	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} (j (W {\cdot_{A}}_{f} D) i) = \underset{i \in X}{\sum_{E}} (((j W i) \cdot_{E} i) \cdot_{E} j)$
422	165	adantr	$⊢ (φ \land j \in Y) \to E \in Ring$
423	370	sselda	$⊢ (φ \land j \in Y) \to j \in {Base}_{E}$
424	165	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to E \in Ring$
425	387	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to {Base}_{Scalar (C)} \subseteq {Base}_{E}$
426	425 222	sseldd	$⊢ ((φ \land j \in Y) \land i \in X) \to j W i \in {Base}_{E}$
427	29 74	ringcl	$⊢ (E \in Ring \land j W i \in {Base}_{E} \land i \in {Base}_{E}) \to (j W i) \cdot_{E} i \in {Base}_{E}$
428	424 426 242 427	syl3anc	$⊢ ((φ \land j \in Y) \land i \in X) \to (j W i) \cdot_{E} i \in {Base}_{E}$
429	315	adantr	$⊢ (φ \land j \in Y) \to 0_{E} = 0_{B}$
430	248 353 429	3brtr4d	$⊢ (φ \land j \in Y) \to {finSupp}_{0_{E}} ((i \in X ⟼ (j W i) \cdot_{E} i))$
431	29 170 100 74 422 148 423 428 430	gsummulc1	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} (((j W i) \cdot_{E} i) \cdot_{E} j) = (\underset{i \in X}{\sum_{E}}, ((j W i) \cdot_{E} i)) \cdot_{E} j$
432	421 431	eqtrd	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} (j (W {\cdot_{A}}_{f} D) i) = (\underset{i \in X}{\sum_{E}}, ((j W i) \cdot_{E} i)) \cdot_{E} j$
433	148	mptexd	$⊢ (φ \land j \in Y) \to (i \in X ⟼ j (W {\cdot_{A}}_{f} D) i) \in V$
434	24	adantr	$⊢ (φ \land j \in Y) \to A \in LMod$
435	43	adantr	$⊢ (φ \land j \in Y) \to V \subseteq {Base}_{E}$
436	1 433 197 434 435	gsumsra	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} (j (W {\cdot_{A}}_{f} D) i) = \underset{i \in X}{\sum_{A}} (j (W {\cdot_{A}}_{f} D) i)$
437	148	mptexd	$⊢ (φ \land j \in Y) \to (i \in X ⟼ (j W i) \cdot_{E} i) \in V$
438	1 437 197 434 435	gsumsra	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} ((j W i) \cdot_{E} i) = \underset{i \in X}{\sum_{A}} ((j W i) \cdot_{E} i)$
439	438	oveq1d	$⊢ (φ \land j \in Y) \to (\underset{i \in X}{\sum_{E}}, ((j W i) \cdot_{E} i)) \cdot_{E} j = (\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{E} i)) \cdot_{E} j$
440	50	adantr	$⊢ (φ \land j \in Y) \to \cdot_{E} = \cdot_{A}$
441	350	oveq2d	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{A}} ((j W i) \cdot_{E} i) = \underset{i \in X}{\sum_{A}} ((j W i) \cdot_{A} i)$
442	440 441 356	oveq123d	$⊢ (φ \land j \in Y) \to (\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{E} i)) \cdot_{E} j = (\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{A} i)) \cdot_{A} j$
443	439 442	eqtrd	$⊢ (φ \land j \in Y) \to (\underset{i \in X}{\sum_{E}}, ((j W i) \cdot_{E} i)) \cdot_{E} j = (\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{A} i)) \cdot_{A} j$
444	432 436 443	3eqtr3d	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{A}} (j (W {\cdot_{A}}_{f} D) i) = (\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{A} i)) \cdot_{A} j$
445	444	mpteq2dva	$⊢ φ \to (j \in Y ⟼ \underset{i \in X}{\sum_{A}} (j (W {\cdot_{A}}_{f} D) i)) = (j \in Y ⟼ (\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{A} i)) \cdot_{A} j)$
446	445	oveq2d	$⊢ φ \to \underset{j \in Y}{\sum_{A}} (\underset{i \in X}{\sum_{A}}, (j (W {\cdot_{A}}_{f} D) i)) = \underset{j \in Y}{\sum_{A}} ((\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{A} i)) \cdot_{A} j)$
447	383 16 446	3eqtr3rd	$⊢ φ \to \underset{j \in Y}{\sum_{A}} ((\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{A} i)) \cdot_{A} j) = 0_{A}$
448	1 6 20	drgext0g	$⊢ φ \to 0_{E} = 0_{A}$
449	447 448 315	3eqtr2d	$⊢ φ \to \underset{j \in Y}{\sum_{A}} ((\underset{i \in X}{\sum_{A}}, ((j W i) \cdot_{A} i)) \cdot_{A} j) = 0_{B}$
450	1 6 20 5 8 14	drgextgsum	$⊢ φ \to \underset{j \in Y}{\sum_{E}} ((\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j) = \underset{j \in Y}{\sum_{A}} ((\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j)$
451	2 6 9 4 7 14	drgextgsum	$⊢ φ \to \underset{j \in Y}{\sum_{E}} ((\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j) = \underset{j \in Y}{\sum_{B}} ((\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j)$
452	450 451	eqtr3d	$⊢ φ \to \underset{j \in Y}{\sum_{A}} ((\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j) = \underset{j \in Y}{\sum_{B}} ((\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j)$
453	361 449 452	3eqtr3rd	$⊢ φ \to \underset{j \in Y}{\sum_{B}} ((\underset{i \in X}{\sum_{B}}, ((j W i) \cdot_{B} i)) \cdot_{B} j) = 0_{B}$
454	346 453	eqtrd	$⊢ φ \to \underset{j \in Y}{\sum_{B}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) \cdot_{B} j) = 0_{B}$
455		breq1	$⊢ b = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \to ({finSupp}_{0_{Scalar (B)}} (b) \leftrightarrow {finSupp}_{0_{Scalar (B)}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i))))$
456		nfmpt1	$⊢ \underline{Ⅎ} j (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i))$
457	456	nfeq2	$⊢ Ⅎ j b = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i))$
458		fveq1	$⊢ b = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \to b (j) = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j)$
459	458	oveq1d	$⊢ b = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \to b (j) \cdot_{B} j = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) \cdot_{B} j$
460	459	adantr	$⊢ (b = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \land j \in Y) \to b (j) \cdot_{B} j = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) \cdot_{B} j$
461	457 460	mpteq2da	$⊢ b = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \to (j \in Y ⟼ b (j) \cdot_{B} j) = (j \in Y ⟼ (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) \cdot_{B} j)$
462	461	oveq2d	$⊢ b = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \to \underset{j \in Y}{\sum_{B}} (b (j) \cdot_{B} j) = \underset{j \in Y}{\sum_{B}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) \cdot_{B} j)$
463	462	eqeq1d	$⊢ b = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \to (\underset{j \in Y}{\sum_{B}} (b (j) \cdot_{B} j) = 0_{B} \leftrightarrow \underset{j \in Y}{\sum_{B}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) \cdot_{B} j) = 0_{B})$
464	455 463	anbi12d	$⊢ b = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \to (({finSupp}_{0_{Scalar (B)}} (b) \land \underset{j \in Y}{\sum_{B}} (b (j) \cdot_{B} j) = 0_{B}) \leftrightarrow ({finSupp}_{0_{Scalar (B)}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i))) \land \underset{j \in Y}{\sum_{B}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) \cdot_{B} j) = 0_{B}))$
465		eqeq1	$⊢ b = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \to (b = Y \times \{0_{Scalar (B)}\} \leftrightarrow (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) = Y \times \{0_{Scalar (B)}\})$
466	464 465	imbi12d	$⊢ b = (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \to ((({finSupp}_{0_{Scalar (B)}} (b) \land \underset{j \in Y}{\sum_{B}} (b (j) \cdot_{B} j) = 0_{B}) \to b = Y \times \{0_{Scalar (B)}\}) \leftrightarrow (({finSupp}_{0_{Scalar (B)}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i))) \land \underset{j \in Y}{\sum_{B}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) \cdot_{B} j) = 0_{B}) \to (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) = Y \times \{0_{Scalar (B)}\}))$
467	367	lbslinds	$⊢ LBasis (B) \subseteq LIndS (B)$
468	467 14	sseldi	$⊢ φ \to Y \in LIndS (B)$
469		eqid	$⊢ {Base}_{Scalar (B)} = {Base}_{Scalar (B)}$
470	236 469 322 247 207 323	islinds5	$⊢ (B \in LMod \land Y \subseteq {Base}_{B}) \to (Y \in LIndS (B) \leftrightarrow \forall b \in ({Base}_{Scalar (B)}^{Y}) (({finSupp}_{0_{Scalar (B)}} (b) \land \underset{j \in Y}{\sum_{B}} (b (j) \cdot_{B} j) = 0_{B}) \to b = Y \times \{0_{Scalar (B)}\}))$
471	470	biimpa	$⊢ ((B \in LMod \land Y \subseteq {Base}_{B}) \land Y \in LIndS (B)) \to \forall b \in ({Base}_{Scalar (B)}^{Y}) (({finSupp}_{0_{Scalar (B)}} (b) \land \underset{j \in Y}{\sum_{B}} (b (j) \cdot_{B} j) = 0_{B}) \to b = Y \times \{0_{Scalar (B)}\})$
472	211 369 468 471	syl21anc	$⊢ φ \to \forall b \in ({Base}_{Scalar (B)}^{Y}) (({finSupp}_{0_{Scalar (B)}} (b) \land \underset{j \in Y}{\sum_{B}} (b (j) \cdot_{B} j) = 0_{B}) \to b = Y \times \{0_{Scalar (B)}\})$
473		fvexd	$⊢ φ \to {Base}_{Scalar (B)} \in V$
474		elmapg	$⊢ ({Base}_{Scalar (B)} \in V \land Y \in LBasis (B)) \to ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \in ({Base}_{Scalar (B)}^{Y}) \leftrightarrow (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) : Y ⟶ {Base}_{Scalar (B)})$
475	474	biimpar	$⊢ (({Base}_{Scalar (B)} \in V \land Y \in LBasis (B)) \land (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) : Y ⟶ {Base}_{Scalar (B)}) \to (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \in ({Base}_{Scalar (B)}^{Y})$
476	473 14 254 475	syl21anc	$⊢ φ \to (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) \in ({Base}_{Scalar (B)}^{Y})$
477	466 472 476	rspcdva	$⊢ φ \to (({finSupp}_{0_{Scalar (B)}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i))) \land \underset{j \in Y}{\sum_{B}} ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) (j) \cdot_{B} j) = 0_{B}) \to (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) = Y \times \{0_{Scalar (B)}\})$
478	340 454 477	mp2and	$⊢ φ \to (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) = Y \times \{0_{Scalar (B)}\}$
479		fconstmpt	$⊢ Y \times \{0_{Scalar (B)}\} = (j \in Y ⟼ 0_{Scalar (B)})$
480	478 479	eqtrdi	$⊢ φ \to (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) = (j \in Y ⟼ 0_{Scalar (B)})$
481		ovex	$⊢ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i) \in V$
482	481	rgenw	$⊢ \forall j \in Y \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i) \in V$
483		mpteqb	$⊢ \forall j \in Y \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i) \in V \to ((j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) = (j \in Y ⟼ 0_{Scalar (B)}) \leftrightarrow \forall j \in Y \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i) = 0_{Scalar (B)})$
484	482 483	ax-mp	$⊢ (j \in Y ⟼ \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i)) = (j \in Y ⟼ 0_{Scalar (B)}) \leftrightarrow \forall j \in Y \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i) = 0_{Scalar (B)}$
485	480 484	sylib	$⊢ φ \to \forall j \in Y \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i) = 0_{Scalar (B)}$
486	485	r19.21bi	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{B}} ((j W i) \cdot_{B} i) = 0_{Scalar (B)}$
487	315 448 316	3eqtr3rd	$⊢ φ \to 0_{Scalar (B)} = 0_{A}$
488	487	adantr	$⊢ (φ \land j \in Y) \to 0_{Scalar (B)} = 0_{A}$
489	205 486 488	3eqtrd	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{A}} ((i \in X ⟼ j W i) (i) \cdot_{A} i) = 0_{A}$
490	186 489	jca	$⊢ (φ \land j \in Y) \to ({finSupp}_{0_{Scalar (A)}} ((i \in X ⟼ j W i)) \land \underset{i \in X}{\sum_{A}} ((i \in X ⟼ j W i) (i) \cdot_{A} i) = 0_{A})$
491	189	fmpttd	$⊢ (φ \land j \in Y) \to (i \in X ⟼ j W i) : X ⟶ {Base}_{Scalar (A)}$
492		fvexd	$⊢ (φ \land j \in Y) \to {Base}_{Scalar (A)} \in V$
493	492 148	elmapd	$⊢ (φ \land j \in Y) \to ((i \in X ⟼ j W i) \in ({Base}_{Scalar (A)}^{X}) \leftrightarrow (i \in X ⟼ j W i) : X ⟶ {Base}_{Scalar (A)})$
494	491 493	mpbird	$⊢ (φ \land j \in Y) \to (i \in X ⟼ j W i) \in ({Base}_{Scalar (A)}^{X})$
495		simpr	$⊢ ((φ \land j \in Y) \land w = (i \in X ⟼ j W i)) \to w = (i \in X ⟼ j W i)$
496	495	breq1d	$⊢ ((φ \land j \in Y) \land w = (i \in X ⟼ j W i)) \to ({finSupp}_{0_{Scalar (A)}} (w) \leftrightarrow {finSupp}_{0_{Scalar (A)}} ((i \in X ⟼ j W i)))$
497		nfv	$⊢ Ⅎ i (φ \land j \in Y)$
498		nfmpt1	$⊢ \underline{Ⅎ} i (i \in X ⟼ j W i)$
499	498	nfeq2	$⊢ Ⅎ i w = (i \in X ⟼ j W i)$
500	497 499	nfan	$⊢ Ⅎ i ((φ \land j \in Y) \land w = (i \in X ⟼ j W i))$
501		simplr	$⊢ (((φ \land j \in Y) \land w = (i \in X ⟼ j W i)) \land i \in X) \to w = (i \in X ⟼ j W i)$
502	501	fveq1d	$⊢ (((φ \land j \in Y) \land w = (i \in X ⟼ j W i)) \land i \in X) \to w (i) = (i \in X ⟼ j W i) (i)$
503	502	oveq1d	$⊢ (((φ \land j \in Y) \land w = (i \in X ⟼ j W i)) \land i \in X) \to w (i) \cdot_{A} i = (i \in X ⟼ j W i) (i) \cdot_{A} i$
504	500 503	mpteq2da	$⊢ ((φ \land j \in Y) \land w = (i \in X ⟼ j W i)) \to (i \in X ⟼ w (i) \cdot_{A} i) = (i \in X ⟼ (i \in X ⟼ j W i) (i) \cdot_{A} i)$
505	504	oveq2d	$⊢ ((φ \land j \in Y) \land w = (i \in X ⟼ j W i)) \to \underset{i \in X}{\sum_{A}} (w (i) \cdot_{A} i) = \underset{i \in X}{\sum_{A}} ((i \in X ⟼ j W i) (i) \cdot_{A} i)$
506	505	eqeq1d	$⊢ ((φ \land j \in Y) \land w = (i \in X ⟼ j W i)) \to (\underset{i \in X}{\sum_{A}} (w (i) \cdot_{A} i) = 0_{A} \leftrightarrow \underset{i \in X}{\sum_{A}} ((i \in X ⟼ j W i) (i) \cdot_{A} i) = 0_{A})$
507	496 506	anbi12d	$⊢ ((φ \land j \in Y) \land w = (i \in X ⟼ j W i)) \to (({finSupp}_{0_{Scalar (A)}} (w) \land \underset{i \in X}{\sum_{A}} (w (i) \cdot_{A} i) = 0_{A}) \leftrightarrow ({finSupp}_{0_{Scalar (A)}} ((i \in X ⟼ j W i)) \land \underset{i \in X}{\sum_{A}} ((i \in X ⟼ j W i) (i) \cdot_{A} i) = 0_{A}))$
508	495	eqeq1d	$⊢ ((φ \land j \in Y) \land w = (i \in X ⟼ j W i)) \to (w = X \times \{0_{Scalar (A)}\} \leftrightarrow (i \in X ⟼ j W i) = X \times \{0_{Scalar (A)}\})$
509	507 508	imbi12d	$⊢ ((φ \land j \in Y) \land w = (i \in X ⟼ j W i)) \to ((({finSupp}_{0_{Scalar (A)}} (w) \land \underset{i \in X}{\sum_{A}} (w (i) \cdot_{A} i) = 0_{A}) \to w = X \times \{0_{Scalar (A)}\}) \leftrightarrow (({finSupp}_{0_{Scalar (A)}} ((i \in X ⟼ j W i)) \land \underset{i \in X}{\sum_{A}} ((i \in X ⟼ j W i) (i) \cdot_{A} i) = 0_{A}) \to (i \in X ⟼ j W i) = X \times \{0_{Scalar (A)}\}))$
510	494 509	rspcdv	$⊢ (φ \land j \in Y) \to (\forall w \in ({Base}_{Scalar (A)}^{X}) (({finSupp}_{0_{Scalar (A)}} (w) \land \underset{i \in X}{\sum_{A}} (w (i) \cdot_{A} i) = 0_{A}) \to w = X \times \{0_{Scalar (A)}\}) \to (({finSupp}_{0_{Scalar (A)}} ((i \in X ⟼ j W i)) \land \underset{i \in X}{\sum_{A}} ((i \in X ⟼ j W i) (i) \cdot_{A} i) = 0_{A}) \to (i \in X ⟼ j W i) = X \times \{0_{Scalar (A)}\}))$
511	144 490 510	mp2d	$⊢ (φ \land j \in Y) \to (i \in X ⟼ j W i) = X \times \{0_{Scalar (A)}\}$
512	511 257	eqtrdi	$⊢ (φ \land j \in Y) \to (i \in X ⟼ j W i) = (i \in X ⟼ 0_{Scalar (A)})$
513	512 311	sylib	$⊢ (φ \land j \in Y) \to \forall i \in X j W i = 0_{Scalar (A)}$
514	513	ralrimiva	$⊢ φ \to \forall j \in Y \forall i \in X j W i = 0_{Scalar (A)}$
515		eqidd	$⊢ (j = k \land i = l) \to 0_{Scalar (A)} = 0_{Scalar (A)}$
516		fvexd	$⊢ (φ \land j \in Y \land i \in X) \to 0_{Scalar (A)} \in V$
517		fvexd	$⊢ (φ \land k \in Y \land l \in X) \to 0_{Scalar (A)} \in V$
518	160 515 516 517	fnmpoovd	$⊢ φ \to (W = (k \in Y, l \in X ⟼ 0_{Scalar (A)}) \leftrightarrow \forall j \in Y \forall i \in X j W i = 0_{Scalar (A)})$
519	514 518	mpbird	$⊢ φ \to W = (k \in Y, l \in X ⟼ 0_{Scalar (A)})$
520		fconstmpo	$⊢ (Y \times X) \times \{0_{Scalar (A)}\} = (k \in Y, l \in X ⟼ 0_{Scalar (A)})$
521	519 520	eqtr4di	$⊢ φ \to W = (Y \times X) \times \{0_{Scalar (A)}\}$

Metamath Proof Explorer

Theorem fedgmullem2

Proof