Theorem fldextrspunlsp 33679

Description: Lemma for fldextrspunfld 33681. 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 2817	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ (𝑁‘(𝐺 ∪ 𝐻))))
4		eqid 2731	. . . 4 ⊢ (Base‘𝐿) = (Base‘𝐿)
5		eqid 2731	. . . 4 ⊢ (.r‘𝐿) = (.r‘𝐿)
6		eqid 2731	. . . 4 ⊢ (0g‘𝐿) = (0g‘𝐿)
7		fldextrspunlsp.n	. . . 4 ⊢ 𝑁 = (RingSpan‘𝐿)
8		fldextrspunfld.2	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ Field)
9	8	fldcrngd 20652	. . . 4 ⊢ (𝜑 → 𝐿 ∈ CRing)
10		fldextrspunfld.5	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
11		sdrgsubrg 20701	. . . . 5 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
12	10, 11	syl 17	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
13		fldextrspunfld.6	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
14		sdrgsubrg 20701	. . . . 5 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ∈ (SubRing‘𝐿))
15	13, 14	syl 17	. . . 4 ⊢ (𝜑 → 𝐻 ∈ (SubRing‘𝐿))
16	4, 5, 6, 7, 9, 12, 15	elrgspnsubrun 33208	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝑁‘(𝐺 ∪ 𝐻)) ↔ ∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))))
17	4	subrgss 20482	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
18	12, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
19		eqid 2731	. . . . . . . . 9 ⊢ (𝐿 ↾s 𝐺) = (𝐿 ↾s 𝐺)
20	19, 4	ressbas2 17144	. . . . . . . 8 ⊢ (𝐺 ⊆ (Base‘𝐿) → 𝐺 = (Base‘(𝐿 ↾s 𝐺)))
21	18, 20	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 = (Base‘(𝐿 ↾s 𝐺)))
22		eqidd 2732	. . . . . . . . 9 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺))
23	22, 18	srasca 21109	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ↾s 𝐺) = (Scalar‘((subringAlg ‘𝐿)‘𝐺)))
24	23	fveq2d 6821	. . . . . . 7 ⊢ (𝜑 → (Base‘(𝐿 ↾s 𝐺)) = (Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))))
25	21, 24	eqtr2d 2767	. . . . . 6 ⊢ (𝜑 → (Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) = 𝐺)
26	25	oveq1d 7356	. . . . 5 ⊢ (𝜑 → ((Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ↑m 𝐵) = (𝐺 ↑m 𝐵))
27	9	crngringd 20159	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ Ring)
28	27	ringcmnd 20197	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ CMnd)
29	28	cmnmndd 19711	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ Mnd)
30		subrgsubg 20487	. . . . . . . . . . 11 ⊢ (𝐺 ∈ (SubRing‘𝐿) → 𝐺 ∈ (SubGrp‘𝐿))
31	12, 30	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (SubGrp‘𝐿))
32	6	subg0cl 19042	. . . . . . . . . 10 ⊢ (𝐺 ∈ (SubGrp‘𝐿) → (0g‘𝐿) ∈ 𝐺)
33	31, 32	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (0g‘𝐿) ∈ 𝐺)
34	19, 4, 6	ress0g 18665	. . . . . . . . 9 ⊢ ((𝐿 ∈ Mnd ∧ (0g‘𝐿) ∈ 𝐺 ∧ 𝐺 ⊆ (Base‘𝐿)) → (0g‘𝐿) = (0g‘(𝐿 ↾s 𝐺)))
35	29, 33, 18, 34	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (0g‘𝐿) = (0g‘(𝐿 ↾s 𝐺)))
36	23	fveq2d 6821	. . . . . . . 8 ⊢ (𝜑 → (0g‘(𝐿 ↾s 𝐺)) = (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))))
37	35, 36	eqtr2d 2767	. . . . . . 7 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) = (0g‘𝐿))
38	37	breq2d 5098	. . . . . 6 ⊢ (𝜑 → (𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ↔ 𝑎 finSupp (0g‘𝐿)))
39		eqid 2731	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺)
40		fldextrspunlsp.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
41	40	mptexd 7153	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)) ∈ V)
42	39	sralmod 21116	. . . . . . . . . 10 ⊢ (𝐺 ∈ (SubRing‘𝐿) → ((subringAlg ‘𝐿)‘𝐺) ∈ LMod)
43	12, 42	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐺) ∈ LMod)
44	39, 41, 8, 43, 18	gsumsra 33019	. . . . . . . 8 ⊢ (𝜑 → (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))) = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))
45	22, 18	sravsca 21110	. . . . . . . . . . 11 ⊢ (𝜑 → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺)))
46	45	oveqd 7358	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑎‘𝑣)(.r‘𝐿)𝑣) = ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣))
47	46	mpteq2dv 5180	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)) = (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣)))
48	47	oveq2d 7357	. . . . . . . 8 ⊢ (𝜑 → (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))) = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣))))
49	44, 48	eqtr2d 2767	. . . . . . 7 ⊢ (𝜑 → (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣))) = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))
50	49	eqeq2d 2742	. . . . . 6 ⊢ (𝜑 → (𝑥 = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣))) ↔ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))))
51	38, 50	anbi12d 632	. . . . 5 ⊢ (𝜑 → ((𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ∧ 𝑥 = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣)))) ↔ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))))
52	26, 51	rexeqbidv 3313	. . . 4 ⊢ (𝜑 → (∃𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ↑m 𝐵)(𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ∧ 𝑥 = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣)))) ↔ ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))))
53		eqid 2731	. . . . 5 ⊢ (LSpan‘((subringAlg ‘𝐿)‘𝐺)) = (LSpan‘((subringAlg ‘𝐿)‘𝐺))
54		eqid 2731	. . . . 5 ⊢ (Base‘((subringAlg ‘𝐿)‘𝐺)) = (Base‘((subringAlg ‘𝐿)‘𝐺))
55		eqid 2731	. . . . 5 ⊢ (Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) = (Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺)))
56		eqid 2731	. . . . 5 ⊢ (Scalar‘((subringAlg ‘𝐿)‘𝐺)) = (Scalar‘((subringAlg ‘𝐿)‘𝐺))
57		eqid 2731	. . . . 5 ⊢ (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) = (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺)))
58		eqid 2731	. . . . 5 ⊢ ( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺)) = ( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))
59		eqid 2731	. . . . . . . . . 10 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
60		eqid 2731	. . . . . . . . . 10 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
61	59, 60	lbsss 21006	. . . . . . . . 9 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
62	40, 61	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
63	4	subrgss 20482	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
64	15, 63	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
65		fldextrspunfld.j	. . . . . . . . . . 11 ⊢ 𝐽 = (𝐿 ↾s 𝐻)
66	65, 4	ressbas2 17144	. . . . . . . . . 10 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
67	64, 66	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
68		eqidd 2732	. . . . . . . . . 10 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
69		fldextrspunfld.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
70		eqid 2731	. . . . . . . . . . . 12 ⊢ (Base‘𝐽) = (Base‘𝐽)
71	70	sdrgss 20703	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
72	69, 71	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
73	68, 72	srabase 21106	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
74	67, 73	eqtrd 2766	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
75	62, 74	sseqtrrd 3967	. . . . . . 7 ⊢ (𝜑 → 𝐵 ⊆ 𝐻)
76	75, 64	sstrd 3940	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝐿))
77	22, 18	srabase 21106	. . . . . 6 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
78	76, 77	sseqtrd 3966	. . . . 5 ⊢ (𝜑 → 𝐵 ⊆ (Base‘((subringAlg ‘𝐿)‘𝐺)))
79	53, 54, 55, 56, 57, 58, 43, 78	ellspds 33325	. . . 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 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐿 ∈ Field)
83		fldextrspunfld.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
84	83	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐹 ∈ (SubDRing‘𝐼))
85	69	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐹 ∈ (SubDRing‘𝐽))
86	10	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐺 ∈ (SubDRing‘𝐿))
87	13	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐻 ∈ (SubDRing‘𝐿))
88		fldextrspunlsp.e	. . . . . . 7 ⊢ 𝐸 = (𝐿 ↾s 𝐶)
89	40	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
90		fldextrspunlsp.2	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ Fin)
91	90	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝐵 ∈ Fin)
92		simplr 768	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝑝 ∈ (𝐺 ↑m 𝐻))
93	87, 86, 92	elmaprd 32653	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝑝:𝐻⟶𝐺)
94		simprl 770	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝑝 finSupp (0g‘𝐿))
95		simprr 772	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))
96		fveq2 6817	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (𝑝‘𝑓) = (𝑝‘ℎ))
97		id 22	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → 𝑓 = ℎ)
98	96, 97	oveq12d 7359	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑝‘𝑓)(.r‘𝐿)𝑓) = ((𝑝‘ℎ)(.r‘𝐿)ℎ))
99	98	cbvmptv 5190	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)) = (ℎ ∈ 𝐻 ↦ ((𝑝‘ℎ)(.r‘𝐿)ℎ))
100	99	oveq2i 7352	. . . . . . . 8 ⊢ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑝‘ℎ)(.r‘𝐿)ℎ)))
101	95, 100	eqtrdi 2782	. . . . . . 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 33678	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))))
103	102	r19.29an 3136	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))))
104		breq1 5089	. . . . . . . 8 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝑝 finSupp (0g‘𝐿) ↔ (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) finSupp (0g‘𝐿)))
105		fveq1 6816	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝑝‘𝑓) = ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓))
106	105	oveq1d 7356	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → ((𝑝‘𝑓)(.r‘𝐿)𝑓) = (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))
107	106	mpteq2dv 5180	. . . . . . . . . 10 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)) = (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)))
108	107	oveq2d 7357	. . . . . . . . 9 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))))
109	108	eqeq2d 2742	. . . . . . . 8 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))) ↔ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)))))
110	104, 109	anbi12d 632	. . . . . . 7 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → ((𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)))) ↔ ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))))))
111	10	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → 𝐺 ∈ (SubDRing‘𝐿))
112	13	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → 𝐻 ∈ (SubDRing‘𝐿))
113	40	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
114	10	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → 𝐺 ∈ (SubDRing‘𝐿))
115		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → 𝑎 ∈ (𝐺 ↑m 𝐵))
116	113, 114, 115	elmaprd 32653	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → 𝑎:𝐵⟶𝐺)
117	116	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ 𝐻) → 𝑎:𝐵⟶𝐺)
118	117	ffvelcdmda 7012	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ 𝐻) ∧ 𝑔 ∈ 𝐵) → (𝑎‘𝑔) ∈ 𝐺)
119	33	ad4antr 732	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ 𝐻) ∧ ¬ 𝑔 ∈ 𝐵) → (0g‘𝐿) ∈ 𝐺)
120	118, 119	ifclda 4506	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ 𝐻) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) ∈ 𝐺)
121	120	fmpttd 7043	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))):𝐻⟶𝐺)
122	111, 112, 121	elmapdd 8760	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) ∈ (𝐺 ↑m 𝐻))
123		fvexd 6832	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → (0g‘𝐿) ∈ V)
124	121	ffund 6650	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → Fun (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))))
125		simprl 770	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → 𝑎 finSupp (0g‘𝐿))
126	116	ffnd 6647	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → 𝑎 Fn 𝐵)
127	126	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → 𝑎 Fn 𝐵)
128	40	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
129		fvexd 6832	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → (0g‘𝐿) ∈ V)
130		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ 𝐵)
131		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿))))
132	131	eldifbd 3910	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → ¬ 𝑔 ∈ (𝑎 supp (0g‘𝐿)))
133	130, 132	eldifd 3908	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿))))
134	127, 128, 129, 133	fvdifsupp 8096	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → (𝑎‘𝑔) = (0g‘𝐿))
135		eqidd 2732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ ¬ 𝑔 ∈ 𝐵) → (0g‘𝐿) = (0g‘𝐿))
136	134, 135	ifeqda 4507	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) = (0g‘𝐿))
137	136, 112	suppss2 8125	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) supp (0g‘𝐿)) ⊆ (𝑎 supp (0g‘𝐿)))
138	122, 123, 124, 125, 137	fsuppsssuppgd 9261	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) finSupp (0g‘𝐿))
139		eqid 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))
140		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → 𝑔 = 𝑓)
141		suppssdm 8102	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 supp (0g‘𝐿)) ⊆ dom 𝑎
142	116	fdmd 6656	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → dom 𝑎 = 𝐵)
143	142	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → dom 𝑎 = 𝐵)
144	141, 143	sseqtrid 3972	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑎 supp (0g‘𝐿)) ⊆ 𝐵)
145	144	sselda 3929	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → 𝑓 ∈ 𝐵)
146	145	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → 𝑓 ∈ 𝐵)
147	140, 146	eqeltrd 2831	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → 𝑔 ∈ 𝐵)
148	147	iftrued 4478	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) = (𝑎‘𝑔))
149		fveq2 6817	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → (𝑎‘𝑔) = (𝑎‘𝑓))
150	149	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → (𝑎‘𝑔) = (𝑎‘𝑓))
151	148, 150	eqtrd 2766	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) = (𝑎‘𝑓))
152	75	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐵 ⊆ 𝐻)
153	144, 152	sstrd 3940	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑎 supp (0g‘𝐿)) ⊆ 𝐻)
154	153	sselda 3929	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → 𝑓 ∈ 𝐻)
155		fvexd 6832	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → (𝑎‘𝑓) ∈ V)
156	139, 151, 154, 155	fvmptd2 6932	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓) = (𝑎‘𝑓))
157	156	oveq1d 7356	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓) = ((𝑎‘𝑓)(.r‘𝐿)𝑓))
158	157	mpteq2dva 5179	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)) = (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑓)(.r‘𝐿)𝑓)))
159		fveq2 6817	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑣 → (𝑎‘𝑓) = (𝑎‘𝑣))
160		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑣 → 𝑓 = 𝑣)
161	159, 160	oveq12d 7359	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑣 → ((𝑎‘𝑓)(.r‘𝐿)𝑓) = ((𝑎‘𝑣)(.r‘𝐿)𝑣))
162	161	cbvmptv 5190	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑓)(.r‘𝐿)𝑓)) = (𝑣 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))
163	158, 162	eqtrdi 2782	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)) = (𝑣 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))
164	163	oveq2d 7357	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐿 Σg (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑣 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))
165	28	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐿 ∈ CMnd)
166	13	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐻 ∈ (SubDRing‘𝐿))
167		eleq1w 2814	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑓 → (𝑔 ∈ 𝐵 ↔ 𝑓 ∈ 𝐵))
168	167, 149	ifbieq1d 4495	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑓 → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) = if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿)))
169		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿))))
170	169	eldifad 3909	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑓 ∈ 𝐻)
171		fvexd 6832	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (𝑎‘𝑓) ∈ V)
172		fvexd 6832	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (0g‘𝐿) ∈ V)
173	171, 172	ifcld 4517	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿)) ∈ V)
174	139, 168, 170, 173	fvmptd3 6947	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓) = if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿)))
175	174	oveq1d 7356	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓) = (if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿))(.r‘𝐿)𝑓))
176	126	ad3antrrr 730	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → 𝑎 Fn 𝐵)
177	40	ad4antr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
178		fvexd 6832	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → (0g‘𝐿) ∈ V)
179		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → 𝑓 ∈ 𝐵)
180		simplr 768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿))))
181	180	eldifbd 3910	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → ¬ 𝑓 ∈ (𝑎 supp (0g‘𝐿)))
182	179, 181	eldifd 3908	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → 𝑓 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿))))
183	176, 177, 178, 182	fvdifsupp 8096	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → (𝑎‘𝑓) = (0g‘𝐿))
184		eqidd 2732	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ ¬ 𝑓 ∈ 𝐵) → (0g‘𝐿) = (0g‘𝐿))
185	183, 184	ifeqda 4507	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿)) = (0g‘𝐿))
186	185	oveq1d 7356	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿))(.r‘𝐿)𝑓) = ((0g‘𝐿)(.r‘𝐿)𝑓))
187	27	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → 𝐿 ∈ Ring)
188	166, 14, 63	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐻 ⊆ (Base‘𝐿))
189	188	ssdifssd 4092	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐻 ∖ (𝑎 supp (0g‘𝐿))) ⊆ (Base‘𝐿))
190	189	sselda 3929	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑓 ∈ (Base‘𝐿))
191	4, 5, 6, 187, 190	ringlzd 20208	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → ((0g‘𝐿)(.r‘𝐿)𝑓) = (0g‘𝐿))
192	175, 186, 191	3eqtrd 2770	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓) = (0g‘𝐿))
193		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝑎 finSupp (0g‘𝐿))
194	193	fsuppimpd 9248	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑎 supp (0g‘𝐿)) ∈ Fin)
195	27	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ 𝐻) → 𝐿 ∈ Ring)
196	18	ad4antr 732	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) ∧ 𝑔 ∈ 𝐵) → 𝐺 ⊆ (Base‘𝐿))
197	116	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) → 𝑎:𝐵⟶𝐺)
198	197	ffvelcdmda 7012	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) ∧ 𝑔 ∈ 𝐵) → (𝑎‘𝑔) ∈ 𝐺)
199	196, 198	sseldd 3930	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) ∧ 𝑔 ∈ 𝐵) → (𝑎‘𝑔) ∈ (Base‘𝐿))
200	18, 33	sseldd 3930	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝐿) ∈ (Base‘𝐿))
201	200	ad4antr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) ∧ ¬ 𝑔 ∈ 𝐵) → (0g‘𝐿) ∈ (Base‘𝐿))
202	199, 201	ifclda 4506	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) ∈ (Base‘𝐿))
203	202	fmpttd 7043	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))):𝐻⟶(Base‘𝐿))
204	203	ffvelcdmda 7012	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ 𝐻) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓) ∈ (Base‘𝐿))
205	188	sselda 3929	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ (Base‘𝐿))
206	4, 5, 195, 204, 205	ringcld 20173	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ 𝐻) → (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓) ∈ (Base‘𝐿))
207	4, 6, 165, 166, 192, 194, 206, 153	gsummptres2 33025	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))))
208	113	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
209	126	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑎 Fn 𝐵)
210	208	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
211		fvexd 6832	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → (0g‘𝐿) ∈ V)
212		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿))))
213	209, 210, 211, 212	fvdifsupp 8096	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → (𝑎‘𝑣) = (0g‘𝐿))
214	213	oveq1d 7356	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → ((𝑎‘𝑣)(.r‘𝐿)𝑣) = ((0g‘𝐿)(.r‘𝐿)𝑣))
215	27	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → 𝐿 ∈ Ring)
216	76	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐵 ⊆ (Base‘𝐿))
217	216	ssdifssd 4092	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐵 ∖ (𝑎 supp (0g‘𝐿))) ⊆ (Base‘𝐿))
218	217	sselda 3929	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑣 ∈ (Base‘𝐿))
219	4, 5, 6, 215, 218	ringlzd 20208	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → ((0g‘𝐿)(.r‘𝐿)𝑣) = (0g‘𝐿))
220	214, 219	eqtrd 2766	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → ((𝑎‘𝑣)(.r‘𝐿)𝑣) = (0g‘𝐿))
221	27	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → 𝐿 ∈ Ring)
222	18	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → 𝐺 ⊆ (Base‘𝐿))
223	116	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝑎:𝐵⟶𝐺)
224	223	ffvelcdmda 7012	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → (𝑎‘𝑣) ∈ 𝐺)
225	222, 224	sseldd 3930	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → (𝑎‘𝑣) ∈ (Base‘𝐿))
226	216	sselda 3929	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ (Base‘𝐿))
227	4, 5, 221, 225, 226	ringcld 20173	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → ((𝑎‘𝑣)(.r‘𝐿)𝑣) ∈ (Base‘𝐿))
228	4, 6, 165, 208, 220, 194, 227, 144	gsummptres2 33025	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))) = (𝐿 Σg (𝑣 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))
229	164, 207, 228	3eqtr4d 2776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))
230	229	eqeq2d 2742	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))) ↔ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))))
231	230	biimpar 477	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))) → 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))))
232	231	anasss 466	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))))
233	138, 232	jca 511	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)))))
234	110, 122, 233	rspcedvdw 3575	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → ∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)))))
235	234	r19.29an 3136	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → ∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)))))
236	103, 235	impbida 800	. . . 4 ⊢ (𝜑 → (∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)))) ↔ ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))))
237	52, 79, 236	3bitr4rd 312	. . 3 ⊢ (𝜑 → (∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)))) ↔ 𝑥 ∈ ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝐵)))
238	3, 16, 237	3bitrd 305	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝐵)))
239	238	eqrdv 2729	1 ⊢ (𝜑 → 𝐶 = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∃wrex 3056  Vcvv 3436   ∖ cdif 3894   ∪ cun 3895   ⊆ wss 3897  ifcif 4470   class class class wbr 5086   ↦ cmpt 5167  dom cdm 5611   Fn wfn 6471  ⟶wf 6472  ‘cfv 6476  (class class class)co 7341   supp csupp 8085   ↑_m cmap 8745  Fincfn 8864   finSupp cfsupp 9240  Basecbs 17115   ↾_s cress 17136  ._rcmulr 17157  Scalarcsca 17159   ·_𝑠 cvsca 17160  0_gc0g 17338   Σ_g cgsu 17339  Mndcmnd 18637  SubGrpcsubg 19028  CMndccmn 19687  Ringcrg 20146  SubRingcsubrg 20479  RingSpancrgspn 20520  Fieldcfield 20640  SubDRingcsdrg 20696  LModclmod 20788  LSpanclspn 20899  LBasisclbs 21003  subringAlg csra 21100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5212  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-reg 9473  ax-inf2 9526  ax-ac2 10349  ax-cnex 11057  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-mulcom 11065  ax-addass 11066  ax-mulass 11067  ax-distr 11068  ax-i2m1 11069  ax-1ne0 11070  ax-1rid 11071  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074  ax-pre-lttri 11075  ax-pre-lttrn 11076  ax-pre-ltadd 11077  ax-pre-mulgt0 11078  ax-pre-sup 11079  ax-addf 11080

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4855  df-int 4893  df-iun 4938  df-iin 4939  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-se 5565  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-isom 6485  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-of 7605  df-om 7792  df-1st 7916  df-2nd 7917  df-supp 8086  df-tpos 8151  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-1o 8380  df-2o 8381  df-er 8617  df-map 8747  df-ixp 8817  df-en 8865  df-dom 8866  df-sdom 8867  df-fin 8868  df-fsupp 9241  df-sup 9321  df-oi 9391  df-r1 9652  df-rank 9653  df-card 9827  df-ac 10002  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147  df-sub 11341  df-neg 11342  df-div 11770  df-nn 12121  df-2 12183  df-3 12184  df-4 12185  df-5 12186  df-6 12187  df-7 12188  df-8 12189  df-9 12190  df-n0 12377  df-xnn0 12450  df-z 12464  df-dec 12584  df-uz 12728  df-rp 12886  df-fz 13403  df-fzo 13550  df-seq 13904  df-exp 13964  df-hash 14233  df-word 14416  df-lsw 14465  df-concat 14473  df-s1 14499  df-substr 14544  df-pfx 14574  df-s2 14750  df-cj 15001  df-re 15002  df-im 15003  df-sqrt 15137  df-abs 15138  df-clim 15390  df-sum 15589  df-struct 17053  df-sets 17070  df-slot 17088  df-ndx 17100  df-base 17116  df-ress 17137  df-plusg 17169  df-mulr 17170  df-starv 17171  df-sca 17172  df-vsca 17173  df-ip 17174  df-tset 17175  df-ple 17176  df-ds 17178  df-unif 17179  df-hom 17180  df-cco 17181  df-0g 17340  df-gsum 17341  df-prds 17346  df-pws 17348  df-mre 17483  df-mrc 17484  df-acs 17486  df-mgm 18543  df-sgrp 18622  df-mnd 18638  df-mhm 18686  df-submnd 18687  df-grp 18844  df-minusg 18845  df-sbg 18846  df-mulg 18976  df-subg 19031  df-ghm 19120  df-cntz 19224  df-cmn 19689  df-abl 19690  df-mgp 20054  df-rng 20066  df-ur 20095  df-ring 20148  df-cring 20149  df-oppr 20250  df-nzr 20423  df-subrng 20456  df-subrg 20480  df-rgspn 20521  df-drng 20641  df-field 20642  df-sdrg 20697  df-lmod 20790  df-lss 20860  df-lsp 20900  df-lmhm 20951  df-lbs 21004  df-sra 21102  df-rgmod 21103  df-cnfld 21287  df-zring 21379  df-dsmm 21664  df-frlm 21679  df-uvc 21715  df-ind 32824

This theorem is referenced by:  fldextrspunlem1  33680