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	89 88 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	12	adantr	$⊢ (φ \land a \in (G^{B})) \to B \in LBasis (subringAlg (J) (F))$
114	7	adantr	$⊢ (φ \land a \in (G^{B})) \to G \in SubDRing (L)$
115		simpr	$⊢ (φ \land a \in (G^{B})) \to a \in (G^{B})$
116	113 114 115	elmaprd	$⊢ (φ \land a \in (G^{B})) \to a : B ⟶ G$
117	116	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$
118	117	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$
119	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$
120	118 119	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$
121	120	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$
122	111 112 121	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})$
123		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$
124	121	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}))$
125		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)$
126	116	ffnd	$⊢ (φ \land a \in (G^{B})) \to a Fn B$
127	126	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$
128	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))$
129		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$
130		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$
131		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))$
132	131	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)$
133	130 132	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))$
134	127 128 129 133	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}$
135		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}$
136	134 135	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}$
137	136 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}$
138	122 123 124 125 137	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})))$
139		eqid	$⊢ (g \in H ⟼ if (g \in B, a (g), 0_{L})) = (g \in H ⟼ if (g \in B, a (g), 0_{L}))$
140		simpr	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \land g = f) \to g = f$
141		suppssdm	$⊢ a supp 0_{L} \subseteq dom a$
142	116	fdmd	$⊢ (φ \land a \in (G^{B})) \to dom a = B$
143	142	adantr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to dom a = B$
144	141 143	sseqtrid	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to a supp 0_{L} \subseteq B$
145	144	sselda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \to f \in B$
146	145	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$
147	140 146	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$
148	147	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)$
149		fveq2	$⊢ g = f \to a (g) = a (f)$
150	149	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)$
151	148 150	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)$
152	80	ad2antrr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to B \subseteq H$
153	144 152	sstrd	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to a supp 0_{L} \subseteq H$
154	153	sselda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \to f \in H$
155		fvexd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in {supp}_{0_{L}} (a)) \to a (f) \in V$
156	139 151 154 155	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)$
157	156	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$
158	157	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)$
159		fveq2	$⊢ f = v \to a (f) = a (v)$
160		id	$⊢ f = v \to f = v$
161	159 160	oveq12d	$⊢ f = v \to a (f) \cdot_{L} f = a (v) \cdot_{L} v$
162	161	cbvmptv	$⊢ (f \in {supp}_{0_{L}} (a) ⟼ a (f) \cdot_{L} f) = (v \in {supp}_{0_{L}} (a) ⟼ a (v) \cdot_{L} v)$
163	158 162	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)$
164	163	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)$
165	36	ad2antrr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to L \in CMnd$
166	8	ad2antrr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to H \in SubDRing (L)$
167		eleq1w	$⊢ g = f \to (g \in B \leftrightarrow f \in B)$
168	167 149	ifbieq1d	$⊢ g = f \to if (g \in B, a (g), 0_{L}) = if (f \in B, a (f), 0_{L})$
169		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))$
170	169	eldifad	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to f \in H$
171		fvexd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to a (f) \in V$
172		fvexd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to 0_{L} \in V$
173	171 172	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$
174	139 168 170 173	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})$
175	174	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$
176	126	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$
177	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))$
178		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$
179		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$
180		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))$
181	180	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)$
182	179 181	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))$
183	176 177 178 182	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}$
184		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}$
185	183 184	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}$
186	185	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$
187	35	ad3antrrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to L \in Ring$
188	166 22 70	3syl	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to H \subseteq {Base}_{L}$
189	188	ssdifssd	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to H ∖ {supp}_{0_{L}} (a) \subseteq {Base}_{L}$
190	189	sselda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in (H ∖ {supp}_{0_{L}} (a))) \to f \in {Base}_{L}$
191	16 17 18 187 190	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}$
192	175 186 191	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}$
193		simpr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to {finSupp}_{0_{L}} (a)$
194	193	fsuppimpd	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to a supp 0_{L} \in Fin$
195	35	ad3antrrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in H) \to L \in Ring$
196	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}$
197	116	ad2antrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land g \in H) \to a : B ⟶ G$
198	197	ffvelcdmda	$⊢ ((((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land g \in H) \land g \in B) \to a (g) \in G$
199	196 198	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}$
200	26 41	sseldd	$⊢ φ \to 0_{L} \in {Base}_{L}$
201	200	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}$
202	199 201	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}$
203	202	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}$
204	203	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}$
205	188	sselda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land f \in H) \to f \in {Base}_{L}$
206	16 17 195 204 205	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}$
207	16 18 165 166 192 194 206 153	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)$
208	113	adantr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to B \in LBasis (subringAlg (J) (F))$
209	126	ad2antrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to a Fn B$
210	208	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))$
211		fvexd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to 0_{L} \in V$
212		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))$
213	209 210 211 212	fvdifsupp	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to a (v) = 0_{L}$
214	213	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$
215	35	ad3antrrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to L \in Ring$
216	81	ad2antrr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to B \subseteq {Base}_{L}$
217	216	ssdifssd	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to B ∖ {supp}_{0_{L}} (a) \subseteq {Base}_{L}$
218	217	sselda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in (B ∖ {supp}_{0_{L}} (a))) \to v \in {Base}_{L}$
219	16 17 18 215 218	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}$
220	214 219	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}$
221	35	ad3antrrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in B) \to L \in Ring$
222	26	ad3antrrr	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in B) \to G \subseteq {Base}_{L}$
223	116	adantr	$⊢ ((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \to a : B ⟶ G$
224	223	ffvelcdmda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in B) \to a (v) \in G$
225	222 224	sseldd	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in B) \to a (v) \in {Base}_{L}$
226	216	sselda	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in B) \to v \in {Base}_{L}$
227	16 17 221 225 226	ringcld	$⊢ (((φ \land a \in (G^{B})) \land {finSupp}_{0_{L}} (a)) \land v \in B) \to a (v) \cdot_{L} v \in {Base}_{L}$
228	16 18 165 208 220 194 227 144	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)$
229	164 207 228	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)$
230	229	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))$
231	230	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)$
232	231	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)$
233	138 232	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))$
234	110 122 233	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))$
235	234	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))$
236	103 235	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)))$
237	59 84 236	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))$
238	15 24 237	3bitrd	$⊢ φ \to (x \in C \leftrightarrow x \in LSpan (subringAlg (L) (G)) (B))$
239	238	eqrdv	$⊢ φ \to C = LSpan (subringAlg (L) (G)) (B)$

Metamath Proof Explorer

Theorem fldextrspunlsp

Proof