Theorem fldextrspunlsp 33858

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

Hypotheses

Ref	Expression
fldextrspunfld.k	⊢ 𝐾 = (𝐿 ↾s 𝐹)
fldextrspunfld.i	⊢ 𝐼 = (𝐿 ↾s 𝐺)
fldextrspunfld.j	⊢ 𝐽 = (𝐿 ↾s 𝐻)
fldextrspunfld.2	⊢ (𝜑 → 𝐿 ∈ Field)
fldextrspunfld.3	⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
fldextrspunfld.4	⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
fldextrspunfld.5	⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
fldextrspunfld.6	⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
fldextrspunlsp.n	⊢ 𝑁 = (RingSpan‘𝐿)
fldextrspunlsp.c	⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))
fldextrspunlsp.e	⊢ 𝐸 = (𝐿 ↾s 𝐶)
fldextrspunlsp.1	⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
fldextrspunlsp.2	⊢ (𝜑 → 𝐵 ∈ Fin)

Assertion

Ref	Expression
fldextrspunlsp	⊢ (𝜑 → 𝐶 = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝐵))

Proof of Theorem fldextrspunlsp

Dummy variables 𝑎 𝑓 𝑔 ℎ 𝑝 𝑣 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fldextrspunlsp.c	. . . . 5 ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))
2	1	a1i 11	. . . 4 ⊢ (𝜑 → 𝐶 = (𝑁‘(𝐺 ∪ 𝐻)))
3	2	eleq2d 2825	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ (𝑁‘(𝐺 ∪ 𝐻))))
4		eqid 2739	. . . 4 ⊢ (Base‘𝐿) = (Base‘𝐿)
5		eqid 2739	. . . 4 ⊢ (.r‘𝐿) = (.r‘𝐿)
6		eqid 2739	. . . 4 ⊢ (0g‘𝐿) = (0g‘𝐿)
7		fldextrspunlsp.n	. . . 4 ⊢ 𝑁 = (RingSpan‘𝐿)
8		fldextrspunfld.2	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ Field)
9	8	fldcrngd 20714	. . . 4 ⊢ (𝜑 → 𝐿 ∈ CRing)
10		fldextrspunfld.5	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
11		sdrgsubrg 20763	. . . . 5 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
12	10, 11	syl 17	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
13		fldextrspunfld.6	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
14		sdrgsubrg 20763	. . . . 5 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ∈ (SubRing‘𝐿))
15	13, 14	syl 17	. . . 4 ⊢ (𝜑 → 𝐻 ∈ (SubRing‘𝐿))
16	4, 5, 6, 7, 9, 12, 15	elrgspnsubrun 33330	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝑁‘(𝐺 ∪ 𝐻)) ↔ ∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))))
17	4	subrgss 20544	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
18	12, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
19		eqid 2739	. . . . . . . . 9 ⊢ (𝐿 ↾s 𝐺) = (𝐿 ↾s 𝐺)
20	19, 4	ressbas2 17199	. . . . . . . 8 ⊢ (𝐺 ⊆ (Base‘𝐿) → 𝐺 = (Base‘(𝐿 ↾s 𝐺)))
21	18, 20	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 = (Base‘(𝐿 ↾s 𝐺)))
22		eqidd 2740	. . . . . . . . 9 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺))
23	22, 18	srasca 21170	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ↾s 𝐺) = (Scalar‘((subringAlg ‘𝐿)‘𝐺)))
24	23	fveq2d 6831	. . . . . . 7 ⊢ (𝜑 → (Base‘(𝐿 ↾s 𝐺)) = (Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))))
25	21, 24	eqtr2d 2775	. . . . . 6 ⊢ (𝜑 → (Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) = 𝐺)
26	25	oveq1d 7371	. . . . 5 ⊢ (𝜑 → ((Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ↑m 𝐵) = (𝐺 ↑m 𝐵))
27	9	crngringd 20218	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ Ring)
28	27	ringcmnd 20256	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ CMnd)
29	28	cmnmndd 19770	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ Mnd)
30		subrgsubg 20549	. . . . . . . . . . 11 ⊢ (𝐺 ∈ (SubRing‘𝐿) → 𝐺 ∈ (SubGrp‘𝐿))
31	12, 30	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (SubGrp‘𝐿))
32	6	subg0cl 19101	. . . . . . . . . 10 ⊢ (𝐺 ∈ (SubGrp‘𝐿) → (0g‘𝐿) ∈ 𝐺)
33	31, 32	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (0g‘𝐿) ∈ 𝐺)
34	19, 4, 6	ress0g 18721	. . . . . . . . 9 ⊢ ((𝐿 ∈ Mnd ∧ (0g‘𝐿) ∈ 𝐺 ∧ 𝐺 ⊆ (Base‘𝐿)) → (0g‘𝐿) = (0g‘(𝐿 ↾s 𝐺)))
35	29, 33, 18, 34	syl3anc 1379	. . . . . . . 8 ⊢ (𝜑 → (0g‘𝐿) = (0g‘(𝐿 ↾s 𝐺)))
36	23	fveq2d 6831	. . . . . . . 8 ⊢ (𝜑 → (0g‘(𝐿 ↾s 𝐺)) = (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))))
37	35, 36	eqtr2d 2775	. . . . . . 7 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) = (0g‘𝐿))
38	37	breq2d 5084	. . . . . 6 ⊢ (𝜑 → (𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ↔ 𝑎 finSupp (0g‘𝐿)))
39		eqid 2739	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺)
40		fldextrspunlsp.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
41	40	mptexd 7168	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)) ∈ V)
42	39	sralmod 21177	. . . . . . . . . 10 ⊢ (𝐺 ∈ (SubRing‘𝐿) → ((subringAlg ‘𝐿)‘𝐺) ∈ LMod)
43	12, 42	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐺) ∈ LMod)
44	39, 41, 8, 43, 18	gsumsra 33128	. . . . . . . 8 ⊢ (𝜑 → (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))) = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))
45	22, 18	sravsca 21171	. . . . . . . . . . 11 ⊢ (𝜑 → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺)))
46	45	oveqd 7373	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑎‘𝑣)(.r‘𝐿)𝑣) = ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣))
47	46	mpteq2dv 5166	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)) = (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣)))
48	47	oveq2d 7372	. . . . . . . 8 ⊢ (𝜑 → (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))) = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣))))
49	44, 48	eqtr2d 2775	. . . . . . 7 ⊢ (𝜑 → (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣))) = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))
50	49	eqeq2d 2750	. . . . . 6 ⊢ (𝜑 → (𝑥 = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣))) ↔ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))))
51	38, 50	anbi12d 638	. . . . 5 ⊢ (𝜑 → ((𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ∧ 𝑥 = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣)))) ↔ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))))
52	26, 51	rexeqbidv 3314	. . . 4 ⊢ (𝜑 → (∃𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ↑m 𝐵)(𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ∧ 𝑥 = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣)))) ↔ ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))))
53		eqid 2739	. . . . 5 ⊢ (LSpan‘((subringAlg ‘𝐿)‘𝐺)) = (LSpan‘((subringAlg ‘𝐿)‘𝐺))
54		eqid 2739	. . . . 5 ⊢ (Base‘((subringAlg ‘𝐿)‘𝐺)) = (Base‘((subringAlg ‘𝐿)‘𝐺))
55		eqid 2739	. . . . 5 ⊢ (Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) = (Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺)))
56		eqid 2739	. . . . 5 ⊢ (Scalar‘((subringAlg ‘𝐿)‘𝐺)) = (Scalar‘((subringAlg ‘𝐿)‘𝐺))
57		eqid 2739	. . . . 5 ⊢ (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) = (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺)))
58		eqid 2739	. . . . 5 ⊢ ( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺)) = ( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))
59		eqid 2739	. . . . . . . . . 10 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
60		eqid 2739	. . . . . . . . . 10 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
61	59, 60	lbsss 21067	. . . . . . . . 9 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
62	40, 61	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
63	4	subrgss 20544	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
64	15, 63	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
65		fldextrspunfld.j	. . . . . . . . . . 11 ⊢ 𝐽 = (𝐿 ↾s 𝐻)
66	65, 4	ressbas2 17199	. . . . . . . . . 10 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
67	64, 66	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
68		eqidd 2740	. . . . . . . . . 10 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
69		fldextrspunfld.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
70		eqid 2739	. . . . . . . . . . . 12 ⊢ (Base‘𝐽) = (Base‘𝐽)
71	70	sdrgss 20765	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
72	69, 71	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
73	68, 72	srabase 21167	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
74	67, 73	eqtrd 2774	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
75	62, 74	sseqtrrd 3952	. . . . . . 7 ⊢ (𝜑 → 𝐵 ⊆ 𝐻)
76	75, 64	sstrd 3925	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝐿))
77	22, 18	srabase 21167	. . . . . 6 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
78	76, 77	sseqtrd 3951	. . . . 5 ⊢ (𝜑 → 𝐵 ⊆ (Base‘((subringAlg ‘𝐿)‘𝐺)))
79	53, 54, 55, 56, 57, 58, 43, 78	ellspds 33451	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝐵) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ↑m 𝐵)(𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ∧ 𝑥 = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣))))))
80		fldextrspunfld.k	. . . . . . 7 ⊢ 𝐾 = (𝐿 ↾s 𝐹)
81		fldextrspunfld.i	. . . . . . 7 ⊢ 𝐼 = (𝐿 ↾s 𝐺)
82	8	ad2antrr 732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐿 ∈ Field)
83		fldextrspunfld.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
84	83	ad2antrr 732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐹 ∈ (SubDRing‘𝐼))
85	69	ad2antrr 732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐹 ∈ (SubDRing‘𝐽))
86	10	ad2antrr 732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐺 ∈ (SubDRing‘𝐿))
87	13	ad2antrr 732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐻 ∈ (SubDRing‘𝐿))
88		fldextrspunlsp.e	. . . . . . 7 ⊢ 𝐸 = (𝐿 ↾s 𝐶)
89	40	ad2antrr 732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
90		fldextrspunlsp.2	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ Fin)
91	90	ad2antrr 732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐵 ∈ Fin)
92		simplr 774	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝑝 ∈ (𝐺 ↑m 𝐻))
93	87, 86, 92	elmaprd 32772	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝑝:𝐻⟶𝐺)
94		simprl 776	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝑝 finSupp (0g‘𝐿))
95		simprr 778	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))
96		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (𝑝‘𝑓) = (𝑝‘ℎ))
97		id 22	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → 𝑓 = ℎ)
98	96, 97	oveq12d 7374	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑝‘𝑓)(.r‘𝐿)𝑓) = ((𝑝‘ℎ)(.r‘𝐿)ℎ))
99	98	cbvmptv 5176	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)) = (ℎ ∈ 𝐻 ↦ ((𝑝‘ℎ)(.r‘𝐿)ℎ))
100	99	oveq2i 7367	. . . . . . . 8 ⊢ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑝‘ℎ)(.r‘𝐿)ℎ)))
101	95, 100	eqtrdi 2790	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝑥 = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑝‘ℎ)(.r‘𝐿)ℎ))))
102	80, 81, 65, 82, 84, 85, 86, 87, 7, 1, 88, 89, 91, 93, 94, 101	fldextrspunlsplem 33857	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))))
103	102	r19.29an 3143	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))))
104		breq1 5075	. . . . . . . 8 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝑝 finSupp (0g‘𝐿) ↔ (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) finSupp (0g‘𝐿)))
105		fveq1 6826	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝑝‘𝑓) = ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓))
106	105	oveq1d 7371	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → ((𝑝‘𝑓)(.r‘𝐿)𝑓) = (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))
107	106	mpteq2dv 5166	. . . . . . . . . 10 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)) = (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)))
108	107	oveq2d 7372	. . . . . . . . 9 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))))
109	108	eqeq2d 2750	. . . . . . . 8 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))) ↔ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)))))
110	104, 109	anbi12d 638	. . . . . . 7 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → ((𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)))) ↔ ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))))))
111	10	ad2antrr 732	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → 𝐺 ∈ (SubDRing‘𝐿))
112	13	ad2antrr 732	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → 𝐻 ∈ (SubDRing‘𝐿))
113	40	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
114	10	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → 𝐺 ∈ (SubDRing‘𝐿))
115		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → 𝑎 ∈ (𝐺 ↑m 𝐵))
116	113, 114, 115	elmaprd 32772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → 𝑎:𝐵⟶𝐺)
117	116	ad2antrr 732	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ 𝐻) → 𝑎:𝐵⟶𝐺)
118	117	ffvelcdmda 7025	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ 𝐻) ∧ 𝑔 ∈ 𝐵) → (𝑎‘𝑔) ∈ 𝐺)
119	33	ad4antr 738	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ 𝐻) ∧ ¬ 𝑔 ∈ 𝐵) → (0g‘𝐿) ∈ 𝐺)
120	118, 119	ifclda 4490	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ 𝐻) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) ∈ 𝐺)
121	120	fmpttd 7056	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))):𝐻⟶𝐺)
122	111, 112, 121	elmapdd 8778	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) ∈ (𝐺 ↑m 𝐻))
123		fvexd 6842	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → (0g‘𝐿) ∈ V)
124	121	ffund 6659	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → Fun (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))))
125		simprl 776	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → 𝑎 finSupp (0g‘𝐿))
126	116	ffnd 6656	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → 𝑎 Fn 𝐵)
127	126	ad3antrrr 736	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → 𝑎 Fn 𝐵)
128	40	ad4antr 738	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
129		fvexd 6842	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → (0g‘𝐿) ∈ V)
130		simpr 485	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ 𝐵)
131		simplr 774	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿))))
132	131	eldifbd 3896	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → ¬ 𝑔 ∈ (𝑎 supp (0g‘𝐿)))
133	130, 132	eldifd 3894	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿))))
134	127, 128, 129, 133	fvdifsupp 8111	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → (𝑎‘𝑔) = (0g‘𝐿))
135		eqidd 2740	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ ¬ 𝑔 ∈ 𝐵) → (0g‘𝐿) = (0g‘𝐿))
136	134, 135	ifeqda 4491	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) = (0g‘𝐿))
137	136, 112	suppss2 8140	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) supp (0g‘𝐿)) ⊆ (𝑎 supp (0g‘𝐿)))
138	122, 123, 124, 125, 137	fsuppsssuppgd 9285	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) finSupp (0g‘𝐿))
139		eqid 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))
140		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → 𝑔 = 𝑓)
141		suppssdm 8117	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 supp (0g‘𝐿)) ⊆ dom 𝑎
142	116	fdmd 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → dom 𝑎 = 𝐵)
143	142	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → dom 𝑎 = 𝐵)
144	141, 143	sseqtrid 3957	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑎 supp (0g‘𝐿)) ⊆ 𝐵)
145	144	sselda 3915	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → 𝑓 ∈ 𝐵)
146	145	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → 𝑓 ∈ 𝐵)
147	140, 146	eqeltrd 2839	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → 𝑔 ∈ 𝐵)
148	147	iftrued 4462	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) = (𝑎‘𝑔))
149		fveq2 6827	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → (𝑎‘𝑔) = (𝑎‘𝑓))
150	149	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → (𝑎‘𝑔) = (𝑎‘𝑓))
151	148, 150	eqtrd 2774	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) = (𝑎‘𝑓))
152	75	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐵 ⊆ 𝐻)
153	144, 152	sstrd 3925	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑎 supp (0g‘𝐿)) ⊆ 𝐻)
154	153	sselda 3915	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → 𝑓 ∈ 𝐻)
155		fvexd 6842	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → (𝑎‘𝑓) ∈ V)
156	139, 151, 154, 155	fvmptd2 6944	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓) = (𝑎‘𝑓))
157	156	oveq1d 7371	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓) = ((𝑎‘𝑓)(.r‘𝐿)𝑓))
158	157	mpteq2dva 5165	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)) = (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑓)(.r‘𝐿)𝑓)))
159		fveq2 6827	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑣 → (𝑎‘𝑓) = (𝑎‘𝑣))
160		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑣 → 𝑓 = 𝑣)
161	159, 160	oveq12d 7374	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑣 → ((𝑎‘𝑓)(.r‘𝐿)𝑓) = ((𝑎‘𝑣)(.r‘𝐿)𝑣))
162	161	cbvmptv 5176	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑓)(.r‘𝐿)𝑓)) = (𝑣 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))
163	158, 162	eqtrdi 2790	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)) = (𝑣 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))
164	163	oveq2d 7372	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐿 Σg (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑣 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))
165	28	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐿 ∈ CMnd)
166	13	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐻 ∈ (SubDRing‘𝐿))
167		eleq1w 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑓 → (𝑔 ∈ 𝐵 ↔ 𝑓 ∈ 𝐵))
168	167, 149	ifbieq1d 4479	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑓 → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) = if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿)))
169		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿))))
170	169	eldifad 3895	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑓 ∈ 𝐻)
171		fvexd 6842	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (𝑎‘𝑓) ∈ V)
172		fvexd 6842	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (0g‘𝐿) ∈ V)
173	171, 172	ifcld 4501	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿)) ∈ V)
174	139, 168, 170, 173	fvmptd3 6959	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓) = if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿)))
175	174	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓) = (if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿))(.r‘𝐿)𝑓))
176	126	ad3antrrr 736	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → 𝑎 Fn 𝐵)
177	40	ad4antr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
178		fvexd 6842	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → (0g‘𝐿) ∈ V)
179		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → 𝑓 ∈ 𝐵)
180		simplr 774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿))))
181	180	eldifbd 3896	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → ¬ 𝑓 ∈ (𝑎 supp (0g‘𝐿)))
182	179, 181	eldifd 3894	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → 𝑓 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿))))
183	176, 177, 178, 182	fvdifsupp 8111	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → (𝑎‘𝑓) = (0g‘𝐿))
184		eqidd 2740	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ ¬ 𝑓 ∈ 𝐵) → (0g‘𝐿) = (0g‘𝐿))
185	183, 184	ifeqda 4491	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿)) = (0g‘𝐿))
186	185	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿))(.r‘𝐿)𝑓) = ((0g‘𝐿)(.r‘𝐿)𝑓))
187	27	ad3antrrr 736	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → 𝐿 ∈ Ring)
188	166, 14, 63	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐻 ⊆ (Base‘𝐿))
189	188	ssdifssd 4077	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐻 ∖ (𝑎 supp (0g‘𝐿))) ⊆ (Base‘𝐿))
190	189	sselda 3915	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑓 ∈ (Base‘𝐿))
191	4, 5, 6, 187, 190	ringlzd 20267	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → ((0g‘𝐿)(.r‘𝐿)𝑓) = (0g‘𝐿))
192	175, 186, 191	3eqtrd 2778	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓) = (0g‘𝐿))
193		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝑎 finSupp (0g‘𝐿))
194	193	fsuppimpd 9272	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑎 supp (0g‘𝐿)) ∈ Fin)
195	27	ad3antrrr 736	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ 𝐻) → 𝐿 ∈ Ring)
196	18	ad4antr 738	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) ∧ 𝑔 ∈ 𝐵) → 𝐺 ⊆ (Base‘𝐿))
197	116	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) → 𝑎:𝐵⟶𝐺)
198	197	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) ∧ 𝑔 ∈ 𝐵) → (𝑎‘𝑔) ∈ 𝐺)
199	196, 198	sseldd 3916	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) ∧ 𝑔 ∈ 𝐵) → (𝑎‘𝑔) ∈ (Base‘𝐿))
200	18, 33	sseldd 3916	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝐿) ∈ (Base‘𝐿))
201	200	ad4antr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) ∧ ¬ 𝑔 ∈ 𝐵) → (0g‘𝐿) ∈ (Base‘𝐿))
202	199, 201	ifclda 4490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) ∈ (Base‘𝐿))
203	202	fmpttd 7056	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))):𝐻⟶(Base‘𝐿))
204	203	ffvelcdmda 7025	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ 𝐻) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓) ∈ (Base‘𝐿))
205	188	sselda 3915	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ (Base‘𝐿))
206	4, 5, 195, 204, 205	ringcld 20232	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ 𝐻) → (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓) ∈ (Base‘𝐿))
207	4, 6, 165, 166, 192, 194, 206, 153	gsummptres2 33134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))))
208	113	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
209	126	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑎 Fn 𝐵)
210	208	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
211		fvexd 6842	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → (0g‘𝐿) ∈ V)
212		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿))))
213	209, 210, 211, 212	fvdifsupp 8111	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → (𝑎‘𝑣) = (0g‘𝐿))
214	213	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → ((𝑎‘𝑣)(.r‘𝐿)𝑣) = ((0g‘𝐿)(.r‘𝐿)𝑣))
215	27	ad3antrrr 736	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → 𝐿 ∈ Ring)
216	76	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐵 ⊆ (Base‘𝐿))
217	216	ssdifssd 4077	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐵 ∖ (𝑎 supp (0g‘𝐿))) ⊆ (Base‘𝐿))
218	217	sselda 3915	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑣 ∈ (Base‘𝐿))
219	4, 5, 6, 215, 218	ringlzd 20267	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → ((0g‘𝐿)(.r‘𝐿)𝑣) = (0g‘𝐿))
220	214, 219	eqtrd 2774	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → ((𝑎‘𝑣)(.r‘𝐿)𝑣) = (0g‘𝐿))
221	27	ad3antrrr 736	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → 𝐿 ∈ Ring)
222	18	ad3antrrr 736	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → 𝐺 ⊆ (Base‘𝐿))
223	116	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝑎:𝐵⟶𝐺)
224	223	ffvelcdmda 7025	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → (𝑎‘𝑣) ∈ 𝐺)
225	222, 224	sseldd 3916	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → (𝑎‘𝑣) ∈ (Base‘𝐿))
226	216	sselda 3915	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ (Base‘𝐿))
227	4, 5, 221, 225, 226	ringcld 20232	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → ((𝑎‘𝑣)(.r‘𝐿)𝑣) ∈ (Base‘𝐿))
228	4, 6, 165, 208, 220, 194, 227, 144	gsummptres2 33134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))) = (𝐿 Σg (𝑣 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))
229	164, 207, 228	3eqtr4d 2784	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))
230	229	eqeq2d 2750	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))) ↔ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))))
231	230	biimpar 478	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))) → 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))))
232	231	anasss 467	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))))
233	138, 232	jca 516	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)))))
234	110, 122, 233	rspcedvdw 3563	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → ∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)))))
235	234	r19.29an 3143	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → ∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)))))
236	103, 235	impbida 806	. . . 4 ⊢ (𝜑 → (∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)))) ↔ ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))))
237	52, 79, 236	3bitr4rd 313	. . 3 ⊢ (𝜑 → (∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)))) ↔ 𝑥 ∈ ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝐵)))
238	3, 16, 237	3bitrd 306	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝐵)))
239	238	eqrdv 2737	1 ⊢ (𝜑 → 𝐶 = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∃wrex 3063  Vcvv 3431   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883  ifcif 4454   class class class wbr 5072   ↦ cmpt 5153  dom cdm 5618   Fn wfn 6480  ⟶wf 6481  ‘cfv 6485  (class class class)co 7356   supp csupp 8100   ↑_m cmap 8763  Fincfn 8883   finSupp cfsupp 9264  Basecbs 17170   ↾_s cress 17191  ._rcmulr 17212  Scalarcsca 17214   ·_𝑠 cvsca 17215  0_gc0g 17393   Σ_g cgsu 17394  Mndcmnd 18693  SubGrpcsubg 19087  CMndccmn 19746  Ringcrg 20205  SubRingcsubrg 20541  RingSpancrgspn 20582  Fieldcfield 20702  SubDRingcsdrg 20758  LModclmod 20850  LSpanclspn 20961  LBasisclbs 21064  subringAlg csra 21161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-reg 9497  ax-inf2 9553  ax-ac2 10376  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107  ax-addf 11108

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-iin 4924  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-se 5572  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-isom 6494  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7620  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-tpos 8166  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8633  df-map 8765  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9265  df-sup 9345  df-oi 9415  df-r1 9679  df-rank 9680  df-card 9854  df-ac 10029  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-ind 12151  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-xnn0 12502  df-z 12516  df-dec 12636  df-uz 12780  df-rp 12934  df-fz 13453  df-fzo 13600  df-seq 13955  df-exp 14015  df-hash 14284  df-word 14467  df-lsw 14516  df-concat 14524  df-s1 14550  df-substr 14595  df-pfx 14625  df-s2 14801  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15441  df-sum 15640  df-struct 17108  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192  df-plusg 17224  df-mulr 17225  df-starv 17226  df-sca 17227  df-vsca 17228  df-ip 17229  df-tset 17230  df-ple 17231  df-ds 17233  df-unif 17234  df-hom 17235  df-cco 17236  df-0g 17395  df-gsum 17396  df-prds 17401  df-pws 17403  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-mhm 18742  df-submnd 18743  df-grp 18903  df-minusg 18904  df-sbg 18905  df-mulg 19035  df-subg 19090  df-ghm 19179  df-cntz 19283  df-cmn 19748  df-abl 19749  df-mgp 20113  df-rng 20125  df-ur 20154  df-ring 20207  df-cring 20208  df-oppr 20308  df-nzr 20485  df-subrng 20518  df-subrg 20542  df-rgspn 20583  df-drng 20703  df-field 20704  df-sdrg 20759  df-lmod 20852  df-lss 20922  df-lsp 20962  df-lmhm 21012  df-lbs 21065  df-sra 21163  df-rgmod 21164  df-cnfld 21348  df-zring 21422  df-dsmm 21707  df-frlm 21722  df-uvc 21758

This theorem is referenced by:  fldextrspunlem1  33859