fldextrspunlsp

Description: Lemma for fldextrspunfld . The subring generated by the union of two field extensions G and H is the vector sub- G space generated by a basis B of H . Part of the proof of Proposition 5, Chapter 5, of BourbakiAlg2 p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025)

	Ref	Expression
Hypotheses	fldextrspunfld.k	$⊢ K = L ↾_{𝑠} F$
	fldextrspunfld.i	$⊢ I = L ↾_{𝑠} G$
	fldextrspunfld.j	$⊢ J = L ↾_{𝑠} H$
	fldextrspunfld.2	$⊢ φ \to L \in Field$
	fldextrspunfld.3	$⊢ φ \to F \in SubDRing (I)$
	fldextrspunfld.4	$⊢ φ \to F \in SubDRing (J)$
	fldextrspunfld.5	$⊢ φ \to G \in SubDRing (L)$
	fldextrspunfld.6	$⊢ φ \to H \in SubDRing (L)$
	fldextrspunlsp.n	$⊢ N = RingSpan (L)$
	fldextrspunlsp.c	$⊢ C = N (G \cup H)$
	fldextrspunlsp.e	$⊢ E = L ↾_{𝑠} C$
	fldextrspunlsp.1	$⊢ φ \to B \in LBasis (subringAlg (J) (F))$
	fldextrspunlsp.2	$⊢ φ \to B \in Fin$
Assertion	fldextrspunlsp	$⊢ φ \to C = LSpan (subringAlg (L) (G)) (B)$

Proof

