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		simpllr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to u \in ({(F^{B})}^{H})$
47	46	elmaprd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to u : H ⟶ F^{B}$
48	47 34	ffvelcdmd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to u (f) \in (F^{B})$
49	48	elmaprd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to u (f) : B ⟶ F$
50		simplr	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to c \in B$
51	49 50	ffvelcdmd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to u (f) (c) \in F$
52	45 51	sseldd	$⊢ (((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \land f \in H) \to u (f) (c) \in G$
53	31 32 35 52	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$
54	53	fmpttd	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land c \in B) \to (f \in H ⟼ P (f) \cdot_{L} u (f) (c)) : H ⟶ G$
55	54	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$
56		fveq2	$⊢ f = h \to P (f) = P (h)$
57		fveq2	$⊢ f = h \to u (f) = u (h)$
58	57	fveq1d	$⊢ f = h \to u (f) (c) = u (h) (c)$
59	56 58	oveq12d	$⊢ f = h \to P (f) \cdot_{L} u (f) (c) = P (h) \cdot_{L} u (h) (c)$
60	59	cbvmptv	$⊢ (f \in H ⟼ P (f) \cdot_{L} u (f) (c)) = (h \in H ⟼ P (h) \cdot_{L} u (h) (c))$
61		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$
62		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$
63		eqid	$⊢ {Base}_{J} = {Base}_{J}$
64	63	sdrgss	$⊢ F \in SubDRing (J) \to F \subseteq {Base}_{J}$
65	6 64	syl	$⊢ φ \to F \subseteq {Base}_{J}$
66	39	sdrgss	$⊢ H \in SubDRing (L) \to H \subseteq {Base}_{L}$
67	8 66	syl	$⊢ φ \to H \subseteq {Base}_{L}$
68	3 39	ressbas2	$⊢ H \subseteq {Base}_{L} \to H = {Base}_{J}$
69	67 68	syl	$⊢ φ \to H = {Base}_{J}$
70	65 69	sseqtrrd	$⊢ φ \to F \subseteq H$
71	70 67	sstrd	$⊢ φ \to F \subseteq {Base}_{L}$
72	71	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}$
73		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})$
74	73	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}$
75	74	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})$
76	75	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$
77		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$
78	76 77	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$
79	72 78	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}$
80	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$
81	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)$
82	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$
83		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}$
84	39 31 19 82 83	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}$
85	61 61 24 62 79 80 81 84	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)))$
86	60 85	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)))$
87	19 23 24 30 55 86	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$
88	87	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$
89	17 18 88	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})$
90		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)))))$
91	90	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)))))$
92		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)))$
93	92	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)$
94		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)))$
95		fveq2	$⊢ c = b \to u (f) (c) = u (f) (b)$
96	95	oveq2d	$⊢ c = b \to P (f) \cdot_{L} u (f) (c) = P (f) \cdot_{L} u (f) (b)$
97	96	mpteq2dv	$⊢ c = b \to (f \in H ⟼ P (f) \cdot_{L} u (f) (c)) = (f \in H ⟼ P (f) \cdot_{L} u (f) (b))$
98	97	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))$
99		simpr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land b \in B) \to b \in B$
100		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$
101	94 98 99 100	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))$
102	101	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))$
103	93 102	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))$
104	103	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$
105	104	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)$
106	105	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)$
107	106	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))$
108	91 107	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)))$
109	108	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)))$
110	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$
111		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$
112		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$
113	94 110 111 112	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))))$
114	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)$
115	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$
116	115	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$
117	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))$
118	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}$
119	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$
120	119	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$
121	118 120	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}$
122	116	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$
123	71	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}$
124		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})$
125	124	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}$
126		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$
127	125 126	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})$
128	127	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$
129		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$
130	128 129	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$
131	123 130	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}$
132		eqid	$⊢ {Base}_{subringAlg (J) (F)} = {Base}_{subringAlg (J) (F)}$
133		eqid	$⊢ LBasis (subringAlg (J) (F)) = LBasis (subringAlg (J) (F))$
134	132 133	lbsss	$⊢ B \in LBasis (subringAlg (J) (F)) \to B \subseteq {Base}_{subringAlg (J) (F)}$
135	12 134	syl	$⊢ φ \to B \subseteq {Base}_{subringAlg (J) (F)}$
136		eqidd	$⊢ φ \to subringAlg (J) (F) = subringAlg (J) (F)$
137	136 65	srabase	$⊢ φ \to {Base}_{J} = {Base}_{subringAlg (J) (F)}$
138	69 137	eqtr2d	$⊢ φ \to {Base}_{subringAlg (J) (F)} = H$
139	135 138	sseqtrd	$⊢ φ \to B \subseteq H$
140	139 67	sstrd	$⊢ φ \to B \subseteq {Base}_{L}$
141	140	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}$
142	141	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}$
143	39 31 122 131 142	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}$
144		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$
145		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$
146		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})$
147	146	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}$
148	147	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})$
149	148	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$
150	57	breq1d	$⊢ f = h \to ({finSupp}_{0_{L}} (u (f)) \leftrightarrow {finSupp}_{0_{L}} (u (h)))$
151		id	$⊢ f = h \to f = h$
152	57	fveq1d	$⊢ f = h \to u (f) (b) = u (h) (b)$
153	152	oveq1d	$⊢ f = h \to u (f) (b) \cdot_{L} b = u (h) (b) \cdot_{L} b$
154	153	mpteq2dv	$⊢ f = h \to (b \in B ⟼ u (f) (b) \cdot_{L} b) = (b \in B ⟼ u (h) (b) \cdot_{L} b)$
155	154	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)$
156	151 155	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))$
157	150 156	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)))$
158		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))$
159		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$
160	157 158 159	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))$
161	160	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))$
162	116	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$
163		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}$
164	39 31 19 162 163	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}$
165	144 144 117 145 142 149 161 164	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))$
166	39 19 31 116 117 121 143 165	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))$
167	121	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}$
168	39 31 122 167 131 142	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)$
169	168	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))$
170	169	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))$
171	160	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)$
172		fveq2	$⊢ b = c \to u (h) (b) = u (h) (c)$
173		id	$⊢ b = c \to b = c$
174	172 173	oveq12d	$⊢ b = c \to u (h) (b) \cdot_{L} b = u (h) (c) \cdot_{L} c$
175	174	cbvmptv	$⊢ (b \in B ⟼ u (h) (b) \cdot_{L} b) = (c \in B ⟼ u (h) (c) \cdot_{L} c)$
176	175	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)$
177	171 176	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)$
178	177	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))$
179	166 170 178	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)$
180	179	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))$
181	180	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))$
182	56 151	oveq12d	$⊢ f = h \to P (f) \cdot_{L} f = P (h) \cdot_{L} h$
183	182	cbvmptv	$⊢ (f \in H ⟼ P (f) \cdot_{L} f) = (h \in H ⟼ P (h) \cdot_{L} h)$
184	183	oveq2i	$⊢ \underset{f \in H}{\sum_{L}} (P (f) \cdot_{L} f) = \underset{h \in H}{\sum_{L}} (P (h) \cdot_{L} h)$
185	184	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)$
186	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$
187	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)$
188	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$
189	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}$
190	80	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$
191	189 190	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}$
192	39 31 188 191 79	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}$
193	140	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}$
194	193	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}$
195	194	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}$
196	39 31 188 192 195	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}$
197	196	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}$
198	15	fsuppimpd	$⊢ φ \to P supp 0_{L} \in Fin$
199	198	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$
200		suppssdm	$⊢ P supp 0_{L} \subseteq dom P$
201	200 14	fssdm	$⊢ φ \to P supp 0_{L} \subseteq H$
202	201	sseld	$⊢ φ \to (f \in {supp}_{0_{L}} (P) \to f \in H)$
203	202	adantr	$⊢ (φ \land u \in ({(F^{B})}^{H})) \to (f \in {supp}_{0_{L}} (P) \to f \in H)$
204		simpr	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land {finSupp}_{0_{L}} (u (f))) \to {finSupp}_{0_{L}} (u (f))$
205	204	fsuppimpd	$⊢ ((φ \land u \in ({(F^{B})}^{H})) \land {finSupp}_{0_{L}} (u (f))) \to u (f) supp 0_{L} \in Fin$
206	205	ex	$⊢ (φ \land u \in ({(F^{B})}^{H})) \to ({finSupp}_{0_{L}} (u (f)) \to u (f) supp 0_{L} \in Fin)$
207	206	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)$
208	203 207	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))$
209	208	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)$
210	209	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$
211		fveq2	$⊢ f = i \to u (f) = u (i)$
212	211	oveq1d	$⊢ f = i \to u (f) supp 0_{L} = u (i) supp 0_{L}$
213	212	eleq1d	$⊢ f = i \to (u (f) supp 0_{L} \in Fin \leftrightarrow u (i) supp 0_{L} \in Fin)$
214	213	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$
215	210 214	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$
216		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$
217	199 215 216	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$
218		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$
219	217 199 218	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$
220		snssi	$⊢ i \in {supp}_{0_{L}} (P) \to \{i\} \subseteq P supp 0_{L}$
221	220	adantl	$⊢ (φ \land i \in {supp}_{0_{L}} (P)) \to \{i\} \subseteq P supp 0_{L}$
222	221	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)$
223	222	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)$
224	219 223	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$
225	14	ffnd	$⊢ φ \to P Fn H$
226	225	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$
227	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)$
228		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$
229		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$
230		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)$
231	229 230	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))$
232	226 227 228 231	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}$
233	232	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)$
234	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$
235	71	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}$
236		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})$
237	236	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}$
238	237 229	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})$
239	238	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$
240		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$
241	239 240	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$
242	235 241	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}$
243	39 31 19 234 242	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}$
244	233 243	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}$
245		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})$
246	245	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}$
247		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$
248	246 247	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})$
249	248	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$
250	249	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$
251	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))$
252		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$
253		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$
254		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))$
255	253 254	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)))$
256	250 251 252 255	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}$
257	256	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}$
258	188	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$
259	191	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}$
260	39 31 19 258 259	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}$
261	257 260	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}$
262		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\})$
263		fveq2	$⊢ h = i \to u (h) = u (i)$
264	263	oveq1d	$⊢ h = i \to u (h) supp 0_{L} = u (i) supp 0_{L}$
265		sneq	$⊢ h = i \to \{h\} = \{i\}$
266	264 265	xpeq12d	$⊢ h = i \to {supp}_{0_{L}} (u (h)) \times \{h\} = {supp}_{0_{L}} (u (i)) \times \{i\}$
267	266	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\})$
268	267	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\})$
269		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)))$
270	262 268 269	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)))$
271	270	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)))$
272		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)))$
273	271 272	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)))$
274	273	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)))$
275	244 261 274	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}$
276	275	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$
277	115	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$
278	194	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}$
279	39 31 19 277 278	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}$
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) \to (P (h) \cdot_{L} u (h) (c)) \cdot_{L} c = 0_{L}$
281	280	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}$
282	281	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}$
283	282	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}$
284	283	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}$
285	284	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}$
286	39 19 186 18 187 197 224 285	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))$
287	181 185 286	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))$
288	115	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$
289	39 19 31 288 24 194 192 85	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$
290	289	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)$
291	290	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)$
292	114 287 291	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)$
293	56 152	oveq12d	$⊢ f = h \to P (f) \cdot_{L} u (f) (b) = P (h) \cdot_{L} u (h) (b)$
294	293	cbvmptv	$⊢ (f \in H ⟼ P (f) \cdot_{L} u (f) (b)) = (h \in H ⟼ P (h) \cdot_{L} u (h) (b))$
295	172	oveq2d	$⊢ b = c \to P (h) \cdot_{L} u (h) (b) = P (h) \cdot_{L} u (h) (c)$
296	295	mpteq2dv	$⊢ b = c \to (h \in H ⟼ P (h) \cdot_{L} u (h) (b)) = (h \in H ⟼ P (h) \cdot_{L} u (h) (c))$
297	294 296	eqtrid	$⊢ b = c \to (f \in H ⟼ P (f) \cdot_{L} u (f) (b)) = (h \in H ⟼ P (h) \cdot_{L} u (h) (c))$
298	297	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))$
299	298 173	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$
300	299	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)$
301	300	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)$
302	292 301	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)$
303	113 302	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))$
304	89 109 303	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))$
305		breq1	$⊢ e = u (f) \to ({finSupp}_{0_{L}} (e) \leftrightarrow {finSupp}_{0_{L}} (u (f)))$
306		fveq1	$⊢ e = u (f) \to e (b) = u (f) (b)$
307	306	oveq1d	$⊢ e = u (f) \to e (b) \cdot_{L} b = u (f) (b) \cdot_{L} b$
308	307	mpteq2dv	$⊢ e = u (f) \to (b \in B ⟼ e (b) \cdot_{L} b) = (b \in B ⟼ u (f) (b) \cdot_{L} b)$
309	308	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)$
310	309	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))$
311	305 310	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)))$
312		ovexd	$⊢ φ \to F^{B} \in V$
313		eqid	$⊢ LSpan (subringAlg (J) (F)) = LSpan (subringAlg (J) (F))$
314	132 133 313	lbssp	$⊢ B \in LBasis (subringAlg (J) (F)) \to LSpan (subringAlg (J) (F)) (B) = {Base}_{subringAlg (J) (F)}$
315	12 314	syl	$⊢ φ \to LSpan (subringAlg (J) (F)) (B) = {Base}_{subringAlg (J) (F)}$
316	137 69 315	3eqtr4rd	$⊢ φ \to LSpan (subringAlg (J) (F)) (B) = H$
317	316	eleq2d	$⊢ φ \to (f \in LSpan (subringAlg (J) (F)) (B) \leftrightarrow f \in H)$
318		eqid	$⊢ {Base}_{Scalar (subringAlg (J) (F))} = {Base}_{Scalar (subringAlg (J) (F))}$
319		eqid	$⊢ Scalar (subringAlg (J) (F)) = Scalar (subringAlg (J) (F))$
320		eqid	$⊢ 0_{Scalar (subringAlg (J) (F))} = 0_{Scalar (subringAlg (J) (F))}$
321		eqid	$⊢ \cdot_{subringAlg (J) (F)} = \cdot_{subringAlg (J) (F)}$
322		sdrgsubrg	$⊢ F \in SubDRing (J) \to F \in SubRing (J)$
323	6 322	syl	$⊢ φ \to F \in SubRing (J)$
324		eqid	$⊢ subringAlg (J) (F) = subringAlg (J) (F)$
325	324	sralmod	$⊢ F \in SubRing (J) \to subringAlg (J) (F) \in LMod$
326	323 325	syl	$⊢ φ \to subringAlg (J) (F) \in LMod$
327	313 132 318 319 320 321 326 135	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)))$
328	317 327	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)))$
329	328	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))$
330		eqid	$⊢ J ↾_{𝑠} F = J ↾_{𝑠} F$
331	330 63	ressbas2	$⊢ F \subseteq {Base}_{J} \to F = {Base}_{(J ↾_{𝑠} F)}$
332	65 331	syl	$⊢ φ \to F = {Base}_{(J ↾_{𝑠} F)}$
333	136 65	srasca	$⊢ φ \to J ↾_{𝑠} F = Scalar (subringAlg (J) (F))$
334	333	fveq2d	$⊢ φ \to {Base}_{(J ↾_{𝑠} F)} = {Base}_{Scalar (subringAlg (J) (F))}$
335	332 334	eqtr2d	$⊢ φ \to {Base}_{Scalar (subringAlg (J) (F))} = F$
336	335	oveq1d	$⊢ φ \to {Base}_{Scalar (subringAlg (J) (F))}^{B} = F^{B}$
337		sdrgsubrg	$⊢ H \in SubDRing (L) \to H \in SubRing (L)$
338	8 337	syl	$⊢ φ \to H \in SubRing (L)$
339		subrgsubg	$⊢ H \in SubRing (L) \to H \in SubGrp (L)$
340	3 19	subg0	$⊢ H \in SubGrp (L) \to 0_{L} = 0_{J}$
341	338 339 340	3syl	$⊢ φ \to 0_{L} = 0_{J}$
342	3	sdrgdrng	$⊢ H \in SubDRing (L) \to J \in DivRing$
343	8 342	syl	$⊢ φ \to J \in DivRing$
344	343	drngringd	$⊢ φ \to J \in Ring$
345	344	ringcmnd	$⊢ φ \to J \in CMnd$
346	345	cmnmndd	$⊢ φ \to J \in Mnd$
347		subrgsubg	$⊢ F \in SubRing (J) \to F \in SubGrp (J)$
348		eqid	$⊢ 0_{J} = 0_{J}$
349	348	subg0cl	$⊢ F \in SubGrp (J) \to 0_{J} \in F$
350	323 347 349	3syl	$⊢ φ \to 0_{J} \in F$
351	330 63 348	ress0g	$⊢ (J \in Mnd \land 0_{J} \in F \land F \subseteq {Base}_{J}) \to 0_{J} = 0_{(J ↾_{𝑠} F)}$
352	346 350 65 351	syl3anc	$⊢ φ \to 0_{J} = 0_{(J ↾_{𝑠} F)}$
353	333	fveq2d	$⊢ φ \to 0_{(J ↾_{𝑠} F)} = 0_{Scalar (subringAlg (J) (F))}$
354	341 352 353	3eqtrrd	$⊢ φ \to 0_{Scalar (subringAlg (J) (F))} = 0_{L}$
355	354	breq2d	$⊢ φ \to ({finSupp}_{0_{Scalar (subringAlg (J) (F))}} (e) \leftrightarrow {finSupp}_{0_{L}} (e))$
356	355	adantr	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to ({finSupp}_{0_{Scalar (subringAlg (J) (F))}} (e) \leftrightarrow {finSupp}_{0_{L}} (e))$
357	12	adantr	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to B \in LBasis (subringAlg (J) (F))$
358		subgsubm	$⊢ H \in SubGrp (L) \to H \in SubMnd (L)$
359	338 339 358	3syl	$⊢ φ \to H \in SubMnd (L)$
360	359	adantr	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to H \in SubMnd (L)$
361	3 31	ressmulr	$⊢ H \in SubDRing (L) \to \cdot_{L} = \cdot_{J}$
362	8 361	syl	$⊢ φ \to \cdot_{L} = \cdot_{J}$
363	136 65	sravsca	$⊢ φ \to \cdot_{J} = \cdot_{subringAlg (J) (F)}$
364	362 363	eqtrd	$⊢ φ \to \cdot_{L} = \cdot_{subringAlg (J) (F)}$
365	364	ad2antrr	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to \cdot_{L} = \cdot_{subringAlg (J) (F)}$
366	365	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$
367	338	ad2antrr	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to H \in SubRing (L)$
368	70	ad2antrr	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to F \subseteq H$
369	336	eleq2d	$⊢ φ \to (e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B}) \leftrightarrow e \in (F^{B}))$
370	369	biimpa	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to e \in (F^{B})$
371	370	elmaprd	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to e : B ⟶ F$
372	371	ffvelcdmda	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to e (b) \in F$
373	368 372	sseldd	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to e (b) \in H$
374	139	adantr	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to B \subseteq H$
375	374	sselda	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to b \in H$
376	31 367 373 375	subrgmcld	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to e (b) \cdot_{L} b \in H$
377	366 376	eqeltrrd	$⊢ ((φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \land b \in B) \to e (b) \cdot_{subringAlg (J) (F)} b \in H$
378	377	fmpttd	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to (b \in B ⟼ e (b) \cdot_{subringAlg (J) (F)} b) : B ⟶ H$
379	357 360 378 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)$
380	362 363	eqtr2d	$⊢ φ \to \cdot_{subringAlg (J) (F)} = \cdot_{L}$
381	380	adantr	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to \cdot_{subringAlg (J) (F)} = \cdot_{L}$
382	381	oveqd	$⊢ (φ \land e \in ({Base}_{Scalar (subringAlg (J) (F))}^{B})) \to e (b) \cdot_{subringAlg (J) (F)} b = e (b) \cdot_{L} b$
383	382	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)$
384	383	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)$
385	12	mptexd	$⊢ φ \to (b \in B ⟼ e (b) \cdot_{subringAlg (J) (F)} b) \in V$
386		fvexd	$⊢ φ \to subringAlg (J) (F) \in V$
387	324 385 343 386 65	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)$
388	387	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)$
389	379 384 388	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)$
390	389	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))$
391	356 390	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)))$
392	336 391	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)))$
393	392	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)))$
394	329 393	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))$
395	311 8 312 394	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))$
396	304 395	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