fedgmullem1

	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)$
	fedgmullem1.a	$⊢ φ \to Z \in {Base}_{A}$
	fedgmullem1.l	$⊢ φ \to L : Y ⟶ {Base}_{Scalar (B)}$
	fedgmullem1.1	$⊢ φ \to {finSupp}_{0_{Scalar (B)}} (L)$
	fedgmullem1.z	$⊢ φ \to Z = \underset{j \in Y}{\sum_{B}} (L (j) \cdot_{B} j)$
	fedgmullem1.g	$⊢ φ \to G : Y ⟶ {Base}_{Scalar (C)}^{X}$
	fedgmullem1.2	$⊢ (φ \land j \in Y) \to {finSupp}_{0_{Scalar (C)}} (G (j))$
	fedgmullem1.3	$⊢ (φ \land j \in Y) \to L (j) = \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i)$
Assertion	fedgmullem1	$⊢ φ \to ({finSupp}_{0_{Scalar (A)}} (H) \land Z = \sum_{A} (H {\cdot_{A}}_{f} D))$

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		fedgmullem1.a	$⊢ φ \to Z \in {Base}_{A}$
16		fedgmullem1.l	$⊢ φ \to L : Y ⟶ {Base}_{Scalar (B)}$
17		fedgmullem1.1	$⊢ φ \to {finSupp}_{0_{Scalar (B)}} (L)$
18		fedgmullem1.z	$⊢ φ \to Z = \underset{j \in Y}{\sum_{B}} (L (j) \cdot_{B} j)$
19		fedgmullem1.g	$⊢ φ \to G : Y ⟶ {Base}_{Scalar (C)}^{X}$
20		fedgmullem1.2	$⊢ (φ \land j \in Y) \to {finSupp}_{0_{Scalar (C)}} (G (j))$
21		fedgmullem1.3	$⊢ (φ \land j \in Y) \to L (j) = \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i)$
22		simpllr	$⊢ (((φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \land j \in Y) \land i \in X) \to G : Y ⟶ {Base}_{Scalar (C)}^{X}$
23		simplr	$⊢ (((φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \land j \in Y) \land i \in X) \to j \in Y$
24	22 23	ffvelrnd	$⊢ (((φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \land j \in Y) \land i \in X) \to G (j) \in ({Base}_{Scalar (C)}^{X})$
25		elmapi	$⊢ G (j) \in ({Base}_{Scalar (C)}^{X}) \to G (j) : X ⟶ {Base}_{Scalar (C)}$
26	24 25	syl	$⊢ (((φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \land j \in Y) \land i \in X) \to G (j) : X ⟶ {Base}_{Scalar (C)}$
27	26	anasss	$⊢ ((φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \land (j \in Y \land i \in X)) \to G (j) : X ⟶ {Base}_{Scalar (C)}$
28		simprr	$⊢ ((φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \land (j \in Y \land i \in X)) \to i \in X$
29	27 28	ffvelrnd	$⊢ ((φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \land (j \in Y \land i \in X)) \to G (j) (i) \in {Base}_{Scalar (C)}$
30	1	a1i	$⊢ φ \to A = subringAlg (E) (V)$
31	4	subsubrg	$⊢ U \in SubRing (E) \to (V \in SubRing (F) \leftrightarrow (V \in SubRing (E) \land V \subseteq U))$
32	31	biimpa	$⊢ (U \in SubRing (E) \land V \in SubRing (F)) \to (V \in SubRing (E) \land V \subseteq U)$
33	9 10 32	syl2anc	$⊢ φ \to (V \in SubRing (E) \land V \subseteq U)$
34	33	simpld	$⊢ φ \to V \in SubRing (E)$
35		eqid	$⊢ {Base}_{E} = {Base}_{E}$
36	35	subrgss	$⊢ V \in SubRing (E) \to V \subseteq {Base}_{E}$
37	34 36	syl	$⊢ φ \to V \subseteq {Base}_{E}$
38	30 37	srasca	$⊢ φ \to E ↾_{𝑠} V = Scalar (A)$
39	5 38	syl5eq	$⊢ φ \to K = Scalar (A)$
40	33	simprd	$⊢ φ \to V \subseteq U$
41		ressabs	$⊢ (U \in SubRing (E) \land V \subseteq U) \to (E ↾_{𝑠} U) ↾_{𝑠} V = E ↾_{𝑠} V$
42	9 40 41	syl2anc	$⊢ φ \to (E ↾_{𝑠} U) ↾_{𝑠} V = E ↾_{𝑠} V$
43	4	oveq1i	$⊢ F ↾_{𝑠} V = (E ↾_{𝑠} U) ↾_{𝑠} V$
44	42 43 5	3eqtr4g	$⊢ φ \to F ↾_{𝑠} V = K$
45	3	a1i	$⊢ φ \to C = subringAlg (F) (V)$
46		eqid	$⊢ {Base}_{F} = {Base}_{F}$
47	46	subrgss	$⊢ V \in SubRing (F) \to V \subseteq {Base}_{F}$
48	10 47	syl	$⊢ φ \to V \subseteq {Base}_{F}$
49	45 48	srasca	$⊢ φ \to F ↾_{𝑠} V = Scalar (C)$
50	44 49	eqtr3d	$⊢ φ \to K = Scalar (C)$
51	39 50	eqtr3d	$⊢ φ \to Scalar (A) = Scalar (C)$
52	51	fveq2d	$⊢ φ \to {Base}_{Scalar (A)} = {Base}_{Scalar (C)}$
53	52	ad2antrr	$⊢ ((φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \land (j \in Y \land i \in X)) \to {Base}_{Scalar (A)} = {Base}_{Scalar (C)}$
54	29 53	eleqtrrd	$⊢ ((φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \land (j \in Y \land i \in X)) \to G (j) (i) \in {Base}_{Scalar (A)}$
55	54	ralrimivva	$⊢ (φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \to \forall j \in Y \forall i \in X G (j) (i) \in {Base}_{Scalar (A)}$
56	12	fmpo	$⊢ \forall j \in Y \forall i \in X G (j) (i) \in {Base}_{Scalar (A)} \leftrightarrow H : Y \times X ⟶ {Base}_{Scalar (A)}$
57	55 56	sylib	$⊢ (φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \to H : Y \times X ⟶ {Base}_{Scalar (A)}$
58		fvexd	$⊢ (φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \to {Base}_{Scalar (A)} \in V$
59	14 13	xpexd	$⊢ φ \to Y \times X \in V$
60	59	adantr	$⊢ (φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \to Y \times X \in V$
61	58 60	elmapd	$⊢ (φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \to (H \in ({Base}_{Scalar (A)}^{(Y \times X)}) \leftrightarrow H : Y \times X ⟶ {Base}_{Scalar (A)})$
62	57 61	mpbird	$⊢ (φ \land G : Y ⟶ {Base}_{Scalar (C)}^{X}) \to H \in ({Base}_{Scalar (A)}^{(Y \times X)})$
63	19 62	mpdan	$⊢ φ \to H \in ({Base}_{Scalar (A)}^{(Y \times X)})$
64		simpl	$⊢ (φ \land j \in Y) \to φ$
65	64	adantr	$⊢ ((φ \land j \in Y) \land i \in X) \to φ$
66	19	ffvelrnda	$⊢ (φ \land j \in Y) \to G (j) \in ({Base}_{Scalar (C)}^{X})$
67	66 25	syl	$⊢ (φ \land j \in Y) \to G (j) : X ⟶ {Base}_{Scalar (C)}$
68	67	adantr	$⊢ ((φ \land j \in Y) \land i \in X) \to G (j) : X ⟶ {Base}_{Scalar (C)}$
69	52	feq3d	$⊢ φ \to (G (j) : X ⟶ {Base}_{Scalar (A)} \leftrightarrow G (j) : X ⟶ {Base}_{Scalar (C)})$
70	69	biimpar	$⊢ (φ \land G (j) : X ⟶ {Base}_{Scalar (C)}) \to G (j) : X ⟶ {Base}_{Scalar (A)}$
71	65 68 70	syl2anc	$⊢ ((φ \land j \in Y) \land i \in X) \to G (j) : X ⟶ {Base}_{Scalar (A)}$
72		simpr	$⊢ ((φ \land j \in Y) \land i \in X) \to i \in X$
73	71 72	ffvelrnd	$⊢ ((φ \land j \in Y) \land i \in X) \to G (j) (i) \in {Base}_{Scalar (A)}$
74	73	ralrimiva	$⊢ (φ \land j \in Y) \to \forall i \in X G (j) (i) \in {Base}_{Scalar (A)}$
75	74	ralrimiva	$⊢ φ \to \forall j \in Y \forall i \in X G (j) (i) \in {Base}_{Scalar (A)}$
76	75 56	sylib	$⊢ φ \to H : Y \times X ⟶ {Base}_{Scalar (A)}$
77	76	ffund	$⊢ φ \to Fun H$
78		drngring	$⊢ E \in DivRing \to E \in Ring$
79	6 78	syl	$⊢ φ \to E \in Ring$
80		ringgrp	$⊢ E \in Ring \to E \in Grp$
81		eqid	$⊢ 0_{E} = 0_{E}$
82	35 81	grpidcl	$⊢ E \in Grp \to 0_{E} \in {Base}_{E}$
83	79 80 82	3syl	$⊢ φ \to 0_{E} \in {Base}_{E}$
84	17	fsuppimpd	$⊢ φ \to L supp 0_{Scalar (B)} \in Fin$
85		simpl	$⊢ (φ \land j \in (Y ∖ {supp}_{0_{Scalar (B)}} (L))) \to φ$
86		simpr	$⊢ (φ \land j \in (Y ∖ {supp}_{0_{Scalar (B)}} (L))) \to j \in (Y ∖ {supp}_{0_{Scalar (B)}} (L))$
87	86	eldifad	$⊢ (φ \land j \in (Y ∖ {supp}_{0_{Scalar (B)}} (L))) \to j \in Y$
88		ssidd	$⊢ φ \to L supp 0_{Scalar (B)} \subseteq L supp 0_{Scalar (B)}$
89		fvexd	$⊢ φ \to 0_{Scalar (B)} \in V$
90	16 88 14 89	suppssr	$⊢ (φ \land j \in (Y ∖ {supp}_{0_{Scalar (B)}} (L))) \to L (j) = 0_{Scalar (B)}$
91	87 21	syldan	$⊢ (φ \land j \in (Y ∖ {supp}_{0_{Scalar (B)}} (L))) \to L (j) = \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i)$
92	2	a1i	$⊢ φ \to B = subringAlg (E) (U)$
93	35	subrgss	$⊢ U \in SubRing (E) \to U \subseteq {Base}_{E}$
94	9 93	syl	$⊢ φ \to U \subseteq {Base}_{E}$
95	92 94	srasca	$⊢ φ \to E ↾_{𝑠} U = Scalar (B)$
96	4 95	syl5eq	$⊢ φ \to F = Scalar (B)$
97	96	fveq2d	$⊢ φ \to 0_{F} = 0_{Scalar (B)}$
98	3 7 10	drgext0g	$⊢ φ \to 0_{F} = 0_{C}$
99	97 98	eqtr3d	$⊢ φ \to 0_{Scalar (B)} = 0_{C}$
100	99	adantr	$⊢ (φ \land j \in (Y ∖ {supp}_{0_{Scalar (B)}} (L))) \to 0_{Scalar (B)} = 0_{C}$
101	90 91 100	3eqtr3d	$⊢ (φ \land j \in (Y ∖ {supp}_{0_{Scalar (B)}} (L))) \to \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i) = 0_{C}$
102		breq1	$⊢ g = G (j) \to ({finSupp}_{0_{Scalar (C)}} (g) \leftrightarrow {finSupp}_{0_{Scalar (C)}} (G (j)))$
103		fveq1	$⊢ g = G (j) \to g (i) = G (j) (i)$
104	103	oveq1d	$⊢ g = G (j) \to g (i) \cdot_{C} i = G (j) (i) \cdot_{C} i$
105	104	mpteq2dv	$⊢ g = G (j) \to (i \in X ⟼ g (i) \cdot_{C} i) = (i \in X ⟼ G (j) (i) \cdot_{C} i)$
106	105	oveq2d	$⊢ g = G (j) \to \underset{i \in X}{\sum_{C}} (g (i) \cdot_{C} i) = \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i)$
107	106	eqeq1d	$⊢ g = G (j) \to (\underset{i \in X}{\sum_{C}} (g (i) \cdot_{C} i) = 0_{C} \leftrightarrow \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i) = 0_{C})$
108	102 107	anbi12d	$⊢ g = G (j) \to (({finSupp}_{0_{Scalar (C)}} (g) \land \underset{i \in X}{\sum_{C}} (g (i) \cdot_{C} i) = 0_{C}) \leftrightarrow ({finSupp}_{0_{Scalar (C)}} (G (j)) \land \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i) = 0_{C}))$
109		eqeq1	$⊢ g = G (j) \to (g = X \times \{0_{Scalar (C)}\} \leftrightarrow G (j) = X \times \{0_{Scalar (C)}\})$
110	108 109	imbi12d	$⊢ g = G (j) \to ((({finSupp}_{0_{Scalar (C)}} (g) \land \underset{i \in X}{\sum_{C}} (g (i) \cdot_{C} i) = 0_{C}) \to g = X \times \{0_{Scalar (C)}\}) \leftrightarrow (({finSupp}_{0_{Scalar (C)}} (G (j)) \land \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i) = 0_{C}) \to G (j) = X \times \{0_{Scalar (C)}\}))$
111	44 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	116	adantr	$⊢ (φ \land j \in Y) \to C \in LMod$
118		eqid	$⊢ {Base}_{C} = {Base}_{C}$
119		eqid	$⊢ LBasis (C) = LBasis (C)$
120	118 119	lbsss	$⊢ X \in LBasis (C) \to X \subseteq {Base}_{C}$
121	13 120	syl	$⊢ φ \to X \subseteq {Base}_{C}$
122	121	adantr	$⊢ (φ \land j \in Y) \to X \subseteq {Base}_{C}$
123		eqid	$⊢ LSpan (C) = LSpan (C)$
124	118 119 123	islbs4	$⊢ X \in LBasis (C) \leftrightarrow (X \in LIndS (C) \land LSpan (C) (X) = {Base}_{C})$
125	13 124	sylib	$⊢ φ \to (X \in LIndS (C) \land LSpan (C) (X) = {Base}_{C})$
126	125	simpld	$⊢ φ \to X \in LIndS (C)$
127	126	adantr	$⊢ (φ \land j \in Y) \to X \in LIndS (C)$
128		eqid	$⊢ {Base}_{Scalar (C)} = {Base}_{Scalar (C)}$
129		eqid	$⊢ Scalar (C) = Scalar (C)$
130		eqid	$⊢ \cdot_{C} = \cdot_{C}$
131		eqid	$⊢ 0_{C} = 0_{C}$
132		eqid	$⊢ 0_{Scalar (C)} = 0_{Scalar (C)}$
133	118 128 129 130 131 132	islinds5	$⊢ (C \in LMod \land X \subseteq {Base}_{C}) \to (X \in LIndS (C) \leftrightarrow \forall g \in ({Base}_{Scalar (C)}^{X}) (({finSupp}_{0_{Scalar (C)}} (g) \land \underset{i \in X}{\sum_{C}} (g (i) \cdot_{C} i) = 0_{C}) \to g = X \times \{0_{Scalar (C)}\}))$
134	133	biimpa	$⊢ ((C \in LMod \land X \subseteq {Base}_{C}) \land X \in LIndS (C)) \to \forall g \in ({Base}_{Scalar (C)}^{X}) (({finSupp}_{0_{Scalar (C)}} (g) \land \underset{i \in X}{\sum_{C}} (g (i) \cdot_{C} i) = 0_{C}) \to g = X \times \{0_{Scalar (C)}\})$
135	117 122 127 134	syl21anc	$⊢ (φ \land j \in Y) \to \forall g \in ({Base}_{Scalar (C)}^{X}) (({finSupp}_{0_{Scalar (C)}} (g) \land \underset{i \in X}{\sum_{C}} (g (i) \cdot_{C} i) = 0_{C}) \to g = X \times \{0_{Scalar (C)}\})$
136	110 135 66	rspcdva	$⊢ (φ \land j \in Y) \to (({finSupp}_{0_{Scalar (C)}} (G (j)) \land \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i) = 0_{C}) \to G (j) = X \times \{0_{Scalar (C)}\})$
137	20 136	mpand	$⊢ (φ \land j \in Y) \to (\underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i) = 0_{C} \to G (j) = X \times \{0_{Scalar (C)}\})$
138	137	imp	$⊢ ((φ \land j \in Y) \land \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i) = 0_{C}) \to G (j) = X \times \{0_{Scalar (C)}\}$
139	85 87 101 138	syl21anc	$⊢ (φ \land j \in (Y ∖ {supp}_{0_{Scalar (B)}} (L))) \to G (j) = X \times \{0_{Scalar (C)}\}$
140	19 139	suppss	$⊢ φ \to G supp (X \times \{0_{Scalar (C)}\}) \subseteq L supp 0_{Scalar (B)}$
141	84 140	ssfid	$⊢ φ \to G supp (X \times \{0_{Scalar (C)}\}) \in Fin$
142		suppssdm	$⊢ G supp (X \times \{0_{Scalar (C)}\}) \subseteq dom G$
143	142 19	fssdm	$⊢ φ \to G supp (X \times \{0_{Scalar (C)}\}) \subseteq Y$
144	143	sselda	$⊢ (φ \land w \in {supp}_{(X \times \{0_{Scalar (C)}\})} (G)) \to w \in Y$
145		eleq1w	$⊢ j = w \to (j \in Y \leftrightarrow w \in Y)$
146	145	anbi2d	$⊢ j = w \to ((φ \land j \in Y) \leftrightarrow (φ \land w \in Y))$
147		fveq2	$⊢ j = w \to G (j) = G (w)$
148	147	breq1d	$⊢ j = w \to ({finSupp}_{0_{Scalar (C)}} (G (j)) \leftrightarrow {finSupp}_{0_{Scalar (C)}} (G (w)))$
149	146 148	imbi12d	$⊢ j = w \to (((φ \land j \in Y) \to {finSupp}_{0_{Scalar (C)}} (G (j))) \leftrightarrow ((φ \land w \in Y) \to {finSupp}_{0_{Scalar (C)}} (G (w))))$
150	149 20	chvarvv	$⊢ (φ \land w \in Y) \to {finSupp}_{0_{Scalar (C)}} (G (w))$
151	150	fsuppimpd	$⊢ (φ \land w \in Y) \to G (w) supp 0_{Scalar (C)} \in Fin$
152	144 151	syldan	$⊢ (φ \land w \in {supp}_{(X \times \{0_{Scalar (C)}\})} (G)) \to G (w) supp 0_{Scalar (C)} \in Fin$
153	152	ralrimiva	$⊢ φ \to \forall w \in {supp}_{(X \times \{0_{Scalar (C)}\})} (G) G (w) supp 0_{Scalar (C)} \in Fin$
154		iunfi	$⊢ (G supp (X \times \{0_{Scalar (C)}\}) \in Fin \land \forall w \in {supp}_{(X \times \{0_{Scalar (C)}\})} (G) G (w) supp 0_{Scalar (C)} \in Fin) \to ⋃_{w \in G supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} (G (w)) \in Fin$
155	141 153 154	syl2anc	$⊢ φ \to ⋃_{w \in G supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} (G (w)) \in Fin$
156		xpfi	$⊢ (G supp (X \times \{0_{Scalar (C)}\}) \in Fin \land ⋃_{w \in G supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} (G (w)) \in Fin) \to {supp}_{(X \times \{0_{Scalar (C)}\})} (G) \times ⋃_{w \in G supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} (G (w)) \in Fin$
157	141 155 156	syl2anc	$⊢ φ \to {supp}_{(X \times \{0_{Scalar (C)}\})} (G) \times ⋃_{w \in G supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} (G (w)) \in Fin$
158		fveq2	$⊢ v = j \to G (v) = G (j)$
159	158	fveq1d	$⊢ v = j \to G (v) (u) = G (j) (u)$
160	159	mpteq2dv	$⊢ v = j \to (u \in X ⟼ G (v) (u)) = (u \in X ⟼ G (j) (u))$
161		fveq2	$⊢ u = i \to G (j) (u) = G (j) (i)$
162	161	cbvmptv	$⊢ (u \in X ⟼ G (j) (u)) = (i \in X ⟼ G (j) (i))$
163	160 162	eqtrdi	$⊢ v = j \to (u \in X ⟼ G (v) (u)) = (i \in X ⟼ G (j) (i))$
164	163	cbvmptv	$⊢ (v \in Y ⟼ (u \in X ⟼ G (v) (u))) = (j \in Y ⟼ (i \in X ⟼ G (j) (i)))$
165		fvexd	$⊢ φ \to 0_{Scalar (C)} \in V$
166		fvexd	$⊢ (φ \land (j \in Y \land i \in X)) \to G (j) (i) \in V$
167	12 164 14 13 165 166	suppovss	$⊢ φ \to H supp 0_{Scalar (C)} \subseteq {supp}_{(X \times \{0_{Scalar (C)}\})} ((v \in Y ⟼ (u \in X ⟼ G (v) (u)))) \times ⋃_{w \in (v \in Y ⟼ (u \in X ⟼ G (v) (u))) supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} ((v \in Y ⟼ (u \in X ⟼ G (v) (u))) (w))$
168	5 81	subrg0	$⊢ V \in SubRing (E) \to 0_{E} = 0_{K}$
169	34 168	syl	$⊢ φ \to 0_{E} = 0_{K}$
170	50	fveq2d	$⊢ φ \to 0_{K} = 0_{Scalar (C)}$
171	169 170	eqtr2d	$⊢ φ \to 0_{Scalar (C)} = 0_{E}$
172	171	oveq2d	$⊢ φ \to H supp 0_{Scalar (C)} = H supp 0_{E}$
173	19	feqmptd	$⊢ φ \to G = (v \in Y ⟼ G (v))$
174		eleq1w	$⊢ j = v \to (j \in Y \leftrightarrow v \in Y)$
175	174	anbi2d	$⊢ j = v \to ((φ \land j \in Y) \leftrightarrow (φ \land v \in Y))$
176		fveq2	$⊢ j = v \to G (j) = G (v)$
177	176	feq1d	$⊢ j = v \to (G (j) : X ⟶ {Base}_{E} \leftrightarrow G (v) : X ⟶ {Base}_{E})$
178	175 177	imbi12d	$⊢ j = v \to (((φ \land j \in Y) \to G (j) : X ⟶ {Base}_{E}) \leftrightarrow ((φ \land v \in Y) \to G (v) : X ⟶ {Base}_{E}))$
179	5 35	ressbas2	$⊢ V \subseteq {Base}_{E} \to V = {Base}_{K}$
180	37 179	syl	$⊢ φ \to V = {Base}_{K}$
181	50	fveq2d	$⊢ φ \to {Base}_{K} = {Base}_{Scalar (C)}$
182	180 181	eqtrd	$⊢ φ \to V = {Base}_{Scalar (C)}$
183	182 37	eqsstrrd	$⊢ φ \to {Base}_{Scalar (C)} \subseteq {Base}_{E}$
184	183	adantr	$⊢ (φ \land j \in Y) \to {Base}_{Scalar (C)} \subseteq {Base}_{E}$
185	67 184	fssd	$⊢ (φ \land j \in Y) \to G (j) : X ⟶ {Base}_{E}$
186	178 185	chvarvv	$⊢ (φ \land v \in Y) \to G (v) : X ⟶ {Base}_{E}$
187	186	feqmptd	$⊢ (φ \land v \in Y) \to G (v) = (u \in X ⟼ G (v) (u))$
188	187	mpteq2dva	$⊢ φ \to (v \in Y ⟼ G (v)) = (v \in Y ⟼ (u \in X ⟼ G (v) (u)))$
189	173 188	eqtr2d	$⊢ φ \to (v \in Y ⟼ (u \in X ⟼ G (v) (u))) = G$
190	189	oveq1d	$⊢ φ \to (v \in Y ⟼ (u \in X ⟼ G (v) (u))) supp (X \times \{0_{Scalar (C)}\}) = G supp (X \times \{0_{Scalar (C)}\})$
191	189	fveq1d	$⊢ φ \to (v \in Y ⟼ (u \in X ⟼ G (v) (u))) (w) = G (w)$
192	191	oveq1d	$⊢ φ \to (v \in Y ⟼ (u \in X ⟼ G (v) (u))) (w) supp 0_{Scalar (C)} = G (w) supp 0_{Scalar (C)}$
193	190 192	iuneq12d	$⊢ φ \to ⋃_{w \in (v \in Y ⟼ (u \in X ⟼ G (v) (u))) supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} ((v \in Y ⟼ (u \in X ⟼ G (v) (u))) (w)) = ⋃_{w \in G supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} (G (w))$
194	190 193	xpeq12d	$⊢ φ \to {supp}_{(X \times \{0_{Scalar (C)}\})} ((v \in Y ⟼ (u \in X ⟼ G (v) (u)))) \times ⋃_{w \in (v \in Y ⟼ (u \in X ⟼ G (v) (u))) supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} ((v \in Y ⟼ (u \in X ⟼ G (v) (u))) (w)) = {supp}_{(X \times \{0_{Scalar (C)}\})} (G) \times ⋃_{w \in G supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} (G (w))$
195	167 172 194	3sstr3d	$⊢ φ \to H supp 0_{E} \subseteq {supp}_{(X \times \{0_{Scalar (C)}\})} (G) \times ⋃_{w \in G supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} (G (w))$
196		suppssfifsupp	$⊢ ((H \in ({Base}_{Scalar (A)}^{(Y \times X)}) \land Fun H \land 0_{E} \in {Base}_{E}) \land ({supp}_{(X \times \{0_{Scalar (C)}\})} (G) \times ⋃_{w \in G supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} (G (w)) \in Fin \land H supp 0_{E} \subseteq {supp}_{(X \times \{0_{Scalar (C)}\})} (G) \times ⋃_{w \in G supp (X \times \{0_{Scalar (C)}\})} {supp}_{0_{Scalar (C)}} (G (w)))) \to {finSupp}_{0_{E}} (H)$
197	63 77 83 157 195 196	syl32anc	$⊢ φ \to {finSupp}_{0_{E}} (H)$
198	51	fveq2d	$⊢ φ \to 0_{Scalar (A)} = 0_{Scalar (C)}$
199	198 171	eqtr2d	$⊢ φ \to 0_{E} = 0_{Scalar (A)}$
200	197 199	breqtrd	$⊢ φ \to {finSupp}_{0_{Scalar (A)}} (H)$
201	2 6 9 4 7 14	drgextgsum	$⊢ φ \to \underset{j \in Y}{\sum_{E}} (L (j) \cdot_{B} j) = \underset{j \in Y}{\sum_{B}} (L (j) \cdot_{B} j)$
202	13	adantr	$⊢ (φ \land j \in Y) \to X \in LBasis (C)$
203	9	adantr	$⊢ (φ \land j \in Y) \to U \in SubRing (E)$
204		subrgsubg	$⊢ U \in SubRing (E) \to U \in SubGrp (E)$
205		subgsubm	$⊢ U \in SubGrp (E) \to U \in SubMnd (E)$
206	203 204 205	3syl	$⊢ (φ \land j \in Y) \to U \in SubMnd (E)$
207	116	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to C \in LMod$
208	67	ffvelrnda	$⊢ ((φ \land j \in Y) \land i \in X) \to G (j) (i) \in {Base}_{Scalar (C)}$
209	121	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to X \subseteq {Base}_{C}$
210	209 72	sseldd	$⊢ ((φ \land j \in Y) \land i \in X) \to i \in {Base}_{C}$
211	118 129 130 128	lmodvscl	$⊢ (C \in LMod \land G (j) (i) \in {Base}_{Scalar (C)} \land i \in {Base}_{C}) \to G (j) (i) \cdot_{C} i \in {Base}_{C}$
212	207 208 210 211	syl3anc	$⊢ ((φ \land j \in Y) \land i \in X) \to G (j) (i) \cdot_{C} i \in {Base}_{C}$
213	4 35	ressbas2	$⊢ U \subseteq {Base}_{E} \to U = {Base}_{F}$
214	94 213	syl	$⊢ φ \to U = {Base}_{F}$
215	45 48	srabase	$⊢ φ \to {Base}_{F} = {Base}_{C}$
216	214 215	eqtrd	$⊢ φ \to U = {Base}_{C}$
217	216	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to U = {Base}_{C}$
218	212 217	eleqtrrd	$⊢ ((φ \land j \in Y) \land i \in X) \to G (j) (i) \cdot_{C} i \in U$
219	218	fmpttd	$⊢ (φ \land j \in Y) \to (i \in X ⟼ G (j) (i) \cdot_{C} i) : X ⟶ U$
220	202 206 219 4	gsumsubm	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} (G (j) (i) \cdot_{C} i) = \underset{i \in X}{\sum_{F}} (G (j) (i) \cdot_{C} i)$
221		eqid	$⊢ \cdot_{E} = \cdot_{E}$
222	4 221	ressmulr	$⊢ U \in SubRing (E) \to \cdot_{E} = \cdot_{F}$
223	9 222	syl	$⊢ φ \to \cdot_{E} = \cdot_{F}$
224	45 48	sravsca	$⊢ φ \to \cdot_{F} = \cdot_{C}$
225	223 224	eqtr2d	$⊢ φ \to \cdot_{C} = \cdot_{E}$
226	225	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to \cdot_{C} = \cdot_{E}$
227	226	oveqd	$⊢ ((φ \land j \in Y) \land i \in X) \to G (j) (i) \cdot_{C} i = G (j) (i) \cdot_{E} i$
228	227	mpteq2dva	$⊢ (φ \land j \in Y) \to (i \in X ⟼ G (j) (i) \cdot_{C} i) = (i \in X ⟼ G (j) (i) \cdot_{E} i)$
229	228	oveq2d	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} (G (j) (i) \cdot_{C} i) = \underset{i \in X}{\sum_{E}} (G (j) (i) \cdot_{E} i)$
230	3 7 10 112 111 13	drgextgsum	$⊢ φ \to \underset{i \in X}{\sum_{F}} (G (j) (i) \cdot_{C} i) = \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i)$
231	230	adantr	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{F}} (G (j) (i) \cdot_{C} i) = \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i)$
232	220 229 231	3eqtr3d	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} (G (j) (i) \cdot_{E} i) = \underset{i \in X}{\sum_{C}} (G (j) (i) \cdot_{C} i)$
233	232	oveq1d	$⊢ (φ \land j \in Y) \to (\underset{i \in X}{\sum_{E}}, (G (j) (i) \cdot_{E} i)) \cdot_{E} j = (\underset{i \in X}{\sum_{C}}, (G (j) (i) \cdot_{C} i)) \cdot_{E} j$
234	79	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to E \in Ring$
235	183	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to {Base}_{Scalar (C)} \subseteq {Base}_{E}$
236	235 208	sseldd	$⊢ ((φ \land j \in Y) \land i \in X) \to G (j) (i) \in {Base}_{E}$
237	216 94	eqsstrrd	$⊢ φ \to {Base}_{C} \subseteq {Base}_{E}$
238	121 237	sstrd	$⊢ φ \to X \subseteq {Base}_{E}$
239	238	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to X \subseteq {Base}_{E}$
240	239 72	sseldd	$⊢ ((φ \land j \in Y) \land i \in X) \to i \in {Base}_{E}$
241		eqid	$⊢ {Base}_{B} = {Base}_{B}$
242		eqid	$⊢ LBasis (B) = LBasis (B)$
243	241 242	lbsss	$⊢ Y \in LBasis (B) \to Y \subseteq {Base}_{B}$
244	14 243	syl	$⊢ φ \to Y \subseteq {Base}_{B}$
245	92 94	srabase	$⊢ φ \to {Base}_{E} = {Base}_{B}$
246	244 245	sseqtrrd	$⊢ φ \to Y \subseteq {Base}_{E}$
247	246	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to Y \subseteq {Base}_{E}$
248		simplr	$⊢ ((φ \land j \in Y) \land i \in X) \to j \in Y$
249	247 248	sseldd	$⊢ ((φ \land j \in Y) \land i \in X) \to j \in {Base}_{E}$
250	35 221	ringass	$⊢ (E \in Ring \land (G (j) (i) \in {Base}_{E} \land i \in {Base}_{E} \land j \in {Base}_{E})) \to (G (j) (i) \cdot_{E} i) \cdot_{E} j = G (j) (i) \cdot_{E} (i \cdot_{E} j)$
251	234 236 240 249 250	syl13anc	$⊢ ((φ \land j \in Y) \land i \in X) \to (G (j) (i) \cdot_{E} i) \cdot_{E} j = G (j) (i) \cdot_{E} (i \cdot_{E} j)$
252	251	mpteq2dva	$⊢ (φ \land j \in Y) \to (i \in X ⟼ (G (j) (i) \cdot_{E} i) \cdot_{E} j) = (i \in X ⟼ G (j) (i) \cdot_{E} (i \cdot_{E} j))$
253	252	oveq2d	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} ((G (j) (i) \cdot_{E} i) \cdot_{E} j) = \underset{i \in X}{\sum_{E}} (G (j) (i) \cdot_{E} (i \cdot_{E} j))$
254		eqid	$⊢ +_{E} = +_{E}$
255	79	adantr	$⊢ (φ \land j \in Y) \to E \in Ring$
256	244	adantr	$⊢ (φ \land j \in Y) \to Y \subseteq {Base}_{B}$
257	245	adantr	$⊢ (φ \land j \in Y) \to {Base}_{E} = {Base}_{B}$
258	256 257	sseqtrrd	$⊢ (φ \land j \in Y) \to Y \subseteq {Base}_{E}$
259		simpr	$⊢ (φ \land j \in Y) \to j \in Y$
260	258 259	sseldd	$⊢ (φ \land j \in Y) \to j \in {Base}_{E}$
261	35 221	ringcl	$⊢ (E \in Ring \land G (j) (i) \in {Base}_{E} \land i \in {Base}_{E}) \to G (j) (i) \cdot_{E} i \in {Base}_{E}$
262	234 236 240 261	syl3anc	$⊢ ((φ \land j \in Y) \land i \in X) \to G (j) (i) \cdot_{E} i \in {Base}_{E}$
263	171	breq2d	$⊢ φ \to ({finSupp}_{0_{Scalar (C)}} (G (j)) \leftrightarrow {finSupp}_{0_{E}} (G (j)))$
264	263	adantr	$⊢ (φ \land j \in Y) \to ({finSupp}_{0_{Scalar (C)}} (G (j)) \leftrightarrow {finSupp}_{0_{E}} (G (j)))$
265	20 264	mpbid	$⊢ (φ \land j \in Y) \to {finSupp}_{0_{E}} (G (j))$
266	35 255 202 240 185 265	rmfsupp2	$⊢ (φ \land j \in Y) \to {finSupp}_{0_{E}} ((i \in X ⟼ G (j) (i) \cdot_{E} i))$
267	35 81 254 221 255 202 260 262 266	gsummulc1	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} ((G (j) (i) \cdot_{E} i) \cdot_{E} j) = (\underset{i \in X}{\sum_{E}}, (G (j) (i) \cdot_{E} i)) \cdot_{E} j$
268	253 267	eqtr3d	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} (G (j) (i) \cdot_{E} (i \cdot_{E} j)) = (\underset{i \in X}{\sum_{E}}, (G (j) (i) \cdot_{E} i)) \cdot_{E} j$
269	21	oveq1d	$⊢ (φ \land j \in Y) \to L (j) \cdot_{E} j = (\underset{i \in X}{\sum_{C}}, (G (j) (i) \cdot_{C} i)) \cdot_{E} j$
270	233 268 269	3eqtr4rd	$⊢ (φ \land j \in Y) \to L (j) \cdot_{E} j = \underset{i \in X}{\sum_{E}} (G (j) (i) \cdot_{E} (i \cdot_{E} j))$
271	92 94	sravsca	$⊢ φ \to \cdot_{E} = \cdot_{B}$
272	271	adantr	$⊢ (φ \land j \in Y) \to \cdot_{E} = \cdot_{B}$
273	272	oveqd	$⊢ (φ \land j \in Y) \to L (j) \cdot_{E} j = L (j) \cdot_{B} j$
274		fvexd	$⊢ (φ \land j \in Y \land i \in X) \to G (j) (i) \in V$
275		ovexd	$⊢ (φ \land j \in Y \land i \in X) \to i \cdot_{E} j \in V$
276	12	a1i	$⊢ φ \to H = (j \in Y, i \in X ⟼ G (j) (i))$
277	11	a1i	$⊢ φ \to D = (j \in Y, i \in X ⟼ i \cdot_{E} j)$
278	14 13 274 275 276 277	offval22	$⊢ φ \to H {\cdot_{E}}_{f} D = (j \in Y, i \in X ⟼ G (j) (i) \cdot_{E} (i \cdot_{E} j))$
279	278	oveqd	$⊢ φ \to j (H {\cdot_{E}}_{f} D) i = j (j \in Y, i \in X ⟼ G (j) (i) \cdot_{E} (i \cdot_{E} j)) i$
280	279	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to j (H {\cdot_{E}}_{f} D) i = j (j \in Y, i \in X ⟼ G (j) (i) \cdot_{E} (i \cdot_{E} j)) i$
281		ovexd	$⊢ ((φ \land j \in Y) \land i \in X) \to G (j) (i) \cdot_{E} (i \cdot_{E} j) \in V$
282		eqid	$⊢ (j \in Y, i \in X ⟼ G (j) (i) \cdot_{E} (i \cdot_{E} j)) = (j \in Y, i \in X ⟼ G (j) (i) \cdot_{E} (i \cdot_{E} j))$
283	282	ovmpt4g	$⊢ (j \in Y \land i \in X \land G (j) (i) \cdot_{E} (i \cdot_{E} j) \in V) \to j (j \in Y, i \in X ⟼ G (j) (i) \cdot_{E} (i \cdot_{E} j)) i = G (j) (i) \cdot_{E} (i \cdot_{E} j)$
284	248 72 281 283	syl3anc	$⊢ ((φ \land j \in Y) \land i \in X) \to j (j \in Y, i \in X ⟼ G (j) (i) \cdot_{E} (i \cdot_{E} j)) i = G (j) (i) \cdot_{E} (i \cdot_{E} j)$
285	280 284	eqtr2d	$⊢ ((φ \land j \in Y) \land i \in X) \to G (j) (i) \cdot_{E} (i \cdot_{E} j) = j (H {\cdot_{E}}_{f} D) i$
286	285	mpteq2dva	$⊢ (φ \land j \in Y) \to (i \in X ⟼ G (j) (i) \cdot_{E} (i \cdot_{E} j)) = (i \in X ⟼ j (H {\cdot_{E}}_{f} D) i)$
287	286	oveq2d	$⊢ (φ \land j \in Y) \to \underset{i \in X}{\sum_{E}} (G (j) (i) \cdot_{E} (i \cdot_{E} j)) = \underset{i \in X}{\sum_{E}} (j (H {\cdot_{E}}_{f} D) i)$
288	270 273 287	3eqtr3d	$⊢ (φ \land j \in Y) \to L (j) \cdot_{B} j = \underset{i \in X}{\sum_{E}} (j (H {\cdot_{E}}_{f} D) i)$
289	288	mpteq2dva	$⊢ φ \to (j \in Y ⟼ L (j) \cdot_{B} j) = (j \in Y ⟼ \underset{i \in X}{\sum_{E}} (j (H {\cdot_{E}}_{f} D) i))$
290	289	oveq2d	$⊢ φ \to \underset{j \in Y}{\sum_{E}} (L (j) \cdot_{B} j) = \underset{j \in Y}{\sum_{E}} (\underset{i \in X}{\sum_{E}}, (j (H {\cdot_{E}}_{f} D) i))$
291		ringcmn	$⊢ E \in Ring \to E \in CMnd$
292	79 291	syl	$⊢ φ \to E \in CMnd$
293	79	adantr	$⊢ (φ \land (l \in {Base}_{Scalar (A)} \land k \in {Base}_{A})) \to E \in Ring$
294	52 183	eqsstrd	$⊢ φ \to {Base}_{Scalar (A)} \subseteq {Base}_{E}$
295	294	adantr	$⊢ (φ \land (l \in {Base}_{Scalar (A)} \land k \in {Base}_{A})) \to {Base}_{Scalar (A)} \subseteq {Base}_{E}$
296		simprl	$⊢ (φ \land (l \in {Base}_{Scalar (A)} \land k \in {Base}_{A})) \to l \in {Base}_{Scalar (A)}$
297	295 296	sseldd	$⊢ (φ \land (l \in {Base}_{Scalar (A)} \land k \in {Base}_{A})) \to l \in {Base}_{E}$
298		simprr	$⊢ (φ \land (l \in {Base}_{Scalar (A)} \land k \in {Base}_{A})) \to k \in {Base}_{A}$
299	30 37	srabase	$⊢ φ \to {Base}_{E} = {Base}_{A}$
300	299	adantr	$⊢ (φ \land (l \in {Base}_{Scalar (A)} \land k \in {Base}_{A})) \to {Base}_{E} = {Base}_{A}$
301	298 300	eleqtrrd	$⊢ (φ \land (l \in {Base}_{Scalar (A)} \land k \in {Base}_{A})) \to k \in {Base}_{E}$
302	35 221	ringcl	$⊢ (E \in Ring \land l \in {Base}_{E} \land k \in {Base}_{E}) \to l \cdot_{E} k \in {Base}_{E}$
303	293 297 301 302	syl3anc	$⊢ (φ \land (l \in {Base}_{Scalar (A)} \land k \in {Base}_{A})) \to l \cdot_{E} k \in {Base}_{E}$
304	35 221	ringcl	$⊢ (E \in Ring \land i \in {Base}_{E} \land j \in {Base}_{E}) \to i \cdot_{E} j \in {Base}_{E}$
305	234 240 249 304	syl3anc	$⊢ ((φ \land j \in Y) \land i \in X) \to i \cdot_{E} j \in {Base}_{E}$
306	299	ad2antrr	$⊢ ((φ \land j \in Y) \land i \in X) \to {Base}_{E} = {Base}_{A}$
307	305 306	eleqtrd	$⊢ ((φ \land j \in Y) \land i \in X) \to i \cdot_{E} j \in {Base}_{A}$
308	307	anasss	$⊢ (φ \land (j \in Y \land i \in X)) \to i \cdot_{E} j \in {Base}_{A}$
309	308	ralrimivva	$⊢ φ \to \forall j \in Y \forall i \in X i \cdot_{E} j \in {Base}_{A}$
310	11	fmpo	$⊢ \forall j \in Y \forall i \in X i \cdot_{E} j \in {Base}_{A} \leftrightarrow D : Y \times X ⟶ {Base}_{A}$
311	309 310	sylib	$⊢ φ \to D : Y \times X ⟶ {Base}_{A}$
312		inidm	$⊢ (Y \times X) \cap (Y \times X) = Y \times X$
313	303 76 311 59 59 312	off	$⊢ φ \to (H {\cdot_{E}}_{f} D) : Y \times X ⟶ {Base}_{E}$
314	79	adantr	$⊢ (φ \land u \in {Base}_{A}) \to E \in Ring$
315		simpr	$⊢ (φ \land u \in {Base}_{A}) \to u \in {Base}_{A}$
316	299	adantr	$⊢ (φ \land u \in {Base}_{A}) \to {Base}_{E} = {Base}_{A}$
317	315 316	eleqtrrd	$⊢ (φ \land u \in {Base}_{A}) \to u \in {Base}_{E}$
318	35 221 81	ringlz	$⊢ (E \in Ring \land u \in {Base}_{E}) \to 0_{E} \cdot_{E} u = 0_{E}$
319	314 317 318	syl2anc	$⊢ (φ \land u \in {Base}_{A}) \to 0_{E} \cdot_{E} u = 0_{E}$
320	59 83 83 76 311 197 319	offinsupp1	$⊢ φ \to {finSupp}_{0_{E}} ((H {\cdot_{E}}_{f} D))$
321	35 81 292 14 13 313 320	gsumxp	$⊢ φ \to \sum_{E} (H {\cdot_{E}}_{f} D) = \underset{j \in Y}{\sum_{E}} (\underset{i \in X}{\sum_{E}}, (j (H {\cdot_{E}}_{f} D) i))$
322	30 37	sravsca	$⊢ φ \to \cdot_{E} = \cdot_{A}$
323		ofeq	$⊢ \cdot_{E} = \cdot_{A} \to \circ_{f} \cdot_{E} = \circ_{f} \cdot_{A}$
324	322 323	syl	$⊢ φ \to \circ_{f} \cdot_{E} = \circ_{f} \cdot_{A}$
325	324	oveqd	$⊢ φ \to H {\cdot_{E}}_{f} D = H {\cdot_{A}}_{f} D$
326	325	oveq2d	$⊢ φ \to \sum_{E} (H {\cdot_{E}}_{f} D) = \sum_{E} (H {\cdot_{A}}_{f} D)$
327	290 321 326	3eqtr2rd	$⊢ φ \to \sum_{E} (H {\cdot_{A}}_{f} D) = \underset{j \in Y}{\sum_{E}} (L (j) \cdot_{B} j)$
328		ovexd	$⊢ φ \to H {\cdot_{A}}_{f} D \in V$
329	15	elfvexd	$⊢ φ \to A \in V$
330	1 328 6 329 37	gsumsra	$⊢ φ \to \sum_{E} (H {\cdot_{A}}_{f} D) = \sum_{A} (H {\cdot_{A}}_{f} D)$
331	327 330	eqtr3d	$⊢ φ \to \underset{j \in Y}{\sum_{E}} (L (j) \cdot_{B} j) = \sum_{A} (H {\cdot_{A}}_{f} D)$
332	18 201 331	3eqtr2d	$⊢ φ \to Z = \sum_{A} (H {\cdot_{A}}_{f} D)$
333	200 332	jca	$⊢ φ \to ({finSupp}_{0_{Scalar (A)}} (H) \land Z = \sum_{A} (H {\cdot_{A}}_{f} D))$

Metamath Proof Explorer

Theorem fedgmullem1

Proof