Step	Hyp	Ref	Expression
1		fldextrspunfld.k	$⊢ K = L ↾_{𝑠} F$
2		fldextrspunfld.i	$⊢ I = L ↾_{𝑠} G$
3		fldextrspunfld.j	$⊢ J = L ↾_{𝑠} H$
4		fldextrspunfld.2	$⊢ φ \to L \in Field$
5		fldextrspunfld.3	$⊢ φ \to F \in SubDRing (I)$
6		fldextrspunfld.4	$⊢ φ \to F \in SubDRing (J)$
7		fldextrspunfld.5	$⊢ φ \to G \in SubDRing (L)$
8		fldextrspunfld.6	$⊢ φ \to H \in SubDRing (L)$
9		fldextrspunlsp.n	$⊢ N = RingSpan (L)$
10		fldextrspunlsp.c	$⊢ C = N (G \cup H)$
11		fldextrspunlsp.e	$⊢ E = L ↾_{𝑠} C$
12		fldextrspunlsp.1	$⊢ φ \to B \in LBasis (subringAlg (J) (F))$
13		fldextrspunlsp.2	$⊢ φ \to B \in Fin$
14	10	a1i	$⊢ φ \to C = N (G \cup H)$
15	14	eleq2d	$⊢ φ \to (x \in C \leftrightarrow x \in N (G \cup H))$
16		eqid	$⊢ {Base}_{L} = {Base}_{L}$
17		eqid	$⊢ \cdot_{L} = \cdot_{L}$
18		eqid	$⊢ 0_{L} = 0_{L}$
19	4	fldcrngd	$⊢ φ \to L \in CRing$
20		sdrgsubrg	$⊢ G \in SubDRing (L) \to G \in SubRing (L)$
21	7 20	syl	$⊢ φ \to G \in SubRing (L)$
22		sdrgsubrg	$⊢ H \in SubDRing (L) \to H \in SubRing (L)$
23	8 22	syl	$⊢ φ \to H \in SubRing (L)$
24	16 17 18 9 19 21 23	elrgspnsubrun	$⊢ φ \to (x \in N (G \cup H) \leftrightarrow \exists p \in (G^{H}) ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f)))$
25	16	subrgss	$⊢ G \in SubRing (L) \to G \subseteq {Base}_{L}$
26	21 25	syl	$⊢ φ \to G \subseteq {Base}_{L}$
27		eqid	$⊢ L ↾_{𝑠} G = L ↾_{𝑠} G$
28	27 16	ressbas2	$⊢ G \subseteq {Base}_{L} \to G = {Base}_{(L ↾_{𝑠} G)}$
29	26 28	syl	$⊢ φ \to G = {Base}_{(L ↾_{𝑠} G)}$
30		eqidd	$⊢ φ \to subringAlg (L) (G) = subringAlg (L) (G)$
31	30 26	srasca	$⊢ φ \to L ↾_{𝑠} G = Scalar (subringAlg (L) (G))$
32	31	fveq2d	$⊢ φ \to {Base}_{(L ↾_{𝑠} G)} = {Base}_{Scalar (subringAlg (L) (G))}$
33	29 32	eqtr2d	$⊢ φ \to {Base}_{Scalar (subringAlg (L) (G))} = G$
34	33	oveq1d	$⊢ φ \to {Base}_{Scalar (subringAlg (L) (G))}^{B} = G^{B}$
35	19	crngringd	$⊢ φ \to L \in Ring$
36	35	ringcmnd	$⊢ φ \to L \in CMnd$
37	36	cmnmndd	$⊢ φ \to L \in Mnd$
38		subrgsubg	$⊢ G \in SubRing (L) \to G \in SubGrp (L)$
39	21 38	syl	$⊢ φ \to G \in SubGrp (L)$
40	18	subg0cl	$⊢ G \in SubGrp (L) \to 0_{L} \in G$
41	39 40	syl	$⊢ φ \to 0_{L} \in G$
42	27 16 18	ress0g	$⊢ (L \in Mnd \land 0_{L} \in G \land G \subseteq {Base}_{L}) \to 0_{L} = 0_{(L ↾_{𝑠} G)}$
43	37 41 26 42	syl3anc	$⊢ φ \to 0_{L} = 0_{(L ↾_{𝑠} G)}$
44	31	fveq2d	$⊢ φ \to 0_{(L ↾_{𝑠} G)} = 0_{Scalar (subringAlg (L) (G))}$
45	43 44	eqtr2d	$⊢ φ \to 0_{Scalar (subringAlg (L) (G))} = 0_{L}$
46	45	breq2d	$⊢ φ \to ({finSupp}_{0_{Scalar (subringAlg (L) (G))}} (a) \leftrightarrow {finSupp}_{0_{L}} (a))$
47		eqid	$⊢ subringAlg (L) (G) = subringAlg (L) (G)$
48	12	mptexd	$⊢ φ \to (v \in B ⟼ a (v) \cdot_{L} v) \in V$
49	47	sralmod	$⊢ G \in SubRing (L) \to subringAlg (L) (G) \in LMod$
50	21 49	syl	$⊢ φ \to subringAlg (L) (G) \in LMod$
51	47 48 4 50 26	gsumsra	$⊢ φ \to \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v) = \underset{v \in B}{\sum_{subringAlg (L) (G)}} (a (v) \cdot_{L} v)$
52	30 26	sravsca	$⊢ φ \to \cdot_{L} = \cdot_{subringAlg (L) (G)}$
53	52	oveqd	$⊢ φ \to a (v) \cdot_{L} v = a (v) \cdot_{subringAlg (L) (G)} v$
54	53	mpteq2dv	$⊢ φ \to (v \in B ⟼ a (v) \cdot_{L} v) = (v \in B ⟼ a (v) \cdot_{subringAlg (L) (G)} v)$
55	54	oveq2d	$⊢ φ \to \underset{v \in B}{\sum_{subringAlg (L) (G)}} (a (v) \cdot_{L} v) = \underset{v \in B}{\sum_{subringAlg (L) (G)}} (a (v) \cdot_{subringAlg (L) (G)} v)$
56	51 55	eqtr2d	$⊢ φ \to \underset{v \in B}{\sum_{subringAlg (L) (G)}} (a (v) \cdot_{subringAlg (L) (G)} v) = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v)$
57	56	eqeq2d	$⊢ φ \to (x = \underset{v \in B}{\sum_{subringAlg (L) (G)}} (a (v) \cdot_{subringAlg (L) (G)} v) \leftrightarrow x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))$
58	46 57	anbi12d	$⊢ φ \to (({finSupp}_{0_{Scalar (subringAlg (L) (G))}} (a) \land x = \underset{v \in B}{\sum_{subringAlg (L) (G)}} (a (v) \cdot_{subringAlg (L) (G)} v)) \leftrightarrow ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v)))$
59	34 58	rexeqbidv	$⊢ φ \to (\exists a \in ({Base}_{Scalar (subringAlg (L) (G))}^{B}) ({finSupp}_{0_{Scalar (subringAlg (L) (G))}} (a) \land x = \underset{v \in B}{\sum_{subringAlg (L) (G)}} (a (v) \cdot_{subringAlg (L) (G)} v)) \leftrightarrow \exists a \in (G^{B}) ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v)))$
60		eqid	$⊢ LSpan (subringAlg (L) (G)) = LSpan (subringAlg (L) (G))$
61		eqid	$⊢ {Base}_{subringAlg (L) (G)} = {Base}_{subringAlg (L) (G)}$
62		eqid	$⊢ {Base}_{Scalar (subringAlg (L) (G))} = {Base}_{Scalar (subringAlg (L) (G))}$
63		eqid	$⊢ Scalar (subringAlg (L) (G)) = Scalar (subringAlg (L) (G))$
64		eqid	$⊢ 0_{Scalar (subringAlg (L) (G))} = 0_{Scalar (subringAlg (L) (G))}$
65		eqid	$⊢ \cdot_{subringAlg (L) (G)} = \cdot_{subringAlg (L) (G)}$
66		eqid	$⊢ {Base}_{subringAlg (J) (F)} = {Base}_{subringAlg (J) (F)}$
67		eqid	$⊢ LBasis (subringAlg (J) (F)) = LBasis (subringAlg (J) (F))$
68	66 67	lbsss	$⊢ B \in LBasis (subringAlg (J) (F)) \to B \subseteq {Base}_{subringAlg (J) (F)}$
69	12 68	syl	$⊢ φ \to B \subseteq {Base}_{subringAlg (J) (F)}$
70	16	subrgss	$⊢ H \in SubRing (L) \to H \subseteq {Base}_{L}$
71	23 70	syl	$⊢ φ \to H \subseteq {Base}_{L}$
72	3 16	ressbas2	$⊢ H \subseteq {Base}_{L} \to H = {Base}_{J}$
73	71 72	syl	$⊢ φ \to H = {Base}_{J}$
74		eqidd	$⊢ φ \to subringAlg (J) (F) = subringAlg (J) (F)$
75		eqid	$⊢ {Base}_{J} = {Base}_{J}$
76	75	sdrgss	$⊢ F \in SubDRing (J) \to F \subseteq {Base}_{J}$
77	6 76	syl	$⊢ φ \to F \subseteq {Base}_{J}$
78	74 77	srabase	$⊢ φ \to {Base}_{J} = {Base}_{subringAlg (J) (F)}$
79	73 78	eqtrd	$⊢ φ \to H = {Base}_{subringAlg (J) (F)}$
80	69 79	sseqtrrd	$⊢ φ \to B \subseteq H$
81	80 71	sstrd	$⊢ φ \to B \subseteq {Base}_{L}$
82	30 26	srabase	$⊢ φ \to {Base}_{L} = {Base}_{subringAlg (L) (G)}$
83	81 82	sseqtrd	$⊢ φ \to B \subseteq {Base}_{subringAlg (L) (G)}$
84	60 61 62 63 64 65 50 83	ellspds	$⊢ φ \to (x \in LSpan (subringAlg (L) (G)) (B) \leftrightarrow \exists a \in ({Base}_{Scalar (subringAlg (L) (G))}^{B}) ({finSupp}_{0_{Scalar (subringAlg (L) (G))}} (a) \land x = \underset{v \in B}{\sum_{subringAlg (L) (G)}} (a (v) \cdot_{subringAlg (L) (G)} v)))$
85	4	ad2antrr	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to L \in Field$
86	5	ad2antrr	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to F \in SubDRing (I)$
87	6	ad2antrr	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to F \in SubDRing (J)$
88	7	ad2antrr	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to G \in SubDRing (L)$
89	8	ad2antrr	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to H \in SubDRing (L)$
90	12	ad2antrr	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to B \in LBasis (subringAlg (J) (F))$
91	13	ad2antrr	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to B \in Fin$
92		simplr	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to p \in (G^{H})$
93	92	elmaprd	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to p : H ⟶ G$
94		simprl	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to {finSupp}_{0_{L}} (p)$
95		simprr	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f)$
96		fveq2	$⊢ f = h \to p (f) = p (h)$
97		id	$⊢ f = h \to f = h$
98	96 97	oveq12d	$⊢ f = h \to p (f) \cdot_{L} f = p (h) \cdot_{L} h$
99	98	cbvmptv	$⊢ (f \in H ⟼ p (f) \cdot_{L} f) = (h \in H ⟼ p (h) \cdot_{L} h)$
100	99	oveq2i	$⊢ \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f) = \underset{h \in H}{\sum_{L}} (p (h) \cdot_{L} h)$
101	95 100	eqtrdi	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to x = \underset{h \in H}{\sum_{L}} (p (h) \cdot_{L} h)$
102	1 2 3 85 86 87 88 89 9 10 11 90 91 93 94 101	fldextrspunlsplem	$⊢ ((φ \land p \in (G^{H})) \land ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to \exists a \in (G^{B}) ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))$
103	102	r19.29an	$⊢ (φ \land \exists p \in (G^{H}) ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))) \to \exists a \in (G^{B}) ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))$
104		breq1	$⊢ p = (g \in H ⟼ if (g \in B, a (g), 0_{L})) \to ({finSupp}_{0_{L}} (p) \leftrightarrow {finSupp}_{0_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L}))))$
105		fveq1	$⊢ p = (g \in H ⟼ if (g \in B, a (g), 0_{L})) \to p (f) = (g \in H ⟼ if (g \in B, a (g), 0_{L})) (f)$
106	105	oveq1d	$⊢ p = (g \in H ⟼ if (g \in B, a (g), 0_{L})) \to p (f) \cdot_{L} f = (g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f$
107	106	mpteq2dv	$⊢ p = (g \in H ⟼ if (g \in B, a (g), 0_{L})) \to (f \in H ⟼ p (f) \cdot_{L} f) = (f \in H ⟼ (g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f)$
108	107	oveq2d	$⊢ p = (g \in H ⟼ if (g \in B, a (g), 0_{L})) \to \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f) = \underset{f \in H}{\sum_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f)$
109	108	eqeq2d	$⊢ p = (g \in H ⟼ if (g \in B, a (g), 0_{L})) \to (x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f) \leftrightarrow x = \underset{f \in H}{\sum_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f))$
110	104 109	anbi12d	$⊢ p = (g \in H ⟼ if (g \in B, a (g), 0_{L})) \to (({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f)) \leftrightarrow ({finSupp}_{0_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L}))) \land x = \underset{f \in H}{\sum_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f)))$
111	7	ad2antrr	$⊢ ((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to G \in SubDRing (L)$
112	8	ad2antrr	$⊢ ((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to H \in SubDRing (L)$
113		simpr	$⊢ (φ \land a \in (G^{B})) \to a \in (G^{B})$
114	113	elmaprd	$⊢ (φ \land a \in (G^{B})) \to a : B ⟶ G$
115	114	ad2antrr	$⊢ (((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in H) \to a : B ⟶ G$
116	115	ffvelcdmda	$⊢ ((((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in H) \land g \in B) \to a (g) \in G$
117	41	ad4antr	$⊢ ((((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in H) \land \neg g \in B) \to 0_{L} \in G$
118	116 117	ifclda	$⊢ (((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in H) \to if (g \in B, a (g), 0_{L}) \in G$
119	118	fmpttd	$⊢ ((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to (g \in H ⟼ if (g \in B, a (g), 0_{L})) : H ⟶ G$
120	111 112 119	elmapdd	$⊢ ((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to (g \in H ⟼ if (g \in B, a (g), 0_{L})) \in (G^{H})$
121		fvexd	$⊢ ((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to 0_{L} \in V$
122	119	ffund	$⊢ ((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to Fun (g \in H ⟼ if (g \in B, a (g), 0_{L}))$
123		simprl	$⊢ ((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to {finSupp}_{0_{L}} (a)$
124	114	ffnd	$⊢ (φ \land a \in (G^{B})) \to a Fn B$
125	124	ad3antrrr	$⊢ ((((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in (H ∖ {supp}_{0_{L}} (a))) \land g \in B) \to a Fn B$
126	12	ad4antr	$⊢ ((((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in (H ∖ {supp}_{0_{L}} (a))) \land g \in B) \to B \in LBasis (subringAlg (J) (F))$
127		fvexd	$⊢ ((((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in (H ∖ {supp}_{0_{L}} (a))) \land g \in B) \to 0_{L} \in V$
128		simpr	$⊢ ((((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in (H ∖ {supp}_{0_{L}} (a))) \land g \in B) \to g \in B$
129		simplr	$⊢ ((((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in (H ∖ {supp}_{0_{L}} (a))) \land g \in B) \to g \in (H ∖ {supp}_{0_{L}} (a))$
130	129	eldifbd	$⊢ ((((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in (H ∖ {supp}_{0_{L}} (a))) \land g \in B) \to \neg g \in {supp}_{0_{L}} (a)$
131	128 130	eldifd	$⊢ ((((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in (H ∖ {supp}_{0_{L}} (a))) \land g \in B) \to g \in (B ∖ {supp}_{0_{L}} (a))$
132	125 126 127 131	fvdifsupp	$⊢ ((((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in (H ∖ {supp}_{0_{L}} (a))) \land g \in B) \to a (g) = 0_{L}$
133		eqidd	$⊢ ((((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in (H ∖ {supp}_{0_{L}} (a))) \land \neg g \in B) \to 0_{L} = 0_{L}$
134	132 133	ifeqda	$⊢ (((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \land g \in (H ∖ {supp}_{0_{L}} (a))) \to if (g \in B, a (g), 0_{L}) = 0_{L}$
135	134 112	suppss2	$⊢ ((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to (g \in H ⟼ if (g \in B, a (g), 0_{L})) supp 0_{L} \subseteq a supp 0_{L}$
136	120 121 122 123 135	fsuppsssuppgd	$⊢ ((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to {finSupp}_{0_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L})))$
137		eqid	$⊢ (g \in H ⟼ if (g \in B, a (g), 0_{L})) = (g \in H ⟼ if (g \in B, a (g), 0_{L}))$
138		simpr	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \land g = f) \to g = f$
139		suppssdm	$⊢ a supp 0_{L} \subseteq dom a$
140	114	fdmd	$⊢ (φ \land a \in (G^{B})) \to dom a = B$
141	140	adantr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to dom a = B$
142	139 141	sseqtrid	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to a supp 0_{L} \subseteq B$
143	142	sselda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \to f \in B$
144	143	adantr	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \land g = f) \to f \in B$
145	138 144	eqeltrd	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \land g = f) \to g \in B$
146	145	iftrued	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \land g = f) \to if (g \in B, a (g), 0_{L}) = a (g)$
147		fveq2	$⊢ g = f \to a (g) = a (f)$
148	147	adantl	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \land g = f) \to a (g) = a (f)$
149	146 148	eqtrd	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \land g = f) \to if (g \in B, a (g), 0_{L}) = a (f)$
150	80	ad2antrr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to B \subseteq H$
151	142 150	sstrd	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to a supp 0_{L} \subseteq H$
152	151	sselda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \to f \in H$
153		fvexd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \to a (f) \in V$
154	137 149 152 153	fvmptd2	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \to (g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) = a (f)$
155	154	oveq1d	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \to (g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f = a (f) \cdot_{L} f$
156	155	mpteq2dva	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to (f \in {supp}_{0_{L}} (a) ⟼ (g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f) = (f \in {supp}_{0_{L}} (a) ⟼ a (f) \cdot_{L} f)$
157		fveq2	$⊢ f = v \to a (f) = a (v)$
158		id	$⊢ f = v \to f = v$
159	157 158	oveq12d	$⊢ f = v \to a (f) \cdot_{L} f = a (v) \cdot_{L} v$
160	159	cbvmptv	$⊢ (f \in {supp}_{0_{L}} (a) ⟼ a (f) \cdot_{L} f) = (v \in {supp}_{0_{L}} (a) ⟼ a (v) \cdot_{L} v)$
161	156 160	eqtrdi	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to (f \in {supp}_{0_{L}} (a) ⟼ (g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f) = (v \in {supp}_{0_{L}} (a) ⟼ a (v) \cdot_{L} v)$
162	161	oveq2d	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to \underset{f \in a supp 0_{L}}{\sum_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f) = \underset{v \in a supp 0_{L}}{\sum_{L}} (a (v) \cdot_{L} v)$
163	36	ad2antrr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to L \in CMnd$
164	8	ad2antrr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to H \in SubDRing (L)$
165		eleq1w	$⊢ g = f \to (g \in B \leftrightarrow f \in B)$
166	165 147	ifbieq1d	$⊢ g = f \to if (g \in B, a (g), 0_{L}) = if (f \in B, a (f), 0_{L})$
167		simpr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to f \in (H ∖ {supp}_{0_{L}} (a))$
168	167	eldifad	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to f \in H$
169		fvexd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to a (f) \in V$
170		fvexd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to 0_{L} \in V$
171	169 170	ifcld	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to if (f \in B, a (f), 0_{L}) \in V$
172	137 166 168 171	fvmptd3	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to (g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) = if (f \in B, a (f), 0_{L})$
173	172	oveq1d	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to (g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f = if (f \in B, a (f), 0_{L}) \cdot_{L} f$
174	124	ad3antrrr	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \land f \in B) \to a Fn B$
175	12	ad4antr	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \land f \in B) \to B \in LBasis (subringAlg (J) (F))$
176		fvexd	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \land f \in B) \to 0_{L} \in V$
177		simpr	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \land f \in B) \to f \in B$
178		simplr	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \land f \in B) \to f \in (H ∖ {supp}_{0_{L}} (a))$
179	178	eldifbd	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \land f \in B) \to \neg f \in {supp}_{0_{L}} (a)$
180	177 179	eldifd	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \land f \in B) \to f \in (B ∖ {supp}_{0_{L}} (a))$
181	174 175 176 180	fvdifsupp	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \land f \in B) \to a (f) = 0_{L}$
182		eqidd	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \land \neg f \in B) \to 0_{L} = 0_{L}$
183	181 182	ifeqda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to if (f \in B, a (f), 0_{L}) = 0_{L}$
184	183	oveq1d	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to if (f \in B, a (f), 0_{L}) \cdot_{L} f = 0_{L} \cdot_{L} f$
185	35	ad3antrrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to L \in Ring$
186	164 22 70	3syl	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to H \subseteq {Base}_{L}$
187	186	ssdifssd	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to H ∖ {supp}_{0_{L}} (a) \subseteq {Base}_{L}$
188	187	sselda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to f \in {Base}_{L}$
189	16 17 18 185 188	ringlzd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to 0_{L} \cdot_{L} f = 0_{L}$
190	173 184 189	3eqtrd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to (g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f = 0_{L}$
191		simpr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to {finSupp}_{0_{L}} (a)$
192	191	fsuppimpd	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to a supp 0_{L} \in Fin$
193	35	ad3antrrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in H) \to L \in Ring$
194	26	ad4antr	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land g \in H) \land g \in B) \to G \subseteq {Base}_{L}$
195	114	ad2antrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land g \in H) \to a : B ⟶ G$
196	195	ffvelcdmda	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land g \in H) \land g \in B) \to a (g) \in G$
197	194 196	sseldd	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land g \in H) \land g \in B) \to a (g) \in {Base}_{L}$
198	26 41	sseldd	$⊢ φ \to 0_{L} \in {Base}_{L}$
199	198	ad4antr	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land g \in H) \land \neg g \in B) \to 0_{L} \in {Base}_{L}$
200	197 199	ifclda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land g \in H) \to if (g \in B, a (g), 0_{L}) \in {Base}_{L}$
201	200	fmpttd	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to (g \in H ⟼ if (g \in B, a (g), 0_{L})) : H ⟶ {Base}_{L}$
202	201	ffvelcdmda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in H) \to (g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \in {Base}_{L}$
203	186	sselda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in H) \to f \in {Base}_{L}$
204	16 17 193 202 203	ringcld	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in H) \to (g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f \in {Base}_{L}$
205	16 18 163 164 190 192 204 151	gsummptres2	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to \underset{f \in H}{\sum_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f) = \underset{f \in a supp 0_{L}}{\sum_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f)$
206	12	adantr	$⊢ (φ \land a \in (G^{B})) \to B \in LBasis (subringAlg (J) (F))$
207	206	adantr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to B \in LBasis (subringAlg (J) (F))$
208	124	ad2antrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to a Fn B$
209	207	adantr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to B \in LBasis (subringAlg (J) (F))$
210		fvexd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to 0_{L} \in V$
211		simpr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to v \in (B ∖ {supp}_{0_{L}} (a))$
212	208 209 210 211	fvdifsupp	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to a (v) = 0_{L}$
213	212	oveq1d	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to a (v) \cdot_{L} v = 0_{L} \cdot_{L} v$
214	35	ad3antrrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to L \in Ring$
215	81	ad2antrr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to B \subseteq {Base}_{L}$
216	215	ssdifssd	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to B ∖ {supp}_{0_{L}} (a) \subseteq {Base}_{L}$
217	216	sselda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to v \in {Base}_{L}$
218	16 17 18 214 217	ringlzd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to 0_{L} \cdot_{L} v = 0_{L}$
219	213 218	eqtrd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to a (v) \cdot_{L} v = 0_{L}$
220	35	ad3antrrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in B) \to L \in Ring$
221	26	ad3antrrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in B) \to G \subseteq {Base}_{L}$
222	114	adantr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to a : B ⟶ G$
223	222	ffvelcdmda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in B) \to a (v) \in G$
224	221 223	sseldd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in B) \to a (v) \in {Base}_{L}$
225	215	sselda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in B) \to v \in {Base}_{L}$
226	16 17 220 224 225	ringcld	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in B) \to a (v) \cdot_{L} v \in {Base}_{L}$
227	16 18 163 207 219 192 226 142	gsummptres2	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v) = \underset{v \in a supp 0_{L}}{\sum_{L}} (a (v) \cdot_{L} v)$
228	162 205 227	3eqtr4d	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to \underset{f \in H}{\sum_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f) = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v)$
229	228	eqeq2d	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to (x = \underset{f \in H}{\sum_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f) \leftrightarrow x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))$
230	229	biimpar	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v)) \to x = \underset{f \in H}{\sum_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f)$
231	230	anasss	$⊢ ((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to x = \underset{f \in H}{\sum_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f)$
232	136 231	jca	$⊢ ((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to ({finSupp}_{0_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L}))) \land x = \underset{f \in H}{\sum_{L}} ((g \in H ⟼ if (g \in B, a (g), 0_{L})) (f) \cdot_{L} f))$
233	110 120 232	rspcedvdw	$⊢ ((φ \land a \in (G^{B})) \land ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to \exists p \in (G^{H}) ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))$
234	233	r19.29an	$⊢ (φ \land \exists a \in (G^{B}) ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v))) \to \exists p \in (G^{H}) ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f))$
235	103 234	impbida	$⊢ φ \to (\exists p \in (G^{H}) ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f)) \leftrightarrow \exists a \in (G^{B}) ({finSupp}_{0_{L}} (a) \land x = \underset{v \in B}{\sum_{L}} (a (v) \cdot_{L} v)))$
236	59 84 235	3bitr4rd	$⊢ φ \to (\exists p \in (G^{H}) ({finSupp}_{0_{L}} (p) \land x = \underset{f \in H}{\sum_{L}} (p (f) \cdot_{L} f)) \leftrightarrow x \in LSpan (subringAlg (L) (G)) (B))$
237	15 24 236	3bitrd	$⊢ φ \to (x \in C \leftrightarrow x \in LSpan (subringAlg (L) (G)) (B))$
238	237	eqrdv	$⊢ φ \to C = LSpan (subringAlg (L) (G)) (B)$

Metamath Proof Explorer

Theorem fldextrspunlsp

Proof