fldextrspunlsplem

Description: Lemma for fldextrspunlsp : First direction. 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$
	fldextrspunlsplem.2	$⊢ φ \to P : H ⟶ G$
	fldextrspunlsplem.3	$⊢ φ \to {finSupp}_{0_{L}} (P)$
	fldextrspunlsplem.4	$⊢ φ \to X = \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} f)$
Assertion	fldextrspunlsplem	$⊢ φ \to \exists a \in (G^{B}) ({finSupp}_{0_{L}} (a) \land X = \underset{b \in B}{\sum_{L}} (a (b) \cdot_{L} 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		fldextrspunlsplem.2	$⊢ φ \to P : H ⟶ G$
15		fldextrspunlsplem.3	$⊢ φ \to {finSupp}_{0_{L}} (P)$
16		fldextrspunlsplem.4	$⊢ φ \to X = \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} f)$
17	7	ad2antrr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to G \in SubDRing (L)$
18	12	ad2antrr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to B \in LBasis (subringAlg (J) (F))$
19		eqid	$⊢ 0_{L} = 0_{L}$
20	4	flddrngd	$⊢ φ \to L \in DivRing$
21	20	drngringd	$⊢ φ \to L \in Ring$
22	21	ringcmnd	$⊢ φ \to L \in CMnd$
23	22	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to L \in CMnd$
24	8	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to H \in SubDRing (L)$
25		sdrgsubrg	$⊢ G \in SubDRing (L) \to G \in SubRing (L)$
26	7 25	syl	$⊢ φ \to G \in SubRing (L)$
27		subrgsubg	$⊢ G \in SubRing (L) \to G \in SubGrp (L)$
28		subgsubm	$⊢ G \in SubGrp (L) \to G \in SubMnd (L)$
29	26 27 28	3syl	$⊢ φ \to G \in SubMnd (L)$
30	29	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to G \in SubMnd (L)$
31		eqid	$⊢ \cdot_{L} = \cdot_{L}$
32	26	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to G \in SubRing (L)$
33	14	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to P : H ⟶ G$
34		simpr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to f \in H$
35	33 34	ffvelcdmd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to P (f) \in G$
36		eqid	$⊢ {Base}_{I} = {Base}_{I}$
37	36	sdrgss	$⊢ F \in SubDRing (I) \to F \subseteq {Base}_{I}$
38	5 37	syl	$⊢ φ \to F \subseteq {Base}_{I}$
39		eqid	$⊢ {Base}_{L} = {Base}_{L}$
40	39	sdrgss	$⊢ G \in SubDRing (L) \to G \subseteq {Base}_{L}$
41	7 40	syl	$⊢ φ \to G \subseteq {Base}_{L}$
42	2 39	ressbas2	$⊢ G \subseteq {Base}_{L} \to G = {Base}_{I}$
43	41 42	syl	$⊢ φ \to G = {Base}_{I}$
44	38 43	sseqtrrd	$⊢ φ \to F \subseteq G$
45	44	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to F \subseteq G$
46	12	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to B \in LBasis (subringAlg (J) (F))$
47	5	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to F \in SubDRing (I)$
48	8	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to H \in SubDRing (L)$
49		ovexd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to F^{B} \in V$
50		simpllr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to u \in ({(F^{B})}^{H})$
51	48 49 50	elmaprd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to u : H ⟶ F^{B}$
52	51 34	ffvelcdmd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to u (f) \in (F^{B})$
53	46 47 52	elmaprd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to u (f) : B ⟶ F$
54		simplr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to c \in B$
55	53 54	ffvelcdmd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to u (f) (c) \in F$
56	45 55	sseldd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to u (f) (c) \in G$
57	31 32 35 56	subrgmcld	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to P (f) \cdot_{L} u (f) (c) \in G$
58	57	fmpttd	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \to (f \in H ⟼ P (f) \cdot_{L} u (f) (c)) : H ⟶ G$
59	58	adantlr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to (f \in H ⟼ P (f) \cdot_{L} u (f) (c)) : H ⟶ G$
60		fveq2	$⊢ f = h \to P (f) = P (h)$
61		fveq2	$⊢ f = h \to u (f) = u (h)$
62	61	fveq1d	$⊢ f = h \to u (f) (c) = u (h) (c)$
63	60 62	oveq12d	$⊢ f = h \to P (f) \cdot_{L} u (f) (c) = P (h) \cdot_{L} u (h) (c)$
64	63	cbvmptv	$⊢ (f \in H ⟼ P (f) \cdot_{L} u (f) (c)) = (h \in H ⟼ P (h) \cdot_{L} u (h) (c))$
65		fvexd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to 0_{L} \in V$
66		ssidd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to H \subseteq H$
67		eqid	$⊢ {Base}_{J} = {Base}_{J}$
68	67	sdrgss	$⊢ F \in SubDRing (J) \to F \subseteq {Base}_{J}$
69	6 68	syl	$⊢ φ \to F \subseteq {Base}_{J}$
70	39	sdrgss	$⊢ H \in SubDRing (L) \to H \subseteq {Base}_{L}$
71	8 70	syl	$⊢ φ \to H \subseteq {Base}_{L}$
72	3 39	ressbas2	$⊢ H \subseteq {Base}_{L} \to H = {Base}_{J}$
73	71 72	syl	$⊢ φ \to H = {Base}_{J}$
74	69 73	sseqtrrd	$⊢ φ \to F \subseteq H$
75	74 71	sstrd	$⊢ φ \to F \subseteq {Base}_{L}$
76	75	ad4antr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to F \subseteq {Base}_{L}$
77	12	ad4antr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to B \in LBasis (subringAlg (J) (F))$
78	6	ad4antr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to F \in SubDRing (J)$
79		ovexd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to F^{B} \in V$
80		simpllr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to u \in ({(F^{B})}^{H})$
81	24 79 80	elmaprd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to u : H ⟶ F^{B}$
82	81	ffvelcdmda	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to u (h) \in (F^{B})$
83	77 78 82	elmaprd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to u (h) : B ⟶ F$
84		simplr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to c \in B$
85	83 84	ffvelcdmd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to u (h) (c) \in F$
86	76 85	sseldd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to u (h) (c) \in {Base}_{L}$
87	14	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to P : H ⟶ G$
88	15	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to {finSupp}_{0_{L}} (P)$
89	21	ad4antr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land y \in {Base}_{L}) \to L \in Ring$
90		simpr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land y \in {Base}_{L}) \to y \in {Base}_{L}$
91	39 31 19 89 90	ringlzd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land y \in {Base}_{L}) \to 0_{L} \cdot_{L} y = 0_{L}$
92	65 65 24 66 86 87 88 91	fisuppov1	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to {finSupp}_{0_{L}} ((h \in H ⟼ P (h) \cdot_{L} u (h) (c)))$
93	64 92	eqbrtrid	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to {finSupp}_{0_{L}} ((f \in H ⟼ P (f) \cdot_{L} u (f) (c)))$
94	19 23 24 30 59 93	gsumsubmcl	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)) \in G$
95	94	fmpttd	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c))) : B ⟶ G$
96	17 18 95	elmapdd	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c))) \in (G^{B})$
97		breq1	$⊢ a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c))) \to ({finSupp}_{0_{L}} (a) \leftrightarrow {finSupp}_{0_{L}} ((c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))))$
98	97	adantl	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \to ({finSupp}_{0_{L}} (a) \leftrightarrow {finSupp}_{0_{L}} ((c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))))$
99		simplr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \land b \in B) \to a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))$
100	99	fveq1d	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \land b \in B) \to a (b) = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c))) (b)$
101		eqid	$⊢ (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c))) = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))$
102		fveq2	$⊢ c = b \to u (f) (c) = u (f) (b)$
103	102	oveq2d	$⊢ c = b \to P (f) \cdot_{L} u (f) (c) = P (f) \cdot_{L} u (f) (b)$
104	103	mpteq2dv	$⊢ c = b \to (f \in H ⟼ P (f) \cdot_{L} u (f) (c)) = (f \in H ⟼ P (f) \cdot_{L} u (f) (b))$
105	104	oveq2d	$⊢ c = b \to \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)) = \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (b))$
106		simpr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land b \in B) \to b \in B$
107		ovexd	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land b \in B) \to \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (b)) \in V$
108	101 105 106 107	fvmptd3	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land b \in B) \to (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c))) (b) = \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (b))$
109	108	adantlr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \land b \in B) \to (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c))) (b) = \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (b))$
110	100 109	eqtrd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \land b \in B) \to a (b) = \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (b))$
111	110	oveq1d	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \land b \in B) \to a (b) \cdot_{L} b = (\underset{f \in H}{\sum_{L}}, (P (f) \cdot_{L} u (f) (b))) \cdot_{L} b$
112	111	mpteq2dva	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \to (b \in B ⟼ a (b) \cdot_{L} b) = (b \in B ⟼ (\underset{f \in H}{\sum_{L}}, (P (f) \cdot_{L} u (f) (b))) \cdot_{L} b)$
113	112	oveq2d	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \to \underset{b \in B}{\sum_{L}} (a (b) \cdot_{L} b) = \underset{b \in B}{\sum_{L}} ((\underset{f \in H}{\sum_{L}}, (P (f) \cdot_{L} u (f) (b))) \cdot_{L} b)$
114	113	eqeq2d	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \to (X = \underset{b \in B}{\sum_{L}} (a (b) \cdot_{L} b) \leftrightarrow X = \underset{b \in B}{\sum_{L}} ((\underset{f \in H}{\sum_{L}}, (P (f) \cdot_{L} u (f) (b))) \cdot_{L} b))$
115	98 114	anbi12d	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \to (({finSupp}_{0_{L}} (a) \land X = \underset{b \in B}{\sum_{L}} (a (b) \cdot_{L} b)) \leftrightarrow ({finSupp}_{0_{L}} ((c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \land X = \underset{b \in B}{\sum_{L}} ((\underset{f \in H}{\sum_{L}}, (P (f) \cdot_{L} u (f) (b))) \cdot_{L} b)))$
116	115	adantlr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land a = (c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \to (({finSupp}_{0_{L}} (a) \land X = \underset{b \in B}{\sum_{L}} (a (b) \cdot_{L} b)) \leftrightarrow ({finSupp}_{0_{L}} ((c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \land X = \underset{b \in B}{\sum_{L}} ((\underset{f \in H}{\sum_{L}}, (P (f) \cdot_{L} u (f) (b))) \cdot_{L} b)))$
117	13	ad2antrr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to B \in Fin$
118		ovexd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)) \in V$
119		fvexd	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to 0_{L} \in V$
120	101 117 118 119	fsuppmptdm	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to {finSupp}_{0_{L}} ((c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c))))$
121	16	ad2antrr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to X = \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} f)$
122	21	ad2antrr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to L \in Ring$
123	122	adantr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to L \in Ring$
124	12	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to B \in LBasis (subringAlg (J) (F))$
125	41	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to G \subseteq {Base}_{L}$
126	14	ad2antrr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to P : H ⟶ G$
127	126	ffvelcdmda	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to P (h) \in G$
128	125 127	sseldd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to P (h) \in {Base}_{L}$
129	123	adantr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to L \in Ring$
130	75	ad4antr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to F \subseteq {Base}_{L}$
131	12	ad4antr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to B \in LBasis (subringAlg (J) (F))$
132	6	ad4antr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to F \in SubDRing (J)$
133	8	ad4antr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to H \in SubDRing (L)$
134		ovexd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to F^{B} \in V$
135		simp-4r	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to u \in ({(F^{B})}^{H})$
136	133 134 135	elmaprd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to u : H ⟶ F^{B}$
137		simplr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to h \in H$
138	136 137	ffvelcdmd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to u (h) \in (F^{B})$
139	131 132 138	elmaprd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to u (h) : B ⟶ F$
140		simpr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to c \in B$
141	139 140	ffvelcdmd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to u (h) (c) \in F$
142	130 141	sseldd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to u (h) (c) \in {Base}_{L}$
143		eqid	$⊢ {Base}_{subringAlg (J) (F)} = {Base}_{subringAlg (J) (F)}$
144		eqid	$⊢ LBasis (subringAlg (J) (F)) = LBasis (subringAlg (J) (F))$
145	143 144	lbsss	$⊢ B \in LBasis (subringAlg (J) (F)) \to B \subseteq {Base}_{subringAlg (J) (F)}$
146	12 145	syl	$⊢ φ \to B \subseteq {Base}_{subringAlg (J) (F)}$
147		eqidd	$⊢ φ \to subringAlg (J) (F) = subringAlg (J) (F)$
148	147 69	srabase	$⊢ φ \to {Base}_{J} = {Base}_{subringAlg (J) (F)}$
149	73 148	eqtr2d	$⊢ φ \to {Base}_{subringAlg (J) (F)} = H$
150	146 149	sseqtrd	$⊢ φ \to B \subseteq H$
151	150 71	sstrd	$⊢ φ \to B \subseteq {Base}_{L}$
152	151	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to B \subseteq {Base}_{L}$
153	152	sselda	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to c \in {Base}_{L}$
154	39 31 129 142 153	ringcld	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to u (h) (c) \cdot_{L} c \in {Base}_{L}$
155		fvexd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to 0_{L} \in V$
156		ssidd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to B \subseteq B$
157	6	ad3antrrr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to F \in SubDRing (J)$
158	8	ad2antrr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to H \in SubDRing (L)$
159		ovexd	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to F^{B} \in V$
160		simplr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to u \in ({(F^{B})}^{H})$
161	158 159 160	elmaprd	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to u : H ⟶ F^{B}$
162	161	ffvelcdmda	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to u (h) \in (F^{B})$
163	124 157 162	elmaprd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to u (h) : B ⟶ F$
164	61	breq1d	$⊢ f = h \to ({finSupp}_{0_{L}} (u (f)) \leftrightarrow {finSupp}_{0_{L}} (u (h)))$
165		id	$⊢ f = h \to f = h$
166	61	fveq1d	$⊢ f = h \to u (f) (b) = u (h) (b)$
167	166	oveq1d	$⊢ f = h \to u (f) (b) \cdot_{L} b = u (h) (b) \cdot_{L} b$
168	167	mpteq2dv	$⊢ f = h \to (b \in B ⟼ u (f) (b) \cdot_{L} b) = (b \in B ⟼ u (h) (b) \cdot_{L} b)$
169	168	oveq2d	$⊢ f = h \to \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b) = \underset{b \in B}{\sum_{L}} (u (h) (b) \cdot_{L} b)$
170	165 169	eqeq12d	$⊢ f = h \to (f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b) \leftrightarrow h = \underset{b \in B}{\sum_{L}} (u (h) (b) \cdot_{L} b))$
171	164 170	anbi12d	$⊢ f = h \to (({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b)) \leftrightarrow ({finSupp}_{0_{L}} (u (h)) \land h = \underset{b \in B}{\sum_{L}} (u (h) (b) \cdot_{L} b)))$
172		simplr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))$
173		simpr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to h \in H$
174	171 172 173	rspcdva	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to ({finSupp}_{0_{L}} (u (h)) \land h = \underset{b \in B}{\sum_{L}} (u (h) (b) \cdot_{L} b))$
175	174	simpld	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to {finSupp}_{0_{L}} (u (h))$
176	123	adantr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land y \in {Base}_{L}) \to L \in Ring$
177		simpr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land y \in {Base}_{L}) \to y \in {Base}_{L}$
178	39 31 19 176 177	ringlzd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land y \in {Base}_{L}) \to 0_{L} \cdot_{L} y = 0_{L}$
179	155 155 124 156 153 163 175 178	fisuppov1	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to {finSupp}_{0_{L}} ((c \in B ⟼ u (h) (c) \cdot_{L} c))$
180	39 19 31 123 124 128 154 179	gsummulc2	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to \underset{c \in B}{\sum_{L}} (P (h) \cdot_{L} (u (h) (c) \cdot_{L} c)) = P (h) \cdot_{L} (\underset{c \in B}{\sum_{L}}, (u (h) (c) \cdot_{L} c))$
181	128	adantr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to P (h) \in {Base}_{L}$
182	39 31 129 181 142 153	ringassd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \land c \in B) \to (P (h) \cdot_{L} u (h) (c)) \cdot_{L} c = P (h) \cdot_{L} (u (h) (c) \cdot_{L} c)$
183	182	mpteq2dva	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to (c \in B ⟼ (P (h) \cdot_{L} u (h) (c)) \cdot_{L} c) = (c \in B ⟼ P (h) \cdot_{L} (u (h) (c) \cdot_{L} c))$
184	183	oveq2d	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to \underset{c \in B}{\sum_{L}} ((P (h) \cdot_{L} u (h) (c)) \cdot_{L} c) = \underset{c \in B}{\sum_{L}} (P (h) \cdot_{L} (u (h) (c) \cdot_{L} c))$
185	174	simprd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to h = \underset{b \in B}{\sum_{L}} (u (h) (b) \cdot_{L} b)$
186		fveq2	$⊢ b = c \to u (h) (b) = u (h) (c)$
187		id	$⊢ b = c \to b = c$
188	186 187	oveq12d	$⊢ b = c \to u (h) (b) \cdot_{L} b = u (h) (c) \cdot_{L} c$
189	188	cbvmptv	$⊢ (b \in B ⟼ u (h) (b) \cdot_{L} b) = (c \in B ⟼ u (h) (c) \cdot_{L} c)$
190	189	oveq2i	$⊢ \underset{b \in B}{\sum_{L}} (u (h) (b) \cdot_{L} b) = \underset{c \in B}{\sum_{L}} (u (h) (c) \cdot_{L} c)$
191	185 190	eqtrdi	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to h = \underset{c \in B}{\sum_{L}} (u (h) (c) \cdot_{L} c)$
192	191	oveq2d	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to P (h) \cdot_{L} h = P (h) \cdot_{L} (\underset{c \in B}{\sum_{L}}, (u (h) (c) \cdot_{L} c))$
193	180 184 192	3eqtr4rd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land h \in H) \to P (h) \cdot_{L} h = \underset{c \in B}{\sum_{L}} ((P (h) \cdot_{L} u (h) (c)) \cdot_{L} c)$
194	193	mpteq2dva	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to (h \in H ⟼ P (h) \cdot_{L} h) = (h \in H ⟼ \underset{c \in B}{\sum_{L}} ((P (h) \cdot_{L} u (h) (c)) \cdot_{L} c))$
195	194	oveq2d	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to \underset{h \in H}{\sum_{L}} (P (h) \cdot_{L} h) = \underset{h \in H}{\sum_{L}} (\underset{c \in B}{\sum_{L}}, ((P (h) \cdot_{L} u (h) (c)) \cdot_{L} c))$
196	60 165	oveq12d	$⊢ f = h \to P (f) \cdot_{L} f = P (h) \cdot_{L} h$
197	196	cbvmptv	$⊢ (f \in H ⟼ P (f) \cdot_{L} f) = (h \in H ⟼ P (h) \cdot_{L} h)$
198	197	oveq2i	$⊢ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} f) = \underset{h \in H}{\sum_{L}} (P (h) \cdot_{L} h)$
199	198	a1i	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} f) = \underset{h \in H}{\sum_{L}} (P (h) \cdot_{L} h)$
200	22	ad2antrr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to L \in CMnd$
201	21	ad4antr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to L \in Ring$
202	41	ad4antr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to G \subseteq {Base}_{L}$
203	87	ffvelcdmda	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to P (h) \in G$
204	202 203	sseldd	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to P (h) \in {Base}_{L}$
205	39 31 201 204 86	ringcld	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to P (h) \cdot_{L} u (h) (c) \in {Base}_{L}$
206	151	ad2antrr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to B \subseteq {Base}_{L}$
207	206	sselda	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to c \in {Base}_{L}$
208	207	adantr	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to c \in {Base}_{L}$
209	39 31 201 205 208	ringcld	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \to (P (h) \cdot_{L} u (h) (c)) \cdot_{L} c \in {Base}_{L}$
210	209	anasss	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land (c \in B \land h \in H)) \to (P (h) \cdot_{L} u (h) (c)) \cdot_{L} c \in {Base}_{L}$
211	15	fsuppimpd	$⊢ φ \to P supp 0_{L} \in Fin$
212	211	ad2antrr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to P supp 0_{L} \in Fin$
213		suppssdm	$⊢ P supp 0_{L} \subseteq dom P$
214	213 14	fssdm	$⊢ φ \to P supp 0_{L} \subseteq H$
215	214	sseld	$⊢ φ \to (f \in {supp}_{0_{L}} (P) \to f \in H)$
216	215	adantr	$⊢ (φ \land u \in ({(F^{B})}^{H})) \to (f \in {supp}_{0_{L}} (P) \to f \in H)$
217		simpr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land {finSupp}_{0_{L}} (u (f))) \to {finSupp}_{0_{L}} (u (f))$
218	217	fsuppimpd	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land {finSupp}_{0_{L}} (u (f))) \to u (f) supp 0_{L} \in Fin$
219	218	ex	$⊢ (φ \land u \in ({(F^{B})}^{H})) \to ({finSupp}_{0_{L}} (u (f)) \to u (f) supp 0_{L} \in Fin)$
220	219	adantrd	$⊢ (φ \land u \in ({(F^{B})}^{H})) \to (({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b)) \to u (f) supp 0_{L} \in Fin)$
221	216 220	imim12d	$⊢ (φ \land u \in ({(F^{B})}^{H})) \to ((f \in H \to ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to (f \in {supp}_{0_{L}} (P) \to u (f) supp 0_{L} \in Fin))$
222	221	ralimdv2	$⊢ (φ \land u \in ({(F^{B})}^{H})) \to (\forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b)) \to \forall f \in {supp}_{0_{L}} (P) u (f) supp 0_{L} \in Fin)$
223	222	imp	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to \forall f \in {supp}_{0_{L}} (P) u (f) supp 0_{L} \in Fin$
224		fveq2	$⊢ f = i \to u (f) = u (i)$
225	224	oveq1d	$⊢ f = i \to u (f) supp 0_{L} = u (i) supp 0_{L}$
226	225	eleq1d	$⊢ f = i \to (u (f) supp 0_{L} \in Fin \leftrightarrow u (i) supp 0_{L} \in Fin)$
227	226	cbvralvw	$⊢ \forall f \in {supp}_{0_{L}} (P) u (f) supp 0_{L} \in Fin \leftrightarrow \forall i \in {supp}_{0_{L}} (P) u (i) supp 0_{L} \in Fin$
228	223 227	sylib	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to \forall i \in {supp}_{0_{L}} (P) u (i) supp 0_{L} \in Fin$
229		iunfi	$⊢ (P supp 0_{L} \in Fin \land \forall i \in {supp}_{0_{L}} (P) u (i) supp 0_{L} \in Fin) \to ⋃_{i \in P supp 0_{L}} {supp}_{0_{L}} (u (i)) \in Fin$
230	212 228 229	syl2anc	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to ⋃_{i \in P supp 0_{L}} {supp}_{0_{L}} (u (i)) \in Fin$
231		xpfi	$⊢ (⋃_{i \in P supp 0_{L}} {supp}_{0_{L}} (u (i)) \in Fin \land P supp 0_{L} \in Fin) \to ⋃_{i \in P supp 0_{L}} {supp}_{0_{L}} (u (i)) \times {supp}_{0_{L}} (P) \in Fin$
232	230 212 231	syl2anc	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to ⋃_{i \in P supp 0_{L}} {supp}_{0_{L}} (u (i)) \times {supp}_{0_{L}} (P) \in Fin$
233		snssi	$⊢ i \in {supp}_{0_{L}} (P) \to \{i\} \subseteq P supp 0_{L}$
234	233	adantl	$⊢ (φ \land i \in {supp}_{0_{L}} (P)) \to \{i\} \subseteq P supp 0_{L}$
235	234	iunxpssiun1	$⊢ φ \to ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) \subseteq ⋃_{i \in P supp 0_{L}} {supp}_{0_{L}} (u (i)) \times {supp}_{0_{L}} (P)$
236	235	ad2antrr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) \subseteq ⋃_{i \in P supp 0_{L}} {supp}_{0_{L}} (u (i)) \times {supp}_{0_{L}} (P)$
237	232 236	ssfid	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) \in Fin$
238	14	ffnd	$⊢ φ \to P Fn H$
239	238	ad6antr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to P Fn H$
240	8	ad6antr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to H \in SubDRing (L)$
241		fvexd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to 0_{L} \in V$
242		simpllr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to h \in H$
243		simpr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to \neg h \in {supp}_{0_{L}} (P)$
244	242 243	eldifd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to h \in (H ∖ {supp}_{0_{L}} (P))$
245	239 240 241 244	fvdifsupp	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to P (h) = 0_{L}$
246	245	oveq1d	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to P (h) \cdot_{L} u (h) (c) = 0_{L} \cdot_{L} u (h) (c)$
247	21	ad6antr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to L \in Ring$
248	75	ad6antr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to F \subseteq {Base}_{L}$
249	12	ad6antr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to B \in LBasis (subringAlg (J) (F))$
250	6	ad6antr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to F \in SubDRing (J)$
251		ovexd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to F^{B} \in V$
252		simp-6r	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to u \in ({(F^{B})}^{H})$
253	240 251 252	elmaprd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to u : H ⟶ F^{B}$
254	253 242	ffvelcdmd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to u (h) \in (F^{B})$
255	249 250 254	elmaprd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to u (h) : B ⟶ F$
256		simp-4r	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to c \in B$
257	255 256	ffvelcdmd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to u (h) (c) \in F$
258	248 257	sseldd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to u (h) (c) \in {Base}_{L}$
259	39 31 19 247 258	ringlzd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to 0_{L} \cdot_{L} u (h) (c) = 0_{L}$
260	246 259	eqtrd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg h \in {supp}_{0_{L}} (P)) \to P (h) \cdot_{L} u (h) (c) = 0_{L}$
261	12	ad6antr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to B \in LBasis (subringAlg (J) (F))$
262	6	ad6antr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to F \in SubDRing (J)$
263	8	ad6antr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to H \in SubDRing (L)$
264		ovexd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to F^{B} \in V$
265		simp-6r	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to u \in ({(F^{B})}^{H})$
266	263 264 265	elmaprd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to u : H ⟶ F^{B}$
267		simpllr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to h \in H$
268	266 267	ffvelcdmd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to u (h) \in (F^{B})$
269	261 262 268	elmaprd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to u (h) : B ⟶ F$
270	269	ffnd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to u (h) Fn B$
271		fvexd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to 0_{L} \in V$
272		simp-4r	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to c \in B$
273		simpr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to \neg c \in {supp}_{0_{L}} (u (h))$
274	272 273	eldifd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to c \in (B ∖ {supp}_{0_{L}} (u (h)))$
275	270 261 271 274	fvdifsupp	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to u (h) (c) = 0_{L}$
276	275	oveq2d	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to P (h) \cdot_{L} u (h) (c) = P (h) \cdot_{L} 0_{L}$
277	201	ad2antrr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to L \in Ring$
278	204	ad2antrr	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to P (h) \in {Base}_{L}$
279	39 31 19 277 278	ringrzd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to P (h) \cdot_{L} 0_{L} = 0_{L}$
280	276 279	eqtrd	$⊢ ((((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land \neg c \in {supp}_{0_{L}} (u (h))) \to P (h) \cdot_{L} u (h) (c) = 0_{L}$
281		df-br	$⊢ c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h \leftrightarrow ⟨c, h⟩ \in ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\})$
282		fveq2	$⊢ h = i \to u (h) = u (i)$
283	282	oveq1d	$⊢ h = i \to u (h) supp 0_{L} = u (i) supp 0_{L}$
284		sneq	$⊢ h = i \to \{h\} = \{i\}$
285	283 284	xpeq12d	$⊢ h = i \to {supp}_{0_{L}} (u (h)) \times \{h\} = {supp}_{0_{L}} (u (i)) \times \{i\}$
286	285	cbviunv	$⊢ ⋃_{h \in P supp 0_{L}} ({supp}_{0_{L}} (u (h)) \times \{h\}) = ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\})$
287	286	eleq2i	$⊢ ⟨c, h⟩ \in ⋃_{h \in P supp 0_{L}} ({supp}_{0_{L}} (u (h)) \times \{h\}) \leftrightarrow ⟨c, h⟩ \in ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\})$
288		opeliun2xp	$⊢ ⟨c, h⟩ \in ⋃_{h \in P supp 0_{L}} ({supp}_{0_{L}} (u (h)) \times \{h\}) \leftrightarrow (h \in {supp}_{0_{L}} (P) \land c \in {supp}_{0_{L}} (u (h)))$
289	281 287 288	3bitr2i	$⊢ c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h \leftrightarrow (h \in {supp}_{0_{L}} (P) \land c \in {supp}_{0_{L}} (u (h)))$
290	289	notbii	$⊢ \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h \leftrightarrow \neg (h \in {supp}_{0_{L}} (P) \land c \in {supp}_{0_{L}} (u (h)))$
291		ianor	$⊢ \neg (h \in {supp}_{0_{L}} (P) \land c \in {supp}_{0_{L}} (u (h))) \leftrightarrow (\neg h \in {supp}_{0_{L}} (P) \lor \neg c \in {supp}_{0_{L}} (u (h)))$
292	290 291	sylbb	$⊢ \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h \to (\neg h \in {supp}_{0_{L}} (P) \lor \neg c \in {supp}_{0_{L}} (u (h)))$
293	292	adantl	$⊢ (((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \to (\neg h \in {supp}_{0_{L}} (P) \lor \neg c \in {supp}_{0_{L}} (u (h)))$
294	260 280 293	mpjaodan	$⊢ (((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \to P (h) \cdot_{L} u (h) (c) = 0_{L}$
295	294	oveq1d	$⊢ (((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \to (P (h) \cdot_{L} u (h) (c)) \cdot_{L} c = 0_{L} \cdot_{L} c$
296	122	ad3antrrr	$⊢ (((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \to L \in Ring$
297	207	ad2antrr	$⊢ (((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \to c \in {Base}_{L}$
298	39 31 19 296 297	ringlzd	$⊢ (((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \to 0_{L} \cdot_{L} c = 0_{L}$
299	295 298	eqtrd	$⊢ (((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \to (P (h) \cdot_{L} u (h) (c)) \cdot_{L} c = 0_{L}$
300	299	an42ds	$⊢ (((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land h \in H) \land c \in B) \to (P (h) \cdot_{L} u (h) (c)) \cdot_{L} c = 0_{L}$
301	300	an32s	$⊢ (((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land c \in B) \land h \in H) \to (P (h) \cdot_{L} u (h) (c)) \cdot_{L} c = 0_{L}$
302	301	anasss	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \land (c \in B \land h \in H)) \to (P (h) \cdot_{L} u (h) (c)) \cdot_{L} c = 0_{L}$
303	302	an32s	$⊢ ((((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land (c \in B \land h \in H)) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h) \to (P (h) \cdot_{L} u (h) (c)) \cdot_{L} c = 0_{L}$
304	303	anasss	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land ((c \in B \land h \in H) \land \neg c ⋃_{i \in P supp 0_{L}} ({supp}_{0_{L}} (u (i)) \times \{i\}) h)) \to (P (h) \cdot_{L} u (h) (c)) \cdot_{L} c = 0_{L}$
305	39 19 200 18 158 210 237 304	gsumcom3	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to \underset{c \in B}{\sum_{L}} (\underset{h \in H}{\sum_{L}}, ((P (h) \cdot_{L} u (h) (c)) \cdot_{L} c)) = \underset{h \in H}{\sum_{L}} (\underset{c \in B}{\sum_{L}}, ((P (h) \cdot_{L} u (h) (c)) \cdot_{L} c))$
306	195 199 305	3eqtr4d	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} f) = \underset{c \in B}{\sum_{L}} (\underset{h \in H}{\sum_{L}}, ((P (h) \cdot_{L} u (h) (c)) \cdot_{L} c))$
307	122	adantr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to L \in Ring$
308	39 19 31 307 24 207 205 92	gsummulc1	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \land c \in B) \to \underset{h \in H}{\sum_{L}} ((P (h) \cdot_{L} u (h) (c)) \cdot_{L} c) = (\underset{h \in H}{\sum_{L}}, (P (h) \cdot_{L} u (h) (c))) \cdot_{L} c$
309	308	mpteq2dva	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to (c \in B ⟼ \underset{h \in H}{\sum_{L}} ((P (h) \cdot_{L} u (h) (c)) \cdot_{L} c)) = (c \in B ⟼ (\underset{h \in H}{\sum_{L}}, (P (h) \cdot_{L} u (h) (c))) \cdot_{L} c)$
310	309	oveq2d	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to \underset{c \in B}{\sum_{L}} (\underset{h \in H}{\sum_{L}}, ((P (h) \cdot_{L} u (h) (c)) \cdot_{L} c)) = \underset{c \in B}{\sum_{L}} ((\underset{h \in H}{\sum_{L}}, (P (h) \cdot_{L} u (h) (c))) \cdot_{L} c)$
311	121 306 310	3eqtrd	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to X = \underset{c \in B}{\sum_{L}} ((\underset{h \in H}{\sum_{L}}, (P (h) \cdot_{L} u (h) (c))) \cdot_{L} c)$
312	60 166	oveq12d	$⊢ f = h \to P (f) \cdot_{L} u (f) (b) = P (h) \cdot_{L} u (h) (b)$
313	312	cbvmptv	$⊢ (f \in H ⟼ P (f) \cdot_{L} u (f) (b)) = (h \in H ⟼ P (h) \cdot_{L} u (h) (b))$
314	186	oveq2d	$⊢ b = c \to P (h) \cdot_{L} u (h) (b) = P (h) \cdot_{L} u (h) (c)$
315	314	mpteq2dv	$⊢ b = c \to (h \in H ⟼ P (h) \cdot_{L} u (h) (b)) = (h \in H ⟼ P (h) \cdot_{L} u (h) (c))$
316	313 315	eqtrid	$⊢ b = c \to (f \in H ⟼ P (f) \cdot_{L} u (f) (b)) = (h \in H ⟼ P (h) \cdot_{L} u (h) (c))$
317	316	oveq2d	$⊢ b = c \to \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (b)) = \underset{h \in H}{\sum_{L}} (P (h) \cdot_{L} u (h) (c))$
318	317 187	oveq12d	$⊢ b = c \to (\underset{f \in H}{\sum_{L}}, (P (f) \cdot_{L} u (f) (b))) \cdot_{L} b = (\underset{h \in H}{\sum_{L}}, (P (h) \cdot_{L} u (h) (c))) \cdot_{L} c$
319	318	cbvmptv	$⊢ (b \in B ⟼ (\underset{f \in H}{\sum_{L}}, (P (f) \cdot_{L} u (f) (b))) \cdot_{L} b) = (c \in B ⟼ (\underset{h \in H}{\sum_{L}}, (P (h) \cdot_{L} u (h) (c))) \cdot_{L} c)$
320	319	oveq2i	$⊢ \underset{b \in B}{\sum_{L}} ((\underset{f \in H}{\sum_{L}}, (P (f) \cdot_{L} u (f) (b))) \cdot_{L} b) = \underset{c \in B}{\sum_{L}} ((\underset{h \in H}{\sum_{L}}, (P (h) \cdot_{L} u (h) (c))) \cdot_{L} c)$
321	311 320	eqtr4di	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to X = \underset{b \in B}{\sum_{L}} ((\underset{f \in H}{\sum_{L}}, (P (f) \cdot_{L} u (f) (b))) \cdot_{L} b)$
322	120 321	jca	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to ({finSupp}_{0_{L}} ((c \in B ⟼ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} u (f) (c)))) \land X = \underset{b \in B}{\sum_{L}} ((\underset{f \in H}{\sum_{L}}, (P (f) \cdot_{L} u (f) (b))) \cdot_{L} b))$
323	96 116 322	rspcedvd	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))) \to \exists a \in (G^{B}) ({finSupp}_{0_{L}} (a) \land X = \underset{b \in B}{\sum_{L}} (a (b) \cdot_{L} b))$
324		breq1	$⊢ e = u (f) \to ({finSupp}_{0_{L}} (e) \leftrightarrow {finSupp}_{0_{L}} (u (f)))$
325		fveq1	$⊢ e = u (f) \to e (b) = u (f) (b)$
326	325	oveq1d	$⊢ e = u (f) \to e (b) \cdot_{L} b = u (f) (b) \cdot_{L} b$
327	326	mpteq2dv	$⊢ e = u (f) \to (b \in B ⟼ e (b) \cdot_{L} b) = (b \in B ⟼ u (f) (b) \cdot_{L} b)$
328	327	oveq2d	$⊢ e = u (f) \to \underset{b \in B}{\sum_{L}} (e (b) \cdot_{L} b) = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b)$
329	328	eqeq2d	$⊢ e = u (f) \to (f = \underset{b \in B}{\sum_{L}} (e (b) \cdot_{L} b) \leftrightarrow f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))$
330	324 329	anbi12d	$⊢ e = u (f) \to (({finSupp}_{0_{L}} (e) \land f = \underset{b \in B}{\sum_{L}} (e (b) \cdot_{L} b)) \leftrightarrow ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b)))$
331		ovexd	$⊢ φ \to F^{B} \in V$
332		eqid	$⊢ LSpan (subringAlg (J) (F)) = LSpan (subringAlg (J) (F))$
333	143 144 332	lbssp	$⊢ B \in LBasis (subringAlg (J) (F)) \to LSpan (subringAlg (J) (F)) (B) = {Base}_{subringAlg (J) (F)}$
334	12 333	syl	$⊢ φ \to LSpan (subringAlg (J) (F)) (B) = {Base}_{subringAlg (J) (F)}$
335	148 73 334	3eqtr4rd	$⊢ φ \to LSpan (subringAlg (J) (F)) (B) = H$
336	335	eleq2d	$⊢ φ \to (f \in LSpan (subringAlg (J) (F)) (B) \leftrightarrow f \in H)$
337		eqid	$⊢ {Base}_{Scalar (subringAlg (J) (F))} = {Base}_{Scalar (subringAlg (J) (F))}$
338		eqid	$⊢ Scalar (subringAlg (J) (F)) = Scalar (subringAlg (J) (F))$
339		eqid	$⊢ 0_{Scalar (subringAlg (J) (F))} = 0_{Scalar (subringAlg (J) (F))}$
340		eqid	$⊢ \cdot_{subringAlg (J) (F)} = \cdot_{subringAlg (J) (F)}$
341		sdrgsubrg	$⊢ F \in SubDRing (J) \to F \in SubRing (J)$
342	6 341	syl	$⊢ φ \to F \in SubRing (J)$
343		eqid	$⊢ subringAlg (J) (F) = subringAlg (J) (F)$
344	343	sralmod	$⊢ F \in SubRing (J) \to subringAlg (J) (F) \in LMod$
345	342 344	syl	$⊢ φ \to subringAlg (J) (F) \in LMod$
346	332 143 337 338 339 340 345 146	ellspds	$⊢ φ \to (f \in LSpan (subringAlg (J) (F)) (B) \leftrightarrow \exists e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B}) ({finSupp}_{0_{Scalar (subringAlg (J) (F))}} (e) \land f = \underset{b \in B}{\sum_{subringAlg (J) (F)}} (e (b) \cdot_{subringAlg (J) (F)} b)))$
347	336 346	bitr3d	$⊢ φ \to (f \in H \leftrightarrow \exists e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B}) ({finSupp}_{0_{Scalar (subringAlg (J) (F))}} (e) \land f = \underset{b \in B}{\sum_{subringAlg (J) (F)}} (e (b) \cdot_{subringAlg (J) (F)} b)))$
348	347	biimpa	$⊢ (φ \land f \in H) \to \exists e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B}) ({finSupp}_{0_{Scalar (subringAlg (J) (F))}} (e) \land f = \underset{b \in B}{\sum_{subringAlg (J) (F)}} (e (b) \cdot_{subringAlg (J) (F)} b))$
349		eqid	$⊢ J ↾_{𝑠} F = J ↾_{𝑠} F$
350	349 67	ressbas2	$⊢ F \subseteq {Base}_{J} \to F = {Base}_{(J ↾_{𝑠} F)}$
351	69 350	syl	$⊢ φ \to F = {Base}_{(J ↾_{𝑠} F)}$
352	147 69	srasca	$⊢ φ \to J ↾_{𝑠} F = Scalar (subringAlg (J) (F))$
353	352	fveq2d	$⊢ φ \to {Base}_{(J ↾_{𝑠} F)} = {Base}_{Scalar (subringAlg (J) (F))}$
354	351 353	eqtr2d	$⊢ φ \to {Base}_{Scalar (subringAlg (J) (F))} = F$
355	354	oveq1d	$⊢ φ \to {Base}_{Scalar (subringAlg (J) (F))}^{B} = F^{B}$
356		sdrgsubrg	$⊢ H \in SubDRing (L) \to H \in SubRing (L)$
357	8 356	syl	$⊢ φ \to H \in SubRing (L)$
358		subrgsubg	$⊢ H \in SubRing (L) \to H \in SubGrp (L)$
359	3 19	subg0	$⊢ H \in SubGrp (L) \to 0_{L} = 0_{J}$
360	357 358 359	3syl	$⊢ φ \to 0_{L} = 0_{J}$
361	3	sdrgdrng	$⊢ H \in SubDRing (L) \to J \in DivRing$
362	8 361	syl	$⊢ φ \to J \in DivRing$
363	362	drngringd	$⊢ φ \to J \in Ring$
364	363	ringcmnd	$⊢ φ \to J \in CMnd$
365	364	cmnmndd	$⊢ φ \to J \in Mnd$
366		subrgsubg	$⊢ F \in SubRing (J) \to F \in SubGrp (J)$
367		eqid	$⊢ 0_{J} = 0_{J}$
368	367	subg0cl	$⊢ F \in SubGrp (J) \to 0_{J} \in F$
369	342 366 368	3syl	$⊢ φ \to 0_{J} \in F$
370	349 67 367	ress0g	$⊢ (J \in Mnd \land 0_{J} \in F \land F \subseteq {Base}_{J}) \to 0_{J} = 0_{(J ↾_{𝑠} F)}$
371	365 369 69 370	syl3anc	$⊢ φ \to 0_{J} = 0_{(J ↾_{𝑠} F)}$
372	352	fveq2d	$⊢ φ \to 0_{(J ↾_{𝑠} F)} = 0_{Scalar (subringAlg (J) (F))}$
373	360 371 372	3eqtrrd	$⊢ φ \to 0_{Scalar (subringAlg (J) (F))} = 0_{L}$
374	373	breq2d	$⊢ φ \to ({finSupp}_{0_{Scalar (subringAlg (J) (F))}} (e) \leftrightarrow {finSupp}_{0_{L}} (e))$
375	374	adantr	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to ({finSupp}_{0_{Scalar (subringAlg (J) (F))}} (e) \leftrightarrow {finSupp}_{0_{L}} (e))$
376	12	adantr	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to B \in LBasis (subringAlg (J) (F))$
377		subgsubm	$⊢ H \in SubGrp (L) \to H \in SubMnd (L)$
378	357 358 377	3syl	$⊢ φ \to H \in SubMnd (L)$
379	378	adantr	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to H \in SubMnd (L)$
380	3 31	ressmulr	$⊢ H \in SubDRing (L) \to \cdot_{L} = \cdot_{J}$
381	8 380	syl	$⊢ φ \to \cdot_{L} = \cdot_{J}$
382	147 69	sravsca	$⊢ φ \to \cdot_{J} = \cdot_{subringAlg (J) (F)}$
383	381 382	eqtrd	$⊢ φ \to \cdot_{L} = \cdot_{subringAlg (J) (F)}$
384	383	ad2antrr	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to \cdot_{L} = \cdot_{subringAlg (J) (F)}$
385	384	oveqd	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to e (b) \cdot_{L} b = e (b) \cdot_{subringAlg (J) (F)} b$
386	357	ad2antrr	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to H \in SubRing (L)$
387	74	ad2antrr	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to F \subseteq H$
388	5	adantr	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to F \in SubDRing (I)$
389	355	eleq2d	$⊢ φ \to (e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B}) \leftrightarrow e \in (F^{B}))$
390	389	biimpa	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to e \in (F^{B})$
391	376 388 390	elmaprd	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to e : B ⟶ F$
392	391	ffvelcdmda	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to e (b) \in F$
393	387 392	sseldd	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to e (b) \in H$
394	150	adantr	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to B \subseteq H$
395	394	sselda	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to b \in H$
396	31 386 393 395	subrgmcld	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to e (b) \cdot_{L} b \in H$
397	385 396	eqeltrrd	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to e (b) \cdot_{subringAlg (J) (F)} b \in H$
398	397	fmpttd	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to (b \in B ⟼ e (b) \cdot_{subringAlg (J) (F)} b) : B ⟶ H$
399	376 379 398 3	gsumsubm	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to \underset{b \in B}{\sum_{L}} (e (b) \cdot_{subringAlg (J) (F)} b) = \underset{b \in B}{\sum_{J}} (e (b) \cdot_{subringAlg (J) (F)} b)$
400	381 382	eqtr2d	$⊢ φ \to \cdot_{subringAlg (J) (F)} = \cdot_{L}$
401	400	adantr	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to \cdot_{subringAlg (J) (F)} = \cdot_{L}$
402	401	oveqd	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to e (b) \cdot_{subringAlg (J) (F)} b = e (b) \cdot_{L} b$
403	402	mpteq2dv	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to (b \in B ⟼ e (b) \cdot_{subringAlg (J) (F)} b) = (b \in B ⟼ e (b) \cdot_{L} b)$
404	403	oveq2d	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to \underset{b \in B}{\sum_{L}} (e (b) \cdot_{subringAlg (J) (F)} b) = \underset{b \in B}{\sum_{L}} (e (b) \cdot_{L} b)$
405	12	mptexd	$⊢ φ \to (b \in B ⟼ e (b) \cdot_{subringAlg (J) (F)} b) \in V$
406		fvexd	$⊢ φ \to subringAlg (J) (F) \in V$
407	343 405 362 406 69	gsumsra	$⊢ φ \to \underset{b \in B}{\sum_{J}} (e (b) \cdot_{subringAlg (J) (F)} b) = \underset{b \in B}{\sum_{subringAlg (J) (F)}} (e (b) \cdot_{subringAlg (J) (F)} b)$
408	407	adantr	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to \underset{b \in B}{\sum_{J}} (e (b) \cdot_{subringAlg (J) (F)} b) = \underset{b \in B}{\sum_{subringAlg (J) (F)}} (e (b) \cdot_{subringAlg (J) (F)} b)$
409	399 404 408	3eqtr3rd	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to \underset{b \in B}{\sum_{subringAlg (J) (F)}} (e (b) \cdot_{subringAlg (J) (F)} b) = \underset{b \in B}{\sum_{L}} (e (b) \cdot_{L} b)$
410	409	eqeq2d	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to (f = \underset{b \in B}{\sum_{subringAlg (J) (F)}} (e (b) \cdot_{subringAlg (J) (F)} b) \leftrightarrow f = \underset{b \in B}{\sum_{L}} (e (b) \cdot_{L} b))$
411	375 410	anbi12d	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to (({finSupp}_{0_{Scalar (subringAlg (J) (F))}} (e) \land f = \underset{b \in B}{\sum_{subringAlg (J) (F)}} (e (b) \cdot_{subringAlg (J) (F)} b)) \leftrightarrow ({finSupp}_{0_{L}} (e) \land f = \underset{b \in B}{\sum_{L}} (e (b) \cdot_{L} b)))$
412	355 411	rexeqbidva	$⊢ φ \to (\exists e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B}) ({finSupp}_{0_{Scalar (subringAlg (J) (F))}} (e) \land f = \underset{b \in B}{\sum_{subringAlg (J) (F)}} (e (b) \cdot_{subringAlg (J) (F)} b)) \leftrightarrow \exists e \in (F^{B}) ({finSupp}_{0_{L}} (e) \land f = \underset{b \in B}{\sum_{L}} (e (b) \cdot_{L} b)))$
413	412	adantr	$⊢ (φ \land f \in H) \to (\exists e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B}) ({finSupp}_{0_{Scalar (subringAlg (J) (F))}} (e) \land f = \underset{b \in B}{\sum_{subringAlg (J) (F)}} (e (b) \cdot_{subringAlg (J) (F)} b)) \leftrightarrow \exists e \in (F^{B}) ({finSupp}_{0_{L}} (e) \land f = \underset{b \in B}{\sum_{L}} (e (b) \cdot_{L} b)))$
414	348 413	mpbid	$⊢ (φ \land f \in H) \to \exists e \in (F^{B}) ({finSupp}_{0_{L}} (e) \land f = \underset{b \in B}{\sum_{L}} (e (b) \cdot_{L} b))$
415	330 8 331 414	ac6mapd	$⊢ φ \to \exists u \in ({(F^{B})}^{H}) \forall f \in H ({finSupp}_{0_{L}} (u (f)) \land f = \underset{b \in B}{\sum_{L}} (u (f) (b) \cdot_{L} b))$
416	323 415	r19.29a	$⊢ φ \to \exists a \in (G^{B}) ({finSupp}_{0_{L}} (a) \land X = \underset{b \in B}{\sum_{L}} (a (b) \cdot_{L} b))$

Metamath Proof Explorer

Theorem fldextrspunlsplem

Proof