Theorem fldextrspunlsp 33660

Description: Lemma for fldextrspunfld 33662. 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 2814	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ (𝑁‘(𝐺 ∪ 𝐻))))
4		eqid 2729	. . . 4 ⊢ (Base‘𝐿) = (Base‘𝐿)
5		eqid 2729	. . . 4 ⊢ (.r‘𝐿) = (.r‘𝐿)
6		eqid 2729	. . . 4 ⊢ (0g‘𝐿) = (0g‘𝐿)
7		fldextrspunlsp.n	. . . 4 ⊢ 𝑁 = (RingSpan‘𝐿)
8		fldextrspunfld.2	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ Field)
9	8	fldcrngd 20646	. . . 4 ⊢ (𝜑 → 𝐿 ∈ CRing)
10		fldextrspunfld.5	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
11		sdrgsubrg 20695	. . . . 5 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
12	10, 11	syl 17	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
13		fldextrspunfld.6	. . . . 5 ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
14		sdrgsubrg 20695	. . . . 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 20476	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
18	12, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
19		eqid 2729	. . . . . . . . 9 ⊢ (𝐿 ↾s 𝐺) = (𝐿 ↾s 𝐺)
20	19, 4	ressbas2 17168	. . . . . . . 8 ⊢ (𝐺 ⊆ (Base‘𝐿) → 𝐺 = (Base‘(𝐿 ↾s 𝐺)))
21	18, 20	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 = (Base‘(𝐿 ↾s 𝐺)))
22		eqidd 2730	. . . . . . . . 9 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺))
23	22, 18	srasca 21103	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ↾s 𝐺) = (Scalar‘((subringAlg ‘𝐿)‘𝐺)))
24	23	fveq2d 6830	. . . . . . 7 ⊢ (𝜑 → (Base‘(𝐿 ↾s 𝐺)) = (Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))))
25	21, 24	eqtr2d 2765	. . . . . 6 ⊢ (𝜑 → (Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) = 𝐺)
26	25	oveq1d 7368	. . . . 5 ⊢ (𝜑 → ((Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ↑m 𝐵) = (𝐺 ↑m 𝐵))
27	9	crngringd 20150	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ Ring)
28	27	ringcmnd 20188	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ CMnd)
29	28	cmnmndd 19702	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ Mnd)
30		subrgsubg 20481	. . . . . . . . . . 11 ⊢ (𝐺 ∈ (SubRing‘𝐿) → 𝐺 ∈ (SubGrp‘𝐿))
31	12, 30	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (SubGrp‘𝐿))
32	6	subg0cl 19032	. . . . . . . . . 10 ⊢ (𝐺 ∈ (SubGrp‘𝐿) → (0g‘𝐿) ∈ 𝐺)
33	31, 32	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (0g‘𝐿) ∈ 𝐺)
34	19, 4, 6	ress0g 18655	. . . . . . . . 9 ⊢ ((𝐿 ∈ Mnd ∧ (0g‘𝐿) ∈ 𝐺 ∧ 𝐺 ⊆ (Base‘𝐿)) → (0g‘𝐿) = (0g‘(𝐿 ↾s 𝐺)))
35	29, 33, 18, 34	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (0g‘𝐿) = (0g‘(𝐿 ↾s 𝐺)))
36	23	fveq2d 6830	. . . . . . . 8 ⊢ (𝜑 → (0g‘(𝐿 ↾s 𝐺)) = (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))))
37	35, 36	eqtr2d 2765	. . . . . . 7 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) = (0g‘𝐿))
38	37	breq2d 5107	. . . . . 6 ⊢ (𝜑 → (𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ↔ 𝑎 finSupp (0g‘𝐿)))
39		eqid 2729	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐿)‘𝐺) = ((subringAlg ‘𝐿)‘𝐺)
40		fldextrspunlsp.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
41	40	mptexd 7164	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)) ∈ V)
42	39	sralmod 21110	. . . . . . . . . 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 21104	. . . . . . . . . . 11 ⊢ (𝜑 → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺)))
46	45	oveqd 7370	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑎‘𝑣)(.r‘𝐿)𝑣) = ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣))
47	46	mpteq2dv 5189	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)) = (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣)))
48	47	oveq2d 7369	. . . . . . . 8 ⊢ (𝜑 → (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))) = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣))))
49	44, 48	eqtr2d 2765	. . . . . . 7 ⊢ (𝜑 → (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣))) = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))
50	49	eqeq2d 2740	. . . . . 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 3311	. . . 4 ⊢ (𝜑 → (∃𝑎 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ↑m 𝐵)(𝑎 finSupp (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) ∧ 𝑥 = (((subringAlg ‘𝐿)‘𝐺) Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))𝑣)))) ↔ ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))))
53		eqid 2729	. . . . 5 ⊢ (LSpan‘((subringAlg ‘𝐿)‘𝐺)) = (LSpan‘((subringAlg ‘𝐿)‘𝐺))
54		eqid 2729	. . . . 5 ⊢ (Base‘((subringAlg ‘𝐿)‘𝐺)) = (Base‘((subringAlg ‘𝐿)‘𝐺))
55		eqid 2729	. . . . 5 ⊢ (Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) = (Base‘(Scalar‘((subringAlg ‘𝐿)‘𝐺)))
56		eqid 2729	. . . . 5 ⊢ (Scalar‘((subringAlg ‘𝐿)‘𝐺)) = (Scalar‘((subringAlg ‘𝐿)‘𝐺))
57		eqid 2729	. . . . 5 ⊢ (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺))) = (0g‘(Scalar‘((subringAlg ‘𝐿)‘𝐺)))
58		eqid 2729	. . . . 5 ⊢ ( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺)) = ( ·𝑠 ‘((subringAlg ‘𝐿)‘𝐺))
59		eqid 2729	. . . . . . . . . 10 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
60		eqid 2729	. . . . . . . . . 10 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
61	59, 60	lbsss 21000	. . . . . . . . 9 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
62	40, 61	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
63	4	subrgss 20476	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
64	15, 63	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
65		fldextrspunfld.j	. . . . . . . . . . 11 ⊢ 𝐽 = (𝐿 ↾s 𝐻)
66	65, 4	ressbas2 17168	. . . . . . . . . 10 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
67	64, 66	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
68		eqidd 2730	. . . . . . . . . 10 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
69		fldextrspunfld.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
70		eqid 2729	. . . . . . . . . . . 12 ⊢ (Base‘𝐽) = (Base‘𝐽)
71	70	sdrgss 20697	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
72	69, 71	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
73	68, 72	srabase 21100	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
74	67, 73	eqtrd 2764	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (Base‘((subringAlg ‘𝐽)‘𝐹)))
75	62, 74	sseqtrrd 3975	. . . . . . 7 ⊢ (𝜑 → 𝐵 ⊆ 𝐻)
76	75, 64	sstrd 3948	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝐿))
77	22, 18	srabase 21100	. . . . . 6 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐺)))
78	76, 77	sseqtrd 3974	. . . . 5 ⊢ (𝜑 → 𝐵 ⊆ (Base‘((subringAlg ‘𝐿)‘𝐺)))
79	53, 54, 55, 56, 57, 58, 43, 78	ellspds 33324	. . . 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 32641	. . . . . . 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 6826	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (𝑝‘𝑓) = (𝑝‘ℎ))
97		id 22	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → 𝑓 = ℎ)
98	96, 97	oveq12d 7371	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑝‘𝑓)(.r‘𝐿)𝑓) = ((𝑝‘ℎ)(.r‘𝐿)ℎ))
99	98	cbvmptv 5199	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)) = (ℎ ∈ 𝐻 ↦ ((𝑝‘ℎ)(.r‘𝐿)ℎ))
100	99	oveq2i 7364	. . . . . . . 8 ⊢ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑝‘ℎ)(.r‘𝐿)ℎ)))
101	95, 100	eqtrdi 2780	. . . . . . 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 33659	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ (𝐺 ↑m 𝐻)) ∧ (𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))))
103	102	r19.29an 3133	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))))) → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))))
104		breq1 5098	. . . . . . . 8 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝑝 finSupp (0g‘𝐿) ↔ (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) finSupp (0g‘𝐿)))
105		fveq1 6825	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝑝‘𝑓) = ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓))
106	105	oveq1d 7368	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → ((𝑝‘𝑓)(.r‘𝐿)𝑓) = (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))
107	106	mpteq2dv 5189	. . . . . . . . . 10 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)) = (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)))
108	107	oveq2d 7369	. . . . . . . . 9 ⊢ (𝑝 = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))))
109	108	eqeq2d 2740	. . . . . . . 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 32641	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → 𝑎:𝐵⟶𝐺)
117	116	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ 𝐻) → 𝑎:𝐵⟶𝐺)
118	117	ffvelcdmda 7022	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ 𝐻) ∧ 𝑔 ∈ 𝐵) → (𝑎‘𝑔) ∈ 𝐺)
119	33	ad4antr 732	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ 𝐻) ∧ ¬ 𝑔 ∈ 𝐵) → (0g‘𝐿) ∈ 𝐺)
120	118, 119	ifclda 4514	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ 𝐻) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) ∈ 𝐺)
121	120	fmpttd 7053	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))):𝐻⟶𝐺)
122	111, 112, 121	elmapdd 8775	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) ∈ (𝐺 ↑m 𝐻))
123		fvexd 6841	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → (0g‘𝐿) ∈ V)
124	121	ffund 6660	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → Fun (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))))
125		simprl 770	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → 𝑎 finSupp (0g‘𝐿))
126	116	ffnd 6657	. . . . . . . . . . . . 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 6841	. . . . . . . . . . . 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 3918	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑔 ∈ 𝐵) → ¬ 𝑔 ∈ (𝑎 supp (0g‘𝐿)))
133	130, 132	eldifd 3916	. . . . . . . . . . . 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 2730	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) ∧ 𝑔 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ ¬ 𝑔 ∈ 𝐵) → (0g‘𝐿) = (0g‘𝐿))
136	134, 135	ifeqda 4515	. . . . . . . . . 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 9291	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) finSupp (0g‘𝐿))
139		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))) = (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))
140		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → 𝑔 = 𝑓)
141		suppssdm 8117	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 supp (0g‘𝐿)) ⊆ dom 𝑎
142	116	fdmd 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) → dom 𝑎 = 𝐵)
143	142	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → dom 𝑎 = 𝐵)
144	141, 143	sseqtrid 3980	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑎 supp (0g‘𝐿)) ⊆ 𝐵)
145	144	sselda 3937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → 𝑓 ∈ 𝐵)
146	145	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → 𝑓 ∈ 𝐵)
147	140, 146	eqeltrd 2828	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → 𝑔 ∈ 𝐵)
148	147	iftrued 4486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) = (𝑎‘𝑔))
149		fveq2 6826	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → (𝑎‘𝑔) = (𝑎‘𝑓))
150	149	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → (𝑎‘𝑔) = (𝑎‘𝑓))
151	148, 150	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) ∧ 𝑔 = 𝑓) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) = (𝑎‘𝑓))
152	75	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝐵 ⊆ 𝐻)
153	144, 152	sstrd 3948	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑎 supp (0g‘𝐿)) ⊆ 𝐻)
154	153	sselda 3937	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → 𝑓 ∈ 𝐻)
155		fvexd 6841	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → (𝑎‘𝑓) ∈ V)
156	139, 151, 154, 155	fvmptd2 6942	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓) = (𝑎‘𝑓))
157	156	oveq1d 7368	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝑎 supp (0g‘𝐿))) → (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓) = ((𝑎‘𝑓)(.r‘𝐿)𝑓))
158	157	mpteq2dva 5188	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)) = (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑓)(.r‘𝐿)𝑓)))
159		fveq2 6826	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑣 → (𝑎‘𝑓) = (𝑎‘𝑣))
160		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑣 → 𝑓 = 𝑣)
161	159, 160	oveq12d 7371	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑣 → ((𝑎‘𝑓)(.r‘𝐿)𝑓) = ((𝑎‘𝑣)(.r‘𝐿)𝑣))
162	161	cbvmptv 5199	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑓)(.r‘𝐿)𝑓)) = (𝑣 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))
163	158, 162	eqtrdi 2780	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑓 ∈ (𝑎 supp (0g‘𝐿)) ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓)) = (𝑣 ∈ (𝑎 supp (0g‘𝐿)) ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣)))
164	163	oveq2d 7369	. . . . . . . . . . . 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 2811	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑓 → (𝑔 ∈ 𝐵 ↔ 𝑓 ∈ 𝐵))
168	167, 149	ifbieq1d 4503	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑓 → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) = if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿)))
169		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿))))
170	169	eldifad 3917	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑓 ∈ 𝐻)
171		fvexd 6841	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (𝑎‘𝑓) ∈ V)
172		fvexd 6841	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (0g‘𝐿) ∈ V)
173	171, 172	ifcld 4525	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿)) ∈ V)
174	139, 168, 170, 173	fvmptd3 6957	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓) = if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿)))
175	174	oveq1d 7368	. . . . . . . . . . . . . 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 6841	. . . . . . . . . . . . . . . . 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 3918	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → ¬ 𝑓 ∈ (𝑎 supp (0g‘𝐿)))
182	179, 181	eldifd 3916	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → 𝑓 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿))))
183	176, 177, 178, 182	fvdifsupp 8111	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ 𝑓 ∈ 𝐵) → (𝑎‘𝑓) = (0g‘𝐿))
184		eqidd 2730	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) ∧ ¬ 𝑓 ∈ 𝐵) → (0g‘𝐿) = (0g‘𝐿))
185	183, 184	ifeqda 4515	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → if(𝑓 ∈ 𝐵, (𝑎‘𝑓), (0g‘𝐿)) = (0g‘𝐿))
186	185	oveq1d 7368	. . . . . . . . . . . . . 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 4100	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐻 ∖ (𝑎 supp (0g‘𝐿))) ⊆ (Base‘𝐿))
190	189	sselda 3937	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑓 ∈ (Base‘𝐿))
191	4, 5, 6, 187, 190	ringlzd 20199	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → ((0g‘𝐿)(.r‘𝐿)𝑓) = (0g‘𝐿))
192	175, 186, 191	3eqtrd 2768	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ (𝐻 ∖ (𝑎 supp (0g‘𝐿)))) → (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓) = (0g‘𝐿))
193		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → 𝑎 finSupp (0g‘𝐿))
194	193	fsuppimpd 9278	. . . . . . . . . . . . 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 7022	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) ∧ 𝑔 ∈ 𝐵) → (𝑎‘𝑔) ∈ 𝐺)
199	196, 198	sseldd 3938	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) ∧ 𝑔 ∈ 𝐵) → (𝑎‘𝑔) ∈ (Base‘𝐿))
200	18, 33	sseldd 3938	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝐿) ∈ (Base‘𝐿))
201	200	ad4antr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) ∧ ¬ 𝑔 ∈ 𝐵) → (0g‘𝐿) ∈ (Base‘𝐿))
202	199, 201	ifclda 4514	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑔 ∈ 𝐻) → if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)) ∈ (Base‘𝐿))
203	202	fmpttd 7053	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿))):𝐻⟶(Base‘𝐿))
204	203	ffvelcdmda 7022	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ 𝐻) → ((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓) ∈ (Base‘𝐿))
205	188	sselda 3937	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ (Base‘𝐿))
206	4, 5, 195, 204, 205	ringcld 20164	. . . . . . . . . . . . 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 6841	. . . . . . . . . . . . . . . 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 8111	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → (𝑎‘𝑣) = (0g‘𝐿))
214	213	oveq1d 7368	. . . . . . . . . . . . . 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 4100	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐵 ∖ (𝑎 supp (0g‘𝐿))) ⊆ (Base‘𝐿))
218	217	sselda 3937	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → 𝑣 ∈ (Base‘𝐿))
219	4, 5, 6, 215, 218	ringlzd 20199	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ (𝐵 ∖ (𝑎 supp (0g‘𝐿)))) → ((0g‘𝐿)(.r‘𝐿)𝑣) = (0g‘𝐿))
220	214, 219	eqtrd 2764	. . . . . . . . . . . . 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 7022	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → (𝑎‘𝑣) ∈ 𝐺)
225	222, 224	sseldd 3938	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → (𝑎‘𝑣) ∈ (Base‘𝐿))
226	216	sselda 3937	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ (Base‘𝐿))
227	4, 5, 221, 225, 226	ringcld 20164	. . . . . . . . . . . . 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 2774	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ 𝑎 finSupp (0g‘𝐿)) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ (((𝑔 ∈ 𝐻 ↦ if(𝑔 ∈ 𝐵, (𝑎‘𝑔), (0g‘𝐿)))‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))
230	229	eqeq2d 2740	. . . . . . . . . 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 3582	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐺 ↑m 𝐵)) ∧ (𝑎 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑣 ∈ 𝐵 ↦ ((𝑎‘𝑣)(.r‘𝐿)𝑣))))) → ∃𝑝 ∈ (𝐺 ↑m 𝐻)(𝑝 finSupp (0g‘𝐿) ∧ 𝑥 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑝‘𝑓)(.r‘𝐿)𝑓)))))
235	234	r19.29an 3133	. . . . 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 2727	1 ⊢ (𝜑 → 𝐶 = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  Vcvv 3438   ∖ cdif 3902   ∪ cun 3903   ⊆ wss 3905  ifcif 4478   class class class wbr 5095   ↦ cmpt 5176  dom cdm 5623   Fn wfn 6481  ⟶wf 6482  ‘cfv 6486  (class class class)co 7353   supp csupp 8100   ↑_m cmap 8760  Fincfn 8879   finSupp cfsupp 9270  Basecbs 17139   ↾_s cress 17160  ._rcmulr 17181  Scalarcsca 17183   ·_𝑠 cvsca 17184  0_gc0g 17362   Σ_g cgsu 17363  Mndcmnd 18627  SubGrpcsubg 19018  CMndccmn 19678  Ringcrg 20137  SubRingcsubrg 20473  RingSpancrgspn 20514  Fieldcfield 20634  SubDRingcsdrg 20690  LModclmod 20782  LSpanclspn 20893  LBasisclbs 20997  subringAlg csra 21094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-reg 9503  ax-inf2 9556  ax-ac2 10376  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105  ax-pre-sup 11106  ax-addf 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-iin 4947  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-se 5577  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-of 7617  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 8632  df-map 8762  df-ixp 8832  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9271  df-sup 9351  df-oi 9421  df-r1 9679  df-rank 9680  df-card 9854  df-ac 10029  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-div 11797  df-nn 12148  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214  df-7 12215  df-8 12216  df-9 12217  df-n0 12404  df-xnn0 12477  df-z 12491  df-dec 12611  df-uz 12755  df-rp 12913  df-fz 13430  df-fzo 13577  df-seq 13928  df-exp 13988  df-hash 14257  df-word 14440  df-lsw 14489  df-concat 14497  df-s1 14522  df-substr 14567  df-pfx 14597  df-s2 14774  df-cj 15025  df-re 15026  df-im 15027  df-sqrt 15161  df-abs 15162  df-clim 15414  df-sum 15613  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17140  df-ress 17161  df-plusg 17193  df-mulr 17194  df-starv 17195  df-sca 17196  df-vsca 17197  df-ip 17198  df-tset 17199  df-ple 17200  df-ds 17202  df-unif 17203  df-hom 17204  df-cco 17205  df-0g 17364  df-gsum 17365  df-prds 17370  df-pws 17372  df-mre 17507  df-mrc 17508  df-acs 17510  df-mgm 18533  df-sgrp 18612  df-mnd 18628  df-mhm 18676  df-submnd 18677  df-grp 18834  df-minusg 18835  df-sbg 18836  df-mulg 18966  df-subg 19021  df-ghm 19111  df-cntz 19215  df-cmn 19680  df-abl 19681  df-mgp 20045  df-rng 20057  df-ur 20086  df-ring 20139  df-cring 20140  df-oppr 20241  df-nzr 20417  df-subrng 20450  df-subrg 20474  df-rgspn 20515  df-drng 20635  df-field 20636  df-sdrg 20691  df-lmod 20784  df-lss 20854  df-lsp 20894  df-lmhm 20945  df-lbs 20998  df-sra 21096  df-rgmod 21097  df-cnfld 21281  df-zring 21373  df-dsmm 21658  df-frlm 21673  df-uvc 21709  df-ind 32813

This theorem is referenced by:  fldextrspunlem1  33661