Theorem fldextrspunlsplem 34004

Description: Lemma for fldextrspunlsp 34005: 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 738	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐺 ∈ (SubDRing‘𝐿))
3		fldextrspunlsp.1	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
4	3	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
5		eqid 2769	. . . . . 6 ⊢ (0g‘𝐿) = (0g‘𝐿)
6		fldextrspunfld.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ Field)
7	6	flddrngd 20821	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ DivRing)
8	7	drngringd 20817	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ Ring)
9	8	ringcmnd 20363	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ CMnd)
10	9	ad3antrrr 742	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐿 ∈ CMnd)
11		fldextrspunfld.6	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
12	11	ad3antrrr 742	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐻 ∈ (SubDRing‘𝐿))
13		sdrgsubrg 20868	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
14	1, 13	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
15		subrgsubg 20658	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐿) → 𝐺 ∈ (SubGrp‘𝐿))
16		subgsubm 19211	. . . . . . . 8 ⊢ (𝐺 ∈ (SubGrp‘𝐿) → 𝐺 ∈ (SubMnd‘𝐿))
17	14, 15, 16	3syl 19	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (SubMnd‘𝐿))
18	17	ad3antrrr 742	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐺 ∈ (SubMnd‘𝐿))
19		eqid 2769	. . . . . . . . 9 ⊢ (.r‘𝐿) = (.r‘𝐿)
20	14	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐺 ∈ (SubRing‘𝐿))
21		fldextrspunlsplem.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃:𝐻⟶𝐺)
22	21	ad3antrrr 742	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑃:𝐻⟶𝐺)
23		simpr 489	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ 𝐻)
24	22, 23	ffvelcdmd 7078	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑃‘𝑓) ∈ 𝐺)
25		fldextrspunfld.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
26		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐼) = (Base‘𝐼)
27	26	sdrgss 20870	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubDRing‘𝐼) → 𝐹 ⊆ (Base‘𝐼))
28	25, 27	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐼))
29		eqid 2769	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐿) = (Base‘𝐿)
30	29	sdrgss 20870	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
31	1, 30	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
32		fldextrspunfld.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (𝐿 ↾s 𝐺)
33	32, 29	ressbas2 17294	. . . . . . . . . . . . 13 ⊢ (𝐺 ⊆ (Base‘𝐿) → 𝐺 = (Base‘𝐼))
34	31, 33	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 = (Base‘𝐼))
35	28, 34	sseqtrrd 3982	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝐺)
36	35	ad3antrrr 742	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐹 ⊆ 𝐺)
37	3	ad3antrrr 742	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
38	25	ad3antrrr 742	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐹 ∈ (SubDRing‘𝐼))
39	11	ad3antrrr 742	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐻 ∈ (SubDRing‘𝐿))
40		ovexd 7443	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝐹 ↑m 𝐵) ∈ V)
41		simpllr 787	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
42	39, 40, 41	elmaprd 32962	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
43	42, 23	ffvelcdmd 7078	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑢‘𝑓) ∈ (𝐹 ↑m 𝐵))
44	37, 38, 43	elmaprd 32962	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑢‘𝑓):𝐵⟶𝐹)
45		simplr 780	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑐 ∈ 𝐵)
46	44, 45	ffvelcdmd 7078	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑢‘𝑓)‘𝑐) ∈ 𝐹)
47	36, 46	sseldd 3946	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑢‘𝑓)‘𝑐) ∈ 𝐺)
48	19, 20, 24, 47	subrgmcld 33488	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) ∈ 𝐺)
49	48	fmpttd 7108	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))):𝐻⟶𝐺)
50	49	adantlr 727	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))):𝐻⟶𝐺)
51		fveq2 6879	. . . . . . . . 9 ⊢ (𝑓 = ℎ → (𝑃‘𝑓) = (𝑃‘ℎ))
52		fveq2 6879	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → (𝑢‘𝑓) = (𝑢‘ℎ))
53	52	fveq1d 6881	. . . . . . . . 9 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓)‘𝑐) = ((𝑢‘ℎ)‘𝑐))
54	51, 53	oveq12d 7426	. . . . . . . 8 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
55	54	cbvmptv 5216	. . . . . . 7 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
56		fvexd 6894	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (0g‘𝐿) ∈ V)
57		ssidd 3968	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐻 ⊆ 𝐻)
58		fldextrspunfld.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
59		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐽) = (Base‘𝐽)
60	59	sdrgss 20870	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
61	58, 60	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
62	29	sdrgss 20870	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
63	11, 62	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
64		fldextrspunfld.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = (𝐿 ↾s 𝐻)
65	64, 29	ressbas2 17294	. . . . . . . . . . . . 13 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
66	63, 65	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
67	61, 66	sseqtrrd 3982	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝐻)
68	67, 63	sstrd 3955	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
69	68	ad4antr 744	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐹 ⊆ (Base‘𝐿))
70	3	ad4antr 744	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
71	58	ad4antr 744	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐹 ∈ (SubDRing‘𝐽))
72		ovexd 7443	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐹 ↑m 𝐵) ∈ V)
73		simpllr 787	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
74	12, 72, 73	elmaprd 32962	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
75	74	ffvelcdmda 7077	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
76	70, 71, 75	elmaprd 32962	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ):𝐵⟶𝐹)
77		simplr 780	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝑐 ∈ 𝐵)
78	76, 77	ffvelcdmd 7078	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
79	69, 78	sseldd 3946	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
80	21	ad3antrrr 742	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑃:𝐻⟶𝐺)
81		fldextrspunlsplem.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 finSupp (0g‘𝐿))
82	81	ad3antrrr 742	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑃 finSupp (0g‘𝐿))
83	8	ad4antr 744	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝐿 ∈ Ring)
84		simpr 489	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝑦 ∈ (Base‘𝐿))
85	29, 19, 5, 83, 84	ringlzd 20374	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → ((0g‘𝐿)(.r‘𝐿)𝑦) = (0g‘𝐿))
86	56, 56, 12, 57, 79, 80, 82, 85	fisuppov1 32965	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))) finSupp (0g‘𝐿))
87	55, 86	eqbrtrid 5147	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) finSupp (0g‘𝐿))
88	5, 10, 12, 18, 50, 87	gsumsubmcl 19985	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) ∈ 𝐺)
89	88	fmpttd 7108	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))):𝐵⟶𝐺)
90	2, 4, 89	elmapdd 8834	. . 3 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) ∈ (𝐺 ↑m 𝐵))
91		breq1 5113	. . . . . 6 ⊢ (𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) → (𝑎 finSupp (0g‘𝐿) ↔ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿)))
92	91	adantl 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑎 finSupp (0g‘𝐿) ↔ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿)))
93		simplr 780	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))))
94	93	fveq1d 6881	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → (𝑎‘𝑏) = ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏))
95		eqid 2769	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))
96		fveq2 6879	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑏 → ((𝑢‘𝑓)‘𝑐) = ((𝑢‘𝑓)‘𝑏))
97	96	oveq2d 7424	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑏 → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) = ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))
98	97	mpteq2dv 5206	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑏 → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) = (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))
99	98	oveq2d 7424	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑏 → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
100		simpr 489	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
101		ovexd 7443	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))) ∈ V)
102	95, 99, 100, 101	fvmptd3 7011	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
103	102	adantlr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
104	94, 103	eqtrd 2804	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → (𝑎‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
105	104	oveq1d 7423	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → ((𝑎‘𝑏)(.r‘𝐿)𝑏) = ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))
106	105	mpteq2dva 5205	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))
107	106	oveq2d 7424	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))
108	107	eqeq2d 2780	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏))) ↔ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))))
109	92, 108	anbi12d 643	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → ((𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))))
110	109	adantlr 727	. . 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 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ∈ Fin)
113		ovexd 7443	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) ∈ V)
114		fvexd 6894	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (0g‘𝐿) ∈ V)
115	95, 112, 113, 114	fsuppmptdm 9332	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿))
116		fldextrspunlsplem.4	. . . . . . 7 ⊢ (𝜑 → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))))
117	116	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))))
118	8	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐿 ∈ Ring)
119	118	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐿 ∈ Ring)
120	3	ad3antrrr 742	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
121	31	ad3antrrr 742	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐺 ⊆ (Base‘𝐿))
122	21	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑃:𝐻⟶𝐺)
123	122	ffvelcdmda 7077	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ 𝐺)
124	121, 123	sseldd 3946	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ (Base‘𝐿))
125	119	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐿 ∈ Ring)
126	68	ad4antr 744	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐹 ⊆ (Base‘𝐿))
127	3	ad4antr 744	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
128	58	ad4antr 744	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐹 ∈ (SubDRing‘𝐽))
129	11	ad4antr 744	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐻 ∈ (SubDRing‘𝐿))
130		ovexd 7443	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝐹 ↑m 𝐵) ∈ V)
131		simp-4r 795	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
132	129, 130, 131	elmaprd 32962	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
133		simplr 780	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ℎ ∈ 𝐻)
134	132, 133	ffvelcdmd 7078	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
135	127, 128, 134	elmaprd 32962	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑢‘ℎ):𝐵⟶𝐹)
136		simpr 489	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵)
137	135, 136	ffvelcdmd 7078	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
138	126, 137	sseldd 3946	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
139		eqid 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
140		eqid 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
141	139, 140	lbsss 21172	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
142	3, 141	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
143		eqidd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
144	143, 61	srabase 21272	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
145	66, 144	eqtr2d 2805	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘((subringAlg ‘𝐽)‘𝐹)) = 𝐻)
146	142, 145	sseqtrd 3981	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ⊆ 𝐻)
147	146, 63	sstrd 3955	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝐿))
148	147	ad3antrrr 742	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ⊆ (Base‘𝐿))
149	148	sselda 3945	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ (Base‘𝐿))
150	29, 19, 125, 138, 149	ringcld 20338	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
151		fvexd 6894	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (0g‘𝐿) ∈ V)
152		ssidd 3968	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ⊆ 𝐵)
153	58	ad3antrrr 742	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐹 ∈ (SubDRing‘𝐽))
154	11	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐻 ∈ (SubDRing‘𝐿))
155		ovexd 7443	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐹 ↑m 𝐵) ∈ V)
156		simplr 780	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
157	154, 155, 156	elmaprd 32962	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
158	157	ffvelcdmda 7077	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
159	120, 153, 158	elmaprd 32962	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ):𝐵⟶𝐹)
160	52	breq1d 5120	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓) finSupp (0g‘𝐿) ↔ (𝑢‘ℎ) finSupp (0g‘𝐿)))
161		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → 𝑓 = ℎ)
162	52	fveq1d 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓)‘𝑏) = ((𝑢‘ℎ)‘𝑏))
163	162	oveq1d 7423	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = ℎ → (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))
164	163	mpteq2dv 5206	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))
165	164	oveq2d 7424	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))
166	161, 165	eqeq12d 2785	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))) ↔ ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))))
167	160, 166	anbi12d 643	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ℎ → (((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑢‘ℎ) finSupp (0g‘𝐿) ∧ ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))))
168		simplr 780	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
169		simpr 489	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ ∈ 𝐻)
170	167, 168, 169	rspcdva 3591	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ) finSupp (0g‘𝐿) ∧ ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))))
171	170	simpld 499	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) finSupp (0g‘𝐿))
172	119	adantr 485	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝐿 ∈ Ring)
173		simpr 489	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝑦 ∈ (Base‘𝐿))
174	29, 19, 5, 172, 173	ringlzd 20374	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → ((0g‘𝐿)(.r‘𝐿)𝑦) = (0g‘𝐿))
175	151, 151, 120, 152, 149, 159, 171, 174	fisuppov1 32965	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)) finSupp (0g‘𝐿))
176	29, 5, 19, 119, 120, 124, 150, 175	gsummulc2 20394	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))) = ((𝑃‘ℎ)(.r‘𝐿)(𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
177	124	adantr 485	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑃‘ℎ) ∈ (Base‘𝐿))
178	29, 19, 125, 177, 138, 149	ringassd 20335	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))
179	178	mpteq2dva 5205	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)) = (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))))
180	179	oveq2d 7424	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
181	170	simprd 500	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))
182		fveq2 6879	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → ((𝑢‘ℎ)‘𝑏) = ((𝑢‘ℎ)‘𝑐))
183		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → 𝑏 = 𝑐)
184	182, 183	oveq12d 7426	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))
185	184	cbvmptv 5216	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)) = (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))
186	185	oveq2i 7419	. . . . . . . . . . . 12 ⊢ (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))
187	181, 186	eqtrdi 2820	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))))
188	187	oveq2d 7424	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)ℎ) = ((𝑃‘ℎ)(.r‘𝐿)(𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
189	176, 180, 188	3eqtr4rd 2815	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)ℎ) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))
190	189	mpteq2dva 5205	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ)) = (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)))))
191	190	oveq2d 7424	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
192	51, 161	oveq12d 7426	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)𝑓) = ((𝑃‘ℎ)(.r‘𝐿)ℎ))
193	192	cbvmptv 5216	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓)) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))
194	193	oveq2i 7419	. . . . . . . 8 ⊢ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ)))
195	194	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))))
196	9	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐿 ∈ CMnd)
197	8	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐿 ∈ Ring)
198	31	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐺 ⊆ (Base‘𝐿))
199	80	ffvelcdmda 7077	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ 𝐺)
200	198, 199	sseldd 3946	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ (Base‘𝐿))
201	29, 19, 197, 200, 79	ringcld 20338	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) ∈ (Base‘𝐿))
202	147	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ⊆ (Base‘𝐿))
203	202	sselda 3945	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ (Base‘𝐿))
204	203	adantr 485	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝑐 ∈ (Base‘𝐿))
205	29, 19, 197, 201, 204	ringcld 20338	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
206	205	anasss 471	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ (𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻)) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
207	81	fsuppimpd 9325	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 supp (0g‘𝐿)) ∈ Fin)
208	207	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑃 supp (0g‘𝐿)) ∈ Fin)
209		suppssdm 8169	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 supp (0g‘𝐿)) ⊆ dom 𝑃
210	209, 21	fssdm 6723	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 supp (0g‘𝐿)) ⊆ 𝐻)
211	210	sseld 3944	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑓 ∈ (𝑃 supp (0g‘𝐿)) → 𝑓 ∈ 𝐻))
212	211	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → (𝑓 ∈ (𝑃 supp (0g‘𝐿)) → 𝑓 ∈ 𝐻))
213		simpr 489	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ (𝑢‘𝑓) finSupp (0g‘𝐿)) → (𝑢‘𝑓) finSupp (0g‘𝐿))
214	213	fsuppimpd 9325	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ (𝑢‘𝑓) finSupp (0g‘𝐿)) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin)
215	214	ex 417	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → ((𝑢‘𝑓) finSupp (0g‘𝐿) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin))
216	215	adantrd 496	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → (((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin))
217	212, 216	imim12d 82	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → ((𝑓 ∈ 𝐻 → ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑓 ∈ (𝑃 supp (0g‘𝐿)) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin)))
218	217	ralimdv2 3180	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → (∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))) → ∀𝑓 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin))
219	218	imp 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∀𝑓 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin)
220		fveq2 6879	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑖 → (𝑢‘𝑓) = (𝑢‘𝑖))
221	220	oveq1d 7423	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑖 → ((𝑢‘𝑓) supp (0g‘𝐿)) = ((𝑢‘𝑖) supp (0g‘𝐿)))
222	221	eleq1d 2854	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑖 → (((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin ↔ ((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin))
223	222	cbvralvw 3249	. . . . . . . . . . . 12 ⊢ (∀𝑓 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin ↔ ∀𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
224	219, 223	sylib 221	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∀𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
225		iunfi 9296	. . . . . . . . . . 11 ⊢ (((𝑃 supp (0g‘𝐿)) ∈ Fin ∧ ∀𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
226	208, 224, 225	syl2anc 595	. . . . . . . . . 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 595	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))) ∈ Fin)
229		snssi 4753	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (𝑃 supp (0g‘𝐿)) → {𝑖} ⊆ (𝑃 supp (0g‘𝐿)))
230	229	adantl 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑃 supp (0g‘𝐿))) → {𝑖} ⊆ (𝑃 supp (0g‘𝐿)))
231	230	iunxpssiun1 32850	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ⊆ (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))))
232	231	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ⊆ (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))))
233	228, 232	ssfid 9225	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ∈ Fin)
234	21	ffnd 6704	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 Fn 𝐻)
235	234	ad6antr 748	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑃 Fn 𝐻)
236	11	ad6antr 748	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐻 ∈ (SubDRing‘𝐿))
237		fvexd 6894	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (0g‘𝐿) ∈ V)
238		simpllr 787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ℎ ∈ 𝐻)
239		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ¬ ℎ ∈ (𝑃 supp (0g‘𝐿)))
240	238, 239	eldifd 3924	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ℎ ∈ (𝐻 ∖ (𝑃 supp (0g‘𝐿))))
241	235, 236, 237, 240	fvdifsupp 8163	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑃‘ℎ) = (0g‘𝐿))
242	241	oveq1d 7423	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = ((0g‘𝐿)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
243	8	ad6antr 748	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐿 ∈ Ring)
244	68	ad6antr 748	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐹 ⊆ (Base‘𝐿))
245	3	ad6antr 748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
246	58	ad6antr 748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐹 ∈ (SubDRing‘𝐽))
247		ovexd 7443	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝐹 ↑m 𝐵) ∈ V)
248		simp-6r 799	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
249	236, 247, 248	elmaprd 32962	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
250	249, 238	ffvelcdmd 7078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
251	245, 246, 250	elmaprd 32962	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑢‘ℎ):𝐵⟶𝐹)
252		simp-4r 795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑐 ∈ 𝐵)
253	251, 252	ffvelcdmd 7078	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
254	244, 253	sseldd 3946	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
255	29, 19, 5, 243, 254	ringlzd 20374	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((0g‘𝐿)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
256	242, 255	eqtrd 2804	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
257	3	ad6antr 748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
258	58	ad6antr 748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐹 ∈ (SubDRing‘𝐽))
259	11	ad6antr 748	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐻 ∈ (SubDRing‘𝐿))
260		ovexd 7443	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝐹 ↑m 𝐵) ∈ V)
261		simp-6r 799	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
262	259, 260, 261	elmaprd 32962	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
263		simpllr 787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ℎ ∈ 𝐻)
264	262, 263	ffvelcdmd 7078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
265	257, 258, 264	elmaprd 32962	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ):𝐵⟶𝐹)
266	265	ffnd 6704	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ) Fn 𝐵)
267		fvexd 6894	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (0g‘𝐿) ∈ V)
268		simp-4r 795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑐 ∈ 𝐵)
269		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿)))
270	268, 269	eldifd 3924	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑐 ∈ (𝐵 ∖ ((𝑢‘ℎ) supp (0g‘𝐿))))
271	266, 257, 267, 270	fvdifsupp 8163	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) = (0g‘𝐿))
272	271	oveq2d 7424	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = ((𝑃‘ℎ)(.r‘𝐿)(0g‘𝐿)))
273	197	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐿 ∈ Ring)
274	200	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑃‘ℎ) ∈ (Base‘𝐿))
275	29, 19, 5, 273, 274	ringrzd 20375	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)(0g‘𝐿)) = (0g‘𝐿))
276	272, 275	eqtrd 2804	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
277		df-br 5111	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ ⟨𝑐, ℎ⟩ ∈ ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
278		fveq2 6879	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = 𝑖 → (𝑢‘ℎ) = (𝑢‘𝑖))
279	278	oveq1d 7423	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑖 → ((𝑢‘ℎ) supp (0g‘𝐿)) = ((𝑢‘𝑖) supp (0g‘𝐿)))
280		sneq 4601	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑖 → {ℎ} = {𝑖})
281	279, 280	xpeq12d 5690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = 𝑖 → (((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) = (((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
282	281	cbviunv 5004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) = ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})
283	282	eleq2i 2861	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑐, ℎ⟩ ∈ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) ↔ ⟨𝑐, ℎ⟩ ∈ ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
284		opeliun2xp 5727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑐, ℎ⟩ ∈ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) ↔ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
285	277, 283, 284	3bitr2i 302	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
286	285	notbii 323	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ ¬ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
287		ianor 997	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) ↔ (¬ ℎ ∈ (𝑃 supp (0g‘𝐿)) ∨ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
288	286, 287	sylbb 222	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ → (¬ ℎ ∈ (𝑃 supp (0g‘𝐿)) ∨ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
289	288	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (¬ ℎ ∈ (𝑃 supp (0g‘𝐿)) ∨ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
290	256, 276, 289	mpjaodan 973	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
291	290	oveq1d 7423	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = ((0g‘𝐿)(.r‘𝐿)𝑐))
292	118	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → 𝐿 ∈ Ring)
293	203	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → 𝑐 ∈ (Base‘𝐿))
294	29, 19, 5, 292, 293	ringlzd 20374	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → ((0g‘𝐿)(.r‘𝐿)𝑐) = (0g‘𝐿))
295	291, 294	eqtrd 2804	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
296	295	an42ds 1517	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
297	296	an32s 664	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
298	297	anasss 471	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ (𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻)) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
299	298	an32s 664	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ (𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻)) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
300	299	anasss 471	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ((𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ)) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
301	29, 5, 196, 4, 154, 206, 233, 300	gsumcom3 20044	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
302	191, 195, 301	3eqtr4d 2814	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
303	118	adantr 485	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐿 ∈ Ring)
304	29, 5, 19, 303, 12, 203, 201, 86	gsummulc1 20393	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))) = ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
305	304	mpteq2dva 5205	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)))) = (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐)))
306	305	oveq2d 7424	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))))
307	117, 302, 306	3eqtrd 2808	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))))
308	51, 162	oveq12d 7426	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)))
309	308	cbvmptv 5216	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)))
310	182	oveq2d 7424	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
311	310	mpteq2dv 5206	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))
312	309, 311	eqtrid 2816	. . . . . . . . 9 ⊢ (𝑏 = 𝑐 → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))
313	312	oveq2d 7424	. . . . . . . 8 ⊢ (𝑏 = 𝑐 → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))))
314	313, 183	oveq12d 7426	. . . . . . 7 ⊢ (𝑏 = 𝑐 → ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏) = ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
315	314	cbvmptv 5216	. . . . . 6 ⊢ (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)) = (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
316	315	oveq2i 7419	. . . . 5 ⊢ (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐)))
317	307, 316	eqtr4di 2822	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))
318	115, 317	jca 520	. . 3 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))))
319	90, 110, 318	rspcedvd 3592	. 2 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))
320		breq1 5113	. . . 4 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑒 finSupp (0g‘𝐿) ↔ (𝑢‘𝑓) finSupp (0g‘𝐿)))
321		fveq1 6878	. . . . . . . 8 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑒‘𝑏) = ((𝑢‘𝑓)‘𝑏))
322	321	oveq1d 7423	. . . . . . 7 ⊢ (𝑒 = (𝑢‘𝑓) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))
323	322	mpteq2dv 5206	. . . . . 6 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))
324	323	oveq2d 7424	. . . . 5 ⊢ (𝑒 = (𝑢‘𝑓) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))
325	324	eqeq2d 2780	. . . 4 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))) ↔ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
326	320, 325	anbi12d 643	. . 3 ⊢ (𝑒 = (𝑢‘𝑓) → ((𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))))
327		ovexd 7443	. . 3 ⊢ (𝜑 → (𝐹 ↑m 𝐵) ∈ V)
328		eqid 2769	. . . . . . . . . 10 ⊢ (LSpan‘((subringAlg ‘𝐽)‘𝐹)) = (LSpan‘((subringAlg ‘𝐽)‘𝐹))
329	139, 140, 328	lbssp 21174	. . . . . . . . 9 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
330	3, 329	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
331	144, 66, 330	3eqtr4rd 2815	. . . . . . 7 ⊢ (𝜑 → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = 𝐻)
332	331	eleq2d 2855	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) ↔ 𝑓 ∈ 𝐻))
333		eqid 2769	. . . . . . 7 ⊢ (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹)))
334		eqid 2769	. . . . . . 7 ⊢ (Scalar‘((subringAlg ‘𝐽)‘𝐹)) = (Scalar‘((subringAlg ‘𝐽)‘𝐹))
335		eqid 2769	. . . . . . 7 ⊢ (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹)))
336		eqid 2769	. . . . . . 7 ⊢ ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))
337		sdrgsubrg 20868	. . . . . . . . 9 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ∈ (SubRing‘𝐽))
338	58, 337	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐽))
339		eqid 2769	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹)
340	339	sralmod 21282	. . . . . . . 8 ⊢ (𝐹 ∈ (SubRing‘𝐽) → ((subringAlg ‘𝐽)‘𝐹) ∈ LMod)
341	338, 340	syl 18	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ LMod)
342	328, 139, 333, 334, 335, 336, 341, 142	ellspds 33622	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) ↔ ∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))))
343	332, 342	bitr3d 284	. . . . 5 ⊢ (𝜑 → (𝑓 ∈ 𝐻 ↔ ∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))))
344	343	biimpa 481	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐻) → ∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))))
345		eqid 2769	. . . . . . . . . 10 ⊢ (𝐽 ↾s 𝐹) = (𝐽 ↾s 𝐹)
346	345, 59	ressbas2 17294	. . . . . . . . 9 ⊢ (𝐹 ⊆ (Base‘𝐽) → 𝐹 = (Base‘(𝐽 ↾s 𝐹)))
347	61, 346	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (Base‘(𝐽 ↾s 𝐹)))
348	143, 61	srasca 21275	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ↾s 𝐹) = (Scalar‘((subringAlg ‘𝐽)‘𝐹)))
349	348	fveq2d 6883	. . . . . . . 8 ⊢ (𝜑 → (Base‘(𝐽 ↾s 𝐹)) = (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))))
350	347, 349	eqtr2d 2805	. . . . . . 7 ⊢ (𝜑 → (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = 𝐹)
351	350	oveq1d 7423	. . . . . 6 ⊢ (𝜑 → ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵) = (𝐹 ↑m 𝐵))
352		sdrgsubrg 20868	. . . . . . . . . . . 12 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ∈ (SubRing‘𝐿))
353	11, 352	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ (SubRing‘𝐿))
354		subrgsubg 20658	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubRing‘𝐿) → 𝐻 ∈ (SubGrp‘𝐿))
355	64, 5	subg0 19194	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubGrp‘𝐿) → (0g‘𝐿) = (0g‘𝐽))
356	353, 354, 355	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝐿) = (0g‘𝐽))
357	64	sdrgdrng 20867	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐽 ∈ DivRing)
358	11, 357	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ DivRing)
359	358	drngringd 20817	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ Ring)
360	359	ringcmnd 20363	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ CMnd)
361	360	cmnmndd 19870	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ Mnd)
362		subrgsubg 20658	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubRing‘𝐽) → 𝐹 ∈ (SubGrp‘𝐽))
363		eqid 2769	. . . . . . . . . . . . 13 ⊢ (0g‘𝐽) = (0g‘𝐽)
364	363	subg0cl 19196	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubGrp‘𝐽) → (0g‘𝐽) ∈ 𝐹)
365	338, 362, 364	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝐽) ∈ 𝐹)
366	345, 59, 363	ress0g 18816	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Mnd ∧ (0g‘𝐽) ∈ 𝐹 ∧ 𝐹 ⊆ (Base‘𝐽)) → (0g‘𝐽) = (0g‘(𝐽 ↾s 𝐹)))
367	361, 365, 61, 366	syl3anc 1396	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝐽) = (0g‘(𝐽 ↾s 𝐹)))
368	348	fveq2d 6883	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘(𝐽 ↾s 𝐹)) = (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))))
369	356, 367, 368	3eqtrrd 2809	. . . . . . . . 9 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (0g‘𝐿))
370	369	breq2d 5122	. . . . . . . 8 ⊢ (𝜑 → (𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↔ 𝑒 finSupp (0g‘𝐿)))
371	370	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↔ 𝑒 finSupp (0g‘𝐿)))
372	3	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
373		subgsubm 19211	. . . . . . . . . . . 12 ⊢ (𝐻 ∈ (SubGrp‘𝐿) → 𝐻 ∈ (SubMnd‘𝐿))
374	353, 354, 373	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ (SubMnd‘𝐿))
375	374	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐻 ∈ (SubMnd‘𝐿))
376	64, 19	ressmulr 17356	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → (.r‘𝐿) = (.r‘𝐽))
377	11, 376	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐿) = (.r‘𝐽))
378	143, 61	sravsca 21276	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐽) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
379	377, 378	eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
380	379	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
381	380	oveqd 7425	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) = ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))
382	353	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝐻 ∈ (SubRing‘𝐿))
383	67	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝐹 ⊆ 𝐻)
384	25	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐹 ∈ (SubDRing‘𝐼))
385	351	eleq2d 2855	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵) ↔ 𝑒 ∈ (𝐹 ↑m 𝐵)))
386	385	biimpa 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝑒 ∈ (𝐹 ↑m 𝐵))
387	372, 384, 386	elmaprd 32962	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝑒:𝐵⟶𝐹)
388	387	ffvelcdmda 7077	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (𝑒‘𝑏) ∈ 𝐹)
389	383, 388	sseldd 3946	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (𝑒‘𝑏) ∈ 𝐻)
390	146	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐵 ⊆ 𝐻)
391	390	sselda 3945	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐻)
392	19, 382, 389, 391	subrgmcld 33488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) ∈ 𝐻)
393	381, 392	eqeltrrd 2870	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏) ∈ 𝐻)
394	393	fmpttd 7108	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)):𝐵⟶𝐻)
395	372, 375, 394, 64	gsumsubm 18890	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
396	377, 378	eqtr2d 2805	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = (.r‘𝐿))
397	396	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = (.r‘𝐿))
398	397	oveqd 7425	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏) = ((𝑒‘𝑏)(.r‘𝐿)𝑏))
399	398	mpteq2dv 5206	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)) = (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))
400	399	oveq2d 7424	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))
401	3	mptexd 7220	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)) ∈ V)
402		fvexd 6894	. . . . . . . . . . 11 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ V)
403	339, 401, 358, 402, 61	gsumsra 33304	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
404	403	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
405	395, 400, 404	3eqtr3rd 2813	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))
406	405	eqeq2d 2780	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) ↔ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))))
407	371, 406	anbi12d 643	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ((𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))) ↔ (𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))))
408	351, 407	rexeqbidva 3336	. . . . 5 ⊢ (𝜑 → (∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))) ↔ ∃𝑒 ∈ (𝐹 ↑m 𝐵)(𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))))
409	408	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐻) → (∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))) ↔ ∃𝑒 ∈ (𝐹 ↑m 𝐵)(𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))))
410	344, 409	mpbid 235	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐻) → ∃𝑒 ∈ (𝐹 ↑m 𝐵)(𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))))
411	326, 11, 327, 410	ac6mapd 32905	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
412	319, 411	r19.29a 3179	1 ⊢ (𝜑 → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  Vcvv 3463   ∪ cun 3911   ⊆ wss 3913  {csn 4591  ⟨cop 4597  ∪ ciun 4957   class class class wbr 5110   ↦ cmpt 5193   × cxp 5657   Fn wfn 6529  ⟶wf 6530  ‘cfv 6534  (class class class)co 7408   supp csupp 8152   ↑_m cmap 8820  Fincfn 8939   finSupp cfsupp 9317  Basecbs 17265   ↾_s cress 17286  ._rcmulr 17307  Scalarcsca 17309   ·_𝑠 cvsca 17310  0_gc0g 17488   Σ_g cgsu 17489  Mndcmnd 18788  SubMndcsubmnd 18836  SubGrpcsubg 19182  CMndccmn 19846  Ringcrg 20311  SubRingcsubrg 20650  RingSpancrgspn 20691  DivRingcdr 20809  Fieldcfield 20810  SubDRingcsdrg 20863  LModclmod 20955  LSpanclspn 21066  LBasisclbs 21169  subringAlg csra 21266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5239  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-reg 9550  ax-inf2 9606  ax-ac2 10443  ax-cnex 11152  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4874  df-int 4914  df-iun 4959  df-iin 4960  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6300  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-isom 6543  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-of 7672  df-om 7859  df-1st 7982  df-2nd 7983  df-supp 8153  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-2o 8450  df-er 8690  df-map 8822  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9318  df-sup 9398  df-oi 9468  df-r1 9732  df-rank 9733  df-card 9921  df-ac 10096  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440  df-nn 12230  df-2 12299  df-3 12300  df-4 12301  df-5 12302  df-6 12303  df-7 12304  df-8 12305  df-9 12306  df-n0 12501  df-z 12588  df-dec 12708  df-uz 12859  df-fz 13532  df-fzo 13679  df-seq 14034  df-hash 14363  df-struct 17203  df-sets 17220  df-slot 17238  df-ndx 17250  df-base 17266  df-ress 17287  df-plusg 17319  df-mulr 17320  df-sca 17322  df-vsca 17323  df-ip 17324  df-tset 17325  df-ple 17326  df-ds 17328  df-hom 17330  df-cco 17331  df-0g 17490  df-gsum 17491  df-prds 17496  df-pws 17498  df-mre 17634  df-mrc 17635  df-acs 17637  df-mgm 18694  df-sgrp 18773  df-mnd 18789  df-mhm 18837  df-submnd 18838  df-grp 18999  df-minusg 19000  df-sbg 19001  df-mulg 19130  df-subg 19185  df-ghm 19280  df-cntz 19383  df-cmn 19848  df-abl 19849  df-mgp 20213  df-rng 20227  df-ur 20260  df-ring 20313  df-nzr 20592  df-subrng 20627  df-subrg 20651  df-drng 20811  df-field 20812  df-sdrg 20864  df-lmod 20957  df-lss 21027  df-lsp 21067  df-lmhm 21117  df-lbs 21170  df-sra 21268  df-rgmod 21269  df-dsmm 21847  df-frlm 21862  df-uvc 21898

This theorem is referenced by:  fldextrspunlsp  34005