Theorem fldextrspunlsplem 33674

Description: Lemma for fldextrspunlsp 33675: First direction. 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)
fldextrspunlsplem.2	⊢ (𝜑 → 𝑃:𝐻⟶𝐺)
fldextrspunlsplem.3	⊢ (𝜑 → 𝑃 finSupp (0g‘𝐿))
fldextrspunlsplem.4	⊢ (𝜑 → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))))

Assertion

Ref	Expression
fldextrspunlsplem	⊢ (𝜑 → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))

Distinct variable groups:   𝐵,𝑎,𝑏,𝑓   𝐹,𝑎,𝑏,𝑓   𝐺,𝑎,𝑓   𝐻,𝑎,𝑏,𝑓   𝐽,𝑏   𝐾,𝑎,𝑏,𝑓   𝐿,𝑎,𝑏,𝑓   𝑃,𝑎,𝑏,𝑓   𝑋,𝑎   𝜑,𝑎,𝑏,𝑓

Allowed substitution hints:   𝐶(𝑓,𝑎,𝑏)   𝐸(𝑓,𝑎,𝑏)   𝐺(𝑏)   𝐼(𝑓,𝑎,𝑏)   𝐽(𝑓,𝑎)   𝑁(𝑓,𝑎,𝑏)   𝑋(𝑓,𝑏)

Proof of Theorem fldextrspunlsplem

Dummy variables 𝑐 𝑢 𝑒 ℎ 𝑦 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fldextrspunfld.5	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
2	1	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐺 ∈ (SubDRing‘𝐿))
3		fldextrspunlsp.1	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
4	3	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
5		eqid 2730	. . . . . 6 ⊢ (0g‘𝐿) = (0g‘𝐿)
6		fldextrspunfld.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ Field)
7	6	flddrngd 20656	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ DivRing)
8	7	drngringd 20652	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ Ring)
9	8	ringcmnd 20199	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ CMnd)
10	9	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐿 ∈ CMnd)
11		fldextrspunfld.6	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
12	11	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐻 ∈ (SubDRing‘𝐿))
13		sdrgsubrg 20706	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
14	1, 13	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
15		subrgsubg 20492	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐿) → 𝐺 ∈ (SubGrp‘𝐿))
16		subgsubm 19086	. . . . . . . 8 ⊢ (𝐺 ∈ (SubGrp‘𝐿) → 𝐺 ∈ (SubMnd‘𝐿))
17	14, 15, 16	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (SubMnd‘𝐿))
18	17	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐺 ∈ (SubMnd‘𝐿))
19		eqid 2730	. . . . . . . . 9 ⊢ (.r‘𝐿) = (.r‘𝐿)
20	14	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐺 ∈ (SubRing‘𝐿))
21		fldextrspunlsplem.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃:𝐻⟶𝐺)
22	21	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑃:𝐻⟶𝐺)
23		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ 𝐻)
24	22, 23	ffvelcdmd 7059	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑃‘𝑓) ∈ 𝐺)
25		fldextrspunfld.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
26		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐼) = (Base‘𝐼)
27	26	sdrgss 20708	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubDRing‘𝐼) → 𝐹 ⊆ (Base‘𝐼))
28	25, 27	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐼))
29		eqid 2730	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐿) = (Base‘𝐿)
30	29	sdrgss 20708	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
31	1, 30	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
32		fldextrspunfld.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (𝐿 ↾s 𝐺)
33	32, 29	ressbas2 17214	. . . . . . . . . . . . 13 ⊢ (𝐺 ⊆ (Base‘𝐿) → 𝐺 = (Base‘𝐼))
34	31, 33	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 = (Base‘𝐼))
35	28, 34	sseqtrrd 3986	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝐺)
36	35	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐹 ⊆ 𝐺)
37	3	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
38	25	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐹 ∈ (SubDRing‘𝐼))
39	11	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐻 ∈ (SubDRing‘𝐿))
40		ovexd 7424	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝐹 ↑m 𝐵) ∈ V)
41		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
42	39, 40, 41	elmaprd 32609	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
43	42, 23	ffvelcdmd 7059	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑢‘𝑓) ∈ (𝐹 ↑m 𝐵))
44	37, 38, 43	elmaprd 32609	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑢‘𝑓):𝐵⟶𝐹)
45		simplr 768	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑐 ∈ 𝐵)
46	44, 45	ffvelcdmd 7059	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑢‘𝑓)‘𝑐) ∈ 𝐹)
47	36, 46	sseldd 3949	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑢‘𝑓)‘𝑐) ∈ 𝐺)
48	19, 20, 24, 47	subrgmcld 33190	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) ∈ 𝐺)
49	48	fmpttd 7089	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))):𝐻⟶𝐺)
50	49	adantlr 715	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))):𝐻⟶𝐺)
51		fveq2 6860	. . . . . . . . 9 ⊢ (𝑓 = ℎ → (𝑃‘𝑓) = (𝑃‘ℎ))
52		fveq2 6860	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → (𝑢‘𝑓) = (𝑢‘ℎ))
53	52	fveq1d 6862	. . . . . . . . 9 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓)‘𝑐) = ((𝑢‘ℎ)‘𝑐))
54	51, 53	oveq12d 7407	. . . . . . . 8 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
55	54	cbvmptv 5213	. . . . . . 7 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
56		fvexd 6875	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (0g‘𝐿) ∈ V)
57		ssidd 3972	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐻 ⊆ 𝐻)
58		fldextrspunfld.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
59		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐽) = (Base‘𝐽)
60	59	sdrgss 20708	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
61	58, 60	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
62	29	sdrgss 20708	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
63	11, 62	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
64		fldextrspunfld.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = (𝐿 ↾s 𝐻)
65	64, 29	ressbas2 17214	. . . . . . . . . . . . 13 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
66	63, 65	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
67	61, 66	sseqtrrd 3986	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝐻)
68	67, 63	sstrd 3959	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
69	68	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐹 ⊆ (Base‘𝐿))
70	3	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
71	58	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐹 ∈ (SubDRing‘𝐽))
72		ovexd 7424	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐹 ↑m 𝐵) ∈ V)
73		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
74	12, 72, 73	elmaprd 32609	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
75	74	ffvelcdmda 7058	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
76	70, 71, 75	elmaprd 32609	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ):𝐵⟶𝐹)
77		simplr 768	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝑐 ∈ 𝐵)
78	76, 77	ffvelcdmd 7059	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
79	69, 78	sseldd 3949	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
80	21	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑃:𝐻⟶𝐺)
81		fldextrspunlsplem.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 finSupp (0g‘𝐿))
82	81	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑃 finSupp (0g‘𝐿))
83	8	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝐿 ∈ Ring)
84		simpr 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝑦 ∈ (Base‘𝐿))
85	29, 19, 5, 83, 84	ringlzd 20210	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → ((0g‘𝐿)(.r‘𝐿)𝑦) = (0g‘𝐿))
86	56, 56, 12, 57, 79, 80, 82, 85	fisuppov1 32612	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))) finSupp (0g‘𝐿))
87	55, 86	eqbrtrid 5144	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) finSupp (0g‘𝐿))
88	5, 10, 12, 18, 50, 87	gsumsubmcl 19855	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) ∈ 𝐺)
89	88	fmpttd 7089	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))):𝐵⟶𝐺)
90	2, 4, 89	elmapdd 8816	. . 3 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) ∈ (𝐺 ↑m 𝐵))
91		breq1 5112	. . . . . 6 ⊢ (𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) → (𝑎 finSupp (0g‘𝐿) ↔ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿)))
92	91	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑎 finSupp (0g‘𝐿) ↔ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿)))
93		simplr 768	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))))
94	93	fveq1d 6862	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → (𝑎‘𝑏) = ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏))
95		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))
96		fveq2 6860	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑏 → ((𝑢‘𝑓)‘𝑐) = ((𝑢‘𝑓)‘𝑏))
97	96	oveq2d 7405	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑏 → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) = ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))
98	97	mpteq2dv 5203	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑏 → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) = (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))
99	98	oveq2d 7405	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑏 → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
100		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
101		ovexd 7424	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))) ∈ V)
102	95, 99, 100, 101	fvmptd3 6993	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
103	102	adantlr 715	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
104	94, 103	eqtrd 2765	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → (𝑎‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
105	104	oveq1d 7404	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → ((𝑎‘𝑏)(.r‘𝐿)𝑏) = ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))
106	105	mpteq2dva 5202	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))
107	106	oveq2d 7405	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))
108	107	eqeq2d 2741	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏))) ↔ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))))
109	92, 108	anbi12d 632	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → ((𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))))
110	109	adantlr 715	. . 3 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → ((𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))))
111		fldextrspunlsp.2	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ Fin)
112	111	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ∈ Fin)
113		ovexd 7424	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) ∈ V)
114		fvexd 6875	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (0g‘𝐿) ∈ V)
115	95, 112, 113, 114	fsuppmptdm 9333	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿))
116		fldextrspunlsplem.4	. . . . . . 7 ⊢ (𝜑 → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))))
117	116	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))))
118	8	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐿 ∈ Ring)
119	118	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐿 ∈ Ring)
120	3	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
121	31	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐺 ⊆ (Base‘𝐿))
122	21	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑃:𝐻⟶𝐺)
123	122	ffvelcdmda 7058	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ 𝐺)
124	121, 123	sseldd 3949	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ (Base‘𝐿))
125	119	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐿 ∈ Ring)
126	68	ad4antr 732	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐹 ⊆ (Base‘𝐿))
127	3	ad4antr 732	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
128	58	ad4antr 732	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐹 ∈ (SubDRing‘𝐽))
129	11	ad4antr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐻 ∈ (SubDRing‘𝐿))
130		ovexd 7424	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝐹 ↑m 𝐵) ∈ V)
131		simp-4r 783	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
132	129, 130, 131	elmaprd 32609	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
133		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ℎ ∈ 𝐻)
134	132, 133	ffvelcdmd 7059	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
135	127, 128, 134	elmaprd 32609	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑢‘ℎ):𝐵⟶𝐹)
136		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵)
137	135, 136	ffvelcdmd 7059	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
138	126, 137	sseldd 3949	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
139		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
140		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
141	139, 140	lbsss 20990	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
142	3, 141	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
143		eqidd 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
144	143, 61	srabase 21090	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
145	66, 144	eqtr2d 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘((subringAlg ‘𝐽)‘𝐹)) = 𝐻)
146	142, 145	sseqtrd 3985	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ⊆ 𝐻)
147	146, 63	sstrd 3959	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝐿))
148	147	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ⊆ (Base‘𝐿))
149	148	sselda 3948	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ (Base‘𝐿))
150	29, 19, 125, 138, 149	ringcld 20175	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
151		fvexd 6875	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (0g‘𝐿) ∈ V)
152		ssidd 3972	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ⊆ 𝐵)
153	58	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐹 ∈ (SubDRing‘𝐽))
154	11	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐻 ∈ (SubDRing‘𝐿))
155		ovexd 7424	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐹 ↑m 𝐵) ∈ V)
156		simplr 768	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
157	154, 155, 156	elmaprd 32609	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
158	157	ffvelcdmda 7058	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
159	120, 153, 158	elmaprd 32609	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ):𝐵⟶𝐹)
160	52	breq1d 5119	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓) finSupp (0g‘𝐿) ↔ (𝑢‘ℎ) finSupp (0g‘𝐿)))
161		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → 𝑓 = ℎ)
162	52	fveq1d 6862	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓)‘𝑏) = ((𝑢‘ℎ)‘𝑏))
163	162	oveq1d 7404	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = ℎ → (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))
164	163	mpteq2dv 5203	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))
165	164	oveq2d 7405	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))
166	161, 165	eqeq12d 2746	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))) ↔ ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))))
167	160, 166	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ℎ → (((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑢‘ℎ) finSupp (0g‘𝐿) ∧ ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))))
168		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
169		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ ∈ 𝐻)
170	167, 168, 169	rspcdva 3592	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ) finSupp (0g‘𝐿) ∧ ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))))
171	170	simpld 494	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) finSupp (0g‘𝐿))
172	119	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝐿 ∈ Ring)
173		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝑦 ∈ (Base‘𝐿))
174	29, 19, 5, 172, 173	ringlzd 20210	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → ((0g‘𝐿)(.r‘𝐿)𝑦) = (0g‘𝐿))
175	151, 151, 120, 152, 149, 159, 171, 174	fisuppov1 32612	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)) finSupp (0g‘𝐿))
176	29, 5, 19, 119, 120, 124, 150, 175	gsummulc2 20232	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))) = ((𝑃‘ℎ)(.r‘𝐿)(𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
177	124	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑃‘ℎ) ∈ (Base‘𝐿))
178	29, 19, 125, 177, 138, 149	ringassd 20172	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))
179	178	mpteq2dva 5202	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)) = (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))))
180	179	oveq2d 7405	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
181	170	simprd 495	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))
182		fveq2 6860	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → ((𝑢‘ℎ)‘𝑏) = ((𝑢‘ℎ)‘𝑐))
183		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → 𝑏 = 𝑐)
184	182, 183	oveq12d 7407	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))
185	184	cbvmptv 5213	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)) = (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))
186	185	oveq2i 7400	. . . . . . . . . . . 12 ⊢ (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))
187	181, 186	eqtrdi 2781	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))))
188	187	oveq2d 7405	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)ℎ) = ((𝑃‘ℎ)(.r‘𝐿)(𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
189	176, 180, 188	3eqtr4rd 2776	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)ℎ) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))
190	189	mpteq2dva 5202	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ)) = (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)))))
191	190	oveq2d 7405	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
192	51, 161	oveq12d 7407	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)𝑓) = ((𝑃‘ℎ)(.r‘𝐿)ℎ))
193	192	cbvmptv 5213	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓)) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))
194	193	oveq2i 7400	. . . . . . . 8 ⊢ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ)))
195	194	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))))
196	9	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐿 ∈ CMnd)
197	8	ad4antr 732	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐿 ∈ Ring)
198	31	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐺 ⊆ (Base‘𝐿))
199	80	ffvelcdmda 7058	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ 𝐺)
200	198, 199	sseldd 3949	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ (Base‘𝐿))
201	29, 19, 197, 200, 79	ringcld 20175	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) ∈ (Base‘𝐿))
202	147	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ⊆ (Base‘𝐿))
203	202	sselda 3948	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ (Base‘𝐿))
204	203	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝑐 ∈ (Base‘𝐿))
205	29, 19, 197, 201, 204	ringcld 20175	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
206	205	anasss 466	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ (𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻)) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
207	81	fsuppimpd 9326	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 supp (0g‘𝐿)) ∈ Fin)
208	207	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑃 supp (0g‘𝐿)) ∈ Fin)
209		suppssdm 8158	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 supp (0g‘𝐿)) ⊆ dom 𝑃
210	209, 21	fssdm 6709	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 supp (0g‘𝐿)) ⊆ 𝐻)
211	210	sseld 3947	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑓 ∈ (𝑃 supp (0g‘𝐿)) → 𝑓 ∈ 𝐻))
212	211	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → (𝑓 ∈ (𝑃 supp (0g‘𝐿)) → 𝑓 ∈ 𝐻))
213		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ (𝑢‘𝑓) finSupp (0g‘𝐿)) → (𝑢‘𝑓) finSupp (0g‘𝐿))
214	213	fsuppimpd 9326	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ (𝑢‘𝑓) finSupp (0g‘𝐿)) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin)
215	214	ex 412	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → ((𝑢‘𝑓) finSupp (0g‘𝐿) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin))
216	215	adantrd 491	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → (((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin))
217	212, 216	imim12d 81	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → ((𝑓 ∈ 𝐻 → ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑓 ∈ (𝑃 supp (0g‘𝐿)) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin)))
218	217	ralimdv2 3143	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → (∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))) → ∀𝑓 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin))
219	218	imp 406	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∀𝑓 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin)
220		fveq2 6860	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑖 → (𝑢‘𝑓) = (𝑢‘𝑖))
221	220	oveq1d 7404	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑖 → ((𝑢‘𝑓) supp (0g‘𝐿)) = ((𝑢‘𝑖) supp (0g‘𝐿)))
222	221	eleq1d 2814	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑖 → (((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin ↔ ((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin))
223	222	cbvralvw 3216	. . . . . . . . . . . 12 ⊢ (∀𝑓 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin ↔ ∀𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
224	219, 223	sylib 218	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∀𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
225		iunfi 9300	. . . . . . . . . . 11 ⊢ (((𝑃 supp (0g‘𝐿)) ∈ Fin ∧ ∀𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
226	208, 224, 225	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
227		xpfi 9275	. . . . . . . . . 10 ⊢ ((∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin ∧ (𝑃 supp (0g‘𝐿)) ∈ Fin) → (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))) ∈ Fin)
228	226, 208, 227	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))) ∈ Fin)
229		snssi 4774	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (𝑃 supp (0g‘𝐿)) → {𝑖} ⊆ (𝑃 supp (0g‘𝐿)))
230	229	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑃 supp (0g‘𝐿))) → {𝑖} ⊆ (𝑃 supp (0g‘𝐿)))
231	230	iunxpssiun1 32503	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ⊆ (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))))
232	231	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ⊆ (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))))
233	228, 232	ssfid 9218	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ∈ Fin)
234	21	ffnd 6691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 Fn 𝐻)
235	234	ad6antr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑃 Fn 𝐻)
236	11	ad6antr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐻 ∈ (SubDRing‘𝐿))
237		fvexd 6875	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (0g‘𝐿) ∈ V)
238		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ℎ ∈ 𝐻)
239		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ¬ ℎ ∈ (𝑃 supp (0g‘𝐿)))
240	238, 239	eldifd 3927	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ℎ ∈ (𝐻 ∖ (𝑃 supp (0g‘𝐿))))
241	235, 236, 237, 240	fvdifsupp 8152	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑃‘ℎ) = (0g‘𝐿))
242	241	oveq1d 7404	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = ((0g‘𝐿)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
243	8	ad6antr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐿 ∈ Ring)
244	68	ad6antr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐹 ⊆ (Base‘𝐿))
245	3	ad6antr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
246	58	ad6antr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐹 ∈ (SubDRing‘𝐽))
247		ovexd 7424	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝐹 ↑m 𝐵) ∈ V)
248		simp-6r 787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
249	236, 247, 248	elmaprd 32609	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
250	249, 238	ffvelcdmd 7059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
251	245, 246, 250	elmaprd 32609	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑢‘ℎ):𝐵⟶𝐹)
252		simp-4r 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑐 ∈ 𝐵)
253	251, 252	ffvelcdmd 7059	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
254	244, 253	sseldd 3949	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
255	29, 19, 5, 243, 254	ringlzd 20210	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((0g‘𝐿)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
256	242, 255	eqtrd 2765	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
257	3	ad6antr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
258	58	ad6antr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐹 ∈ (SubDRing‘𝐽))
259	11	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐻 ∈ (SubDRing‘𝐿))
260		ovexd 7424	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝐹 ↑m 𝐵) ∈ V)
261		simp-6r 787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
262	259, 260, 261	elmaprd 32609	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
263		simpllr 775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ℎ ∈ 𝐻)
264	262, 263	ffvelcdmd 7059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
265	257, 258, 264	elmaprd 32609	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ):𝐵⟶𝐹)
266	265	ffnd 6691	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ) Fn 𝐵)
267		fvexd 6875	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (0g‘𝐿) ∈ V)
268		simp-4r 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑐 ∈ 𝐵)
269		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿)))
270	268, 269	eldifd 3927	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑐 ∈ (𝐵 ∖ ((𝑢‘ℎ) supp (0g‘𝐿))))
271	266, 257, 267, 270	fvdifsupp 8152	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) = (0g‘𝐿))
272	271	oveq2d 7405	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = ((𝑃‘ℎ)(.r‘𝐿)(0g‘𝐿)))
273	197	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐿 ∈ Ring)
274	200	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑃‘ℎ) ∈ (Base‘𝐿))
275	29, 19, 5, 273, 274	ringrzd 20211	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)(0g‘𝐿)) = (0g‘𝐿))
276	272, 275	eqtrd 2765	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
277		df-br 5110	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ ⟨𝑐, ℎ⟩ ∈ ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
278		fveq2 6860	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = 𝑖 → (𝑢‘ℎ) = (𝑢‘𝑖))
279	278	oveq1d 7404	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑖 → ((𝑢‘ℎ) supp (0g‘𝐿)) = ((𝑢‘𝑖) supp (0g‘𝐿)))
280		sneq 4601	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑖 → {ℎ} = {𝑖})
281	279, 280	xpeq12d 5671	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = 𝑖 → (((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) = (((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
282	281	cbviunv 5006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) = ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})
283	282	eleq2i 2821	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑐, ℎ⟩ ∈ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) ↔ ⟨𝑐, ℎ⟩ ∈ ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
284		opeliun2xp 5708	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑐, ℎ⟩ ∈ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) ↔ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
285	277, 283, 284	3bitr2i 299	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
286	285	notbii 320	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ ¬ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
287		ianor 983	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) ↔ (¬ ℎ ∈ (𝑃 supp (0g‘𝐿)) ∨ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
288	286, 287	sylbb 219	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ → (¬ ℎ ∈ (𝑃 supp (0g‘𝐿)) ∨ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
289	288	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (¬ ℎ ∈ (𝑃 supp (0g‘𝐿)) ∨ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
290	256, 276, 289	mpjaodan 960	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
291	290	oveq1d 7404	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = ((0g‘𝐿)(.r‘𝐿)𝑐))
292	118	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → 𝐿 ∈ Ring)
293	203	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → 𝑐 ∈ (Base‘𝐿))
294	29, 19, 5, 292, 293	ringlzd 20210	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → ((0g‘𝐿)(.r‘𝐿)𝑐) = (0g‘𝐿))
295	291, 294	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
296	295	an42ds 32385	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
297	296	an32s 652	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
298	297	anasss 466	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ (𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻)) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
299	298	an32s 652	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ (𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻)) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
300	299	anasss 466	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ((𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ)) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
301	29, 5, 196, 4, 154, 206, 233, 300	gsumcom3 19914	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
302	191, 195, 301	3eqtr4d 2775	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
303	118	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐿 ∈ Ring)
304	29, 5, 19, 303, 12, 203, 201, 86	gsummulc1 20231	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))) = ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
305	304	mpteq2dva 5202	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)))) = (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐)))
306	305	oveq2d 7405	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))))
307	117, 302, 306	3eqtrd 2769	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))))
308	51, 162	oveq12d 7407	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)))
309	308	cbvmptv 5213	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)))
310	182	oveq2d 7405	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
311	310	mpteq2dv 5203	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))
312	309, 311	eqtrid 2777	. . . . . . . . 9 ⊢ (𝑏 = 𝑐 → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))
313	312	oveq2d 7405	. . . . . . . 8 ⊢ (𝑏 = 𝑐 → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))))
314	313, 183	oveq12d 7407	. . . . . . 7 ⊢ (𝑏 = 𝑐 → ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏) = ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
315	314	cbvmptv 5213	. . . . . 6 ⊢ (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)) = (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
316	315	oveq2i 7400	. . . . 5 ⊢ (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐)))
317	307, 316	eqtr4di 2783	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))
318	115, 317	jca 511	. . 3 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))))
319	90, 110, 318	rspcedvd 3593	. 2 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))
320		breq1 5112	. . . 4 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑒 finSupp (0g‘𝐿) ↔ (𝑢‘𝑓) finSupp (0g‘𝐿)))
321		fveq1 6859	. . . . . . . 8 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑒‘𝑏) = ((𝑢‘𝑓)‘𝑏))
322	321	oveq1d 7404	. . . . . . 7 ⊢ (𝑒 = (𝑢‘𝑓) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))
323	322	mpteq2dv 5203	. . . . . 6 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))
324	323	oveq2d 7405	. . . . 5 ⊢ (𝑒 = (𝑢‘𝑓) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))
325	324	eqeq2d 2741	. . . 4 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))) ↔ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
326	320, 325	anbi12d 632	. . 3 ⊢ (𝑒 = (𝑢‘𝑓) → ((𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))))
327		ovexd 7424	. . 3 ⊢ (𝜑 → (𝐹 ↑m 𝐵) ∈ V)
328		eqid 2730	. . . . . . . . . 10 ⊢ (LSpan‘((subringAlg ‘𝐽)‘𝐹)) = (LSpan‘((subringAlg ‘𝐽)‘𝐹))
329	139, 140, 328	lbssp 20992	. . . . . . . . 9 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
330	3, 329	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
331	144, 66, 330	3eqtr4rd 2776	. . . . . . 7 ⊢ (𝜑 → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = 𝐻)
332	331	eleq2d 2815	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) ↔ 𝑓 ∈ 𝐻))
333		eqid 2730	. . . . . . 7 ⊢ (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹)))
334		eqid 2730	. . . . . . 7 ⊢ (Scalar‘((subringAlg ‘𝐽)‘𝐹)) = (Scalar‘((subringAlg ‘𝐽)‘𝐹))
335		eqid 2730	. . . . . . 7 ⊢ (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹)))
336		eqid 2730	. . . . . . 7 ⊢ ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))
337		sdrgsubrg 20706	. . . . . . . . 9 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ∈ (SubRing‘𝐽))
338	58, 337	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐽))
339		eqid 2730	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹)
340	339	sralmod 21100	. . . . . . . 8 ⊢ (𝐹 ∈ (SubRing‘𝐽) → ((subringAlg ‘𝐽)‘𝐹) ∈ LMod)
341	338, 340	syl 17	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ LMod)
342	328, 139, 333, 334, 335, 336, 341, 142	ellspds 33345	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) ↔ ∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))))
343	332, 342	bitr3d 281	. . . . 5 ⊢ (𝜑 → (𝑓 ∈ 𝐻 ↔ ∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))))
344	343	biimpa 476	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐻) → ∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))))
345		eqid 2730	. . . . . . . . . 10 ⊢ (𝐽 ↾s 𝐹) = (𝐽 ↾s 𝐹)
346	345, 59	ressbas2 17214	. . . . . . . . 9 ⊢ (𝐹 ⊆ (Base‘𝐽) → 𝐹 = (Base‘(𝐽 ↾s 𝐹)))
347	61, 346	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (Base‘(𝐽 ↾s 𝐹)))
348	143, 61	srasca 21093	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ↾s 𝐹) = (Scalar‘((subringAlg ‘𝐽)‘𝐹)))
349	348	fveq2d 6864	. . . . . . . 8 ⊢ (𝜑 → (Base‘(𝐽 ↾s 𝐹)) = (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))))
350	347, 349	eqtr2d 2766	. . . . . . 7 ⊢ (𝜑 → (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = 𝐹)
351	350	oveq1d 7404	. . . . . 6 ⊢ (𝜑 → ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵) = (𝐹 ↑m 𝐵))
352		sdrgsubrg 20706	. . . . . . . . . . . 12 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ∈ (SubRing‘𝐿))
353	11, 352	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ (SubRing‘𝐿))
354		subrgsubg 20492	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubRing‘𝐿) → 𝐻 ∈ (SubGrp‘𝐿))
355	64, 5	subg0 19070	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubGrp‘𝐿) → (0g‘𝐿) = (0g‘𝐽))
356	353, 354, 355	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝐿) = (0g‘𝐽))
357	64	sdrgdrng 20705	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐽 ∈ DivRing)
358	11, 357	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ DivRing)
359	358	drngringd 20652	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ Ring)
360	359	ringcmnd 20199	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ CMnd)
361	360	cmnmndd 19740	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ Mnd)
362		subrgsubg 20492	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubRing‘𝐽) → 𝐹 ∈ (SubGrp‘𝐽))
363		eqid 2730	. . . . . . . . . . . . 13 ⊢ (0g‘𝐽) = (0g‘𝐽)
364	363	subg0cl 19072	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubGrp‘𝐽) → (0g‘𝐽) ∈ 𝐹)
365	338, 362, 364	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝐽) ∈ 𝐹)
366	345, 59, 363	ress0g 18695	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Mnd ∧ (0g‘𝐽) ∈ 𝐹 ∧ 𝐹 ⊆ (Base‘𝐽)) → (0g‘𝐽) = (0g‘(𝐽 ↾s 𝐹)))
367	361, 365, 61, 366	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝐽) = (0g‘(𝐽 ↾s 𝐹)))
368	348	fveq2d 6864	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘(𝐽 ↾s 𝐹)) = (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))))
369	356, 367, 368	3eqtrrd 2770	. . . . . . . . 9 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (0g‘𝐿))
370	369	breq2d 5121	. . . . . . . 8 ⊢ (𝜑 → (𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↔ 𝑒 finSupp (0g‘𝐿)))
371	370	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↔ 𝑒 finSupp (0g‘𝐿)))
372	3	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
373		subgsubm 19086	. . . . . . . . . . . 12 ⊢ (𝐻 ∈ (SubGrp‘𝐿) → 𝐻 ∈ (SubMnd‘𝐿))
374	353, 354, 373	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ (SubMnd‘𝐿))
375	374	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐻 ∈ (SubMnd‘𝐿))
376	64, 19	ressmulr 17276	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → (.r‘𝐿) = (.r‘𝐽))
377	11, 376	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐿) = (.r‘𝐽))
378	143, 61	sravsca 21094	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐽) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
379	377, 378	eqtrd 2765	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
380	379	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
381	380	oveqd 7406	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) = ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))
382	353	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝐻 ∈ (SubRing‘𝐿))
383	67	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝐹 ⊆ 𝐻)
384	25	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐹 ∈ (SubDRing‘𝐼))
385	351	eleq2d 2815	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵) ↔ 𝑒 ∈ (𝐹 ↑m 𝐵)))
386	385	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝑒 ∈ (𝐹 ↑m 𝐵))
387	372, 384, 386	elmaprd 32609	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝑒:𝐵⟶𝐹)
388	387	ffvelcdmda 7058	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (𝑒‘𝑏) ∈ 𝐹)
389	383, 388	sseldd 3949	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (𝑒‘𝑏) ∈ 𝐻)
390	146	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐵 ⊆ 𝐻)
391	390	sselda 3948	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐻)
392	19, 382, 389, 391	subrgmcld 33190	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) ∈ 𝐻)
393	381, 392	eqeltrrd 2830	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏) ∈ 𝐻)
394	393	fmpttd 7089	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)):𝐵⟶𝐻)
395	372, 375, 394, 64	gsumsubm 18768	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
396	377, 378	eqtr2d 2766	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = (.r‘𝐿))
397	396	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = (.r‘𝐿))
398	397	oveqd 7406	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏) = ((𝑒‘𝑏)(.r‘𝐿)𝑏))
399	398	mpteq2dv 5203	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)) = (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))
400	399	oveq2d 7405	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))
401	3	mptexd 7200	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)) ∈ V)
402		fvexd 6875	. . . . . . . . . . 11 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ V)
403	339, 401, 358, 402, 61	gsumsra 32993	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
404	403	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
405	395, 400, 404	3eqtr3rd 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))
406	405	eqeq2d 2741	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) ↔ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))))
407	371, 406	anbi12d 632	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ((𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))) ↔ (𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))))
408	351, 407	rexeqbidva 3308	. . . . 5 ⊢ (𝜑 → (∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))) ↔ ∃𝑒 ∈ (𝐹 ↑m 𝐵)(𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))))
409	408	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐻) → (∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))) ↔ ∃𝑒 ∈ (𝐹 ↑m 𝐵)(𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))))
410	344, 409	mpbid 232	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐻) → ∃𝑒 ∈ (𝐹 ↑m 𝐵)(𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))))
411	326, 11, 327, 410	ac6mapd 32555	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
412	319, 411	r19.29a 3142	1 ⊢ (𝜑 → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054  Vcvv 3450   ∪ cun 3914   ⊆ wss 3916  {csn 4591  ⟨cop 4597  ∪ ciun 4957   class class class wbr 5109   ↦ cmpt 5190   × cxp 5638   Fn wfn 6508  ⟶wf 6509  ‘cfv 6513  (class class class)co 7389   supp csupp 8141   ↑_m cmap 8801  Fincfn 8920   finSupp cfsupp 9318  Basecbs 17185   ↾_s cress 17206  ._rcmulr 17227  Scalarcsca 17229   ·_𝑠 cvsca 17230  0_gc0g 17408   Σ_g cgsu 17409  Mndcmnd 18667  SubMndcsubmnd 18715  SubGrpcsubg 19058  CMndccmn 19716  Ringcrg 20148  SubRingcsubrg 20484  RingSpancrgspn 20525  DivRingcdr 20644  Fieldcfield 20645  SubDRingcsdrg 20701  LModclmod 20772  LSpanclspn 20883  LBasisclbs 20987  subringAlg csra 21084

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 2702  ax-rep 5236  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-reg 9551  ax-inf2 9600  ax-ac2 10422  ax-cnex 11130  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150  ax-pre-mulgt0 11151

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-pss 3936  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4874  df-int 4913  df-iun 4959  df-iin 4960  df-br 5110  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5535  df-eprel 5540  df-po 5548  df-so 5549  df-fr 5593  df-se 5594  df-we 5595  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-pred 6276  df-ord 6337  df-on 6338  df-lim 6339  df-suc 6340  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-isom 6522  df-riota 7346  df-ov 7392  df-oprab 7393  df-mpo 7394  df-of 7655  df-om 7845  df-1st 7970  df-2nd 7971  df-supp 8142  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8380  df-1o 8436  df-2o 8437  df-er 8673  df-map 8803  df-ixp 8873  df-en 8921  df-dom 8922  df-sdom 8923  df-fin 8924  df-fsupp 9319  df-sup 9399  df-oi 9469  df-r1 9723  df-rank 9724  df-card 9898  df-ac 10075  df-pnf 11216  df-mnf 11217  df-xr 11218  df-ltxr 11219  df-le 11220  df-sub 11413  df-neg 11414  df-nn 12188  df-2 12250  df-3 12251  df-4 12252  df-5 12253  df-6 12254  df-7 12255  df-8 12256  df-9 12257  df-n0 12449  df-z 12536  df-dec 12656  df-uz 12800  df-fz 13475  df-fzo 13622  df-seq 13973  df-hash 14302  df-struct 17123  df-sets 17140  df-slot 17158  df-ndx 17170  df-base 17186  df-ress 17207  df-plusg 17239  df-mulr 17240  df-sca 17242  df-vsca 17243  df-ip 17244  df-tset 17245  df-ple 17246  df-ds 17248  df-hom 17250  df-cco 17251  df-0g 17410  df-gsum 17411  df-prds 17416  df-pws 17418  df-mre 17553  df-mrc 17554  df-acs 17556  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-mhm 18716  df-submnd 18717  df-grp 18874  df-minusg 18875  df-sbg 18876  df-mulg 19006  df-subg 19061  df-ghm 19151  df-cntz 19255  df-cmn 19718  df-abl 19719  df-mgp 20056  df-rng 20068  df-ur 20097  df-ring 20150  df-nzr 20428  df-subrng 20461  df-subrg 20485  df-drng 20646  df-field 20647  df-sdrg 20702  df-lmod 20774  df-lss 20844  df-lsp 20884  df-lmhm 20935  df-lbs 20988  df-sra 21086  df-rgmod 21087  df-dsmm 21647  df-frlm 21662  df-uvc 21698

This theorem is referenced by:  fldextrspunlsp  33675