Theorem fldextrspunlsplem 33931

Description: Lemma for fldextrspunlsp 33932: 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 736	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐺 ∈ (SubDRing‘𝐿))
3		fldextrspunlsp.1	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
4	3	ad2antrr 736	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
5		eqid 2761	. . . . . 6 ⊢ (0g‘𝐿) = (0g‘𝐿)
6		fldextrspunfld.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ Field)
7	6	flddrngd 20778	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ DivRing)
8	7	drngringd 20774	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ Ring)
9	8	ringcmnd 20321	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ CMnd)
10	9	ad3antrrr 740	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐿 ∈ CMnd)
11		fldextrspunfld.6	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
12	11	ad3antrrr 740	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐻 ∈ (SubDRing‘𝐿))
13		sdrgsubrg 20828	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
14	1, 13	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
15		subrgsubg 20614	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐿) → 𝐺 ∈ (SubGrp‘𝐿))
16		subgsubm 19181	. . . . . . . 8 ⊢ (𝐺 ∈ (SubGrp‘𝐿) → 𝐺 ∈ (SubMnd‘𝐿))
17	14, 15, 16	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (SubMnd‘𝐿))
18	17	ad3antrrr 740	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐺 ∈ (SubMnd‘𝐿))
19		eqid 2761	. . . . . . . . 9 ⊢ (.r‘𝐿) = (.r‘𝐿)
20	14	ad3antrrr 740	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐺 ∈ (SubRing‘𝐿))
21		fldextrspunlsplem.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃:𝐻⟶𝐺)
22	21	ad3antrrr 740	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑃:𝐻⟶𝐺)
23		simpr 488	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ 𝐻)
24	22, 23	ffvelcdmd 7061	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑃‘𝑓) ∈ 𝐺)
25		fldextrspunfld.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
26		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐼) = (Base‘𝐼)
27	26	sdrgss 20830	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubDRing‘𝐼) → 𝐹 ⊆ (Base‘𝐼))
28	25, 27	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐼))
29		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐿) = (Base‘𝐿)
30	29	sdrgss 20830	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
31	1, 30	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
32		fldextrspunfld.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (𝐿 ↾s 𝐺)
33	32, 29	ressbas2 17265	. . . . . . . . . . . . 13 ⊢ (𝐺 ⊆ (Base‘𝐿) → 𝐺 = (Base‘𝐼))
34	31, 33	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 = (Base‘𝐼))
35	28, 34	sseqtrrd 3971	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝐺)
36	35	ad3antrrr 740	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐹 ⊆ 𝐺)
37	3	ad3antrrr 740	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
38	25	ad3antrrr 740	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐹 ∈ (SubDRing‘𝐼))
39	11	ad3antrrr 740	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐻 ∈ (SubDRing‘𝐿))
40		ovexd 7426	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝐹 ↑m 𝐵) ∈ V)
41		simpllr 785	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
42	39, 40, 41	elmaprd 32843	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
43	42, 23	ffvelcdmd 7061	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑢‘𝑓) ∈ (𝐹 ↑m 𝐵))
44	37, 38, 43	elmaprd 32843	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑢‘𝑓):𝐵⟶𝐹)
45		simplr 778	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑐 ∈ 𝐵)
46	44, 45	ffvelcdmd 7061	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑢‘𝑓)‘𝑐) ∈ 𝐹)
47	36, 46	sseldd 3935	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑢‘𝑓)‘𝑐) ∈ 𝐺)
48	19, 20, 24, 47	subrgmcld 33373	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) ∈ 𝐺)
49	48	fmpttd 7091	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))):𝐻⟶𝐺)
50	49	adantlr 725	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))):𝐻⟶𝐺)
51		fveq2 6862	. . . . . . . . 9 ⊢ (𝑓 = ℎ → (𝑃‘𝑓) = (𝑃‘ℎ))
52		fveq2 6862	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → (𝑢‘𝑓) = (𝑢‘ℎ))
53	52	fveq1d 6864	. . . . . . . . 9 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓)‘𝑐) = ((𝑢‘ℎ)‘𝑐))
54	51, 53	oveq12d 7409	. . . . . . . 8 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
55	54	cbvmptv 5201	. . . . . . 7 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
56		fvexd 6877	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (0g‘𝐿) ∈ V)
57		ssidd 3957	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐻 ⊆ 𝐻)
58		fldextrspunfld.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
59		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐽) = (Base‘𝐽)
60	59	sdrgss 20830	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
61	58, 60	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
62	29	sdrgss 20830	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
63	11, 62	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
64		fldextrspunfld.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = (𝐿 ↾s 𝐻)
65	64, 29	ressbas2 17265	. . . . . . . . . . . . 13 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
66	63, 65	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
67	61, 66	sseqtrrd 3971	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝐻)
68	67, 63	sstrd 3944	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
69	68	ad4antr 742	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐹 ⊆ (Base‘𝐿))
70	3	ad4antr 742	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
71	58	ad4antr 742	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐹 ∈ (SubDRing‘𝐽))
72		ovexd 7426	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐹 ↑m 𝐵) ∈ V)
73		simpllr 785	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
74	12, 72, 73	elmaprd 32843	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
75	74	ffvelcdmda 7060	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
76	70, 71, 75	elmaprd 32843	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ):𝐵⟶𝐹)
77		simplr 778	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝑐 ∈ 𝐵)
78	76, 77	ffvelcdmd 7061	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
79	69, 78	sseldd 3935	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
80	21	ad3antrrr 740	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑃:𝐻⟶𝐺)
81		fldextrspunlsplem.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 finSupp (0g‘𝐿))
82	81	ad3antrrr 740	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑃 finSupp (0g‘𝐿))
83	8	ad4antr 742	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝐿 ∈ Ring)
84		simpr 488	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝑦 ∈ (Base‘𝐿))
85	29, 19, 5, 83, 84	ringlzd 20332	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → ((0g‘𝐿)(.r‘𝐿)𝑦) = (0g‘𝐿))
86	56, 56, 12, 57, 79, 80, 82, 85	fisuppov1 32846	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))) finSupp (0g‘𝐿))
87	55, 86	eqbrtrid 5132	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) finSupp (0g‘𝐿))
88	5, 10, 12, 18, 50, 87	gsumsubmcl 19950	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) ∈ 𝐺)
89	88	fmpttd 7091	. . . 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 5100	. . . . . 6 ⊢ (𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) → (𝑎 finSupp (0g‘𝐿) ↔ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿)))
92	91	adantl 485	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑎 finSupp (0g‘𝐿) ↔ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿)))
93		simplr 778	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))))
94	93	fveq1d 6864	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → (𝑎‘𝑏) = ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏))
95		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))
96		fveq2 6862	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑏 → ((𝑢‘𝑓)‘𝑐) = ((𝑢‘𝑓)‘𝑏))
97	96	oveq2d 7407	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑏 → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) = ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))
98	97	mpteq2dv 5191	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑏 → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) = (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))
99	98	oveq2d 7407	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑏 → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
100		simpr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
101		ovexd 7426	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))) ∈ V)
102	95, 99, 100, 101	fvmptd3 6994	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
103	102	adantlr 725	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
104	94, 103	eqtrd 2796	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → (𝑎‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
105	104	oveq1d 7406	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → ((𝑎‘𝑏)(.r‘𝐿)𝑏) = ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))
106	105	mpteq2dva 5190	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))
107	106	oveq2d 7407	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))
108	107	eqeq2d 2772	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏))) ↔ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))))
109	92, 108	anbi12d 641	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → ((𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))))
110	109	adantlr 725	. . 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 736	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ∈ Fin)
113		ovexd 7426	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) ∈ V)
114		fvexd 6877	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (0g‘𝐿) ∈ V)
115	95, 112, 113, 114	fsuppmptdm 9316	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿))
116		fldextrspunlsplem.4	. . . . . . 7 ⊢ (𝜑 → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))))
117	116	ad2antrr 736	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))))
118	8	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐿 ∈ Ring)
119	118	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐿 ∈ Ring)
120	3	ad3antrrr 740	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
121	31	ad3antrrr 740	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐺 ⊆ (Base‘𝐿))
122	21	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑃:𝐻⟶𝐺)
123	122	ffvelcdmda 7060	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ 𝐺)
124	121, 123	sseldd 3935	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ (Base‘𝐿))
125	119	adantr 484	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐿 ∈ Ring)
126	68	ad4antr 742	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐹 ⊆ (Base‘𝐿))
127	3	ad4antr 742	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
128	58	ad4antr 742	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐹 ∈ (SubDRing‘𝐽))
129	11	ad4antr 742	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐻 ∈ (SubDRing‘𝐿))
130		ovexd 7426	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝐹 ↑m 𝐵) ∈ V)
131		simp-4r 793	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
132	129, 130, 131	elmaprd 32843	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
133		simplr 778	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ℎ ∈ 𝐻)
134	132, 133	ffvelcdmd 7061	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
135	127, 128, 134	elmaprd 32843	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑢‘ℎ):𝐵⟶𝐹)
136		simpr 488	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵)
137	135, 136	ffvelcdmd 7061	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
138	126, 137	sseldd 3935	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
139		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
140		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
141	139, 140	lbsss 21132	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
142	3, 141	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
143		eqidd 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
144	143, 61	srabase 21232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
145	66, 144	eqtr2d 2797	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘((subringAlg ‘𝐽)‘𝐹)) = 𝐻)
146	142, 145	sseqtrd 3970	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ⊆ 𝐻)
147	146, 63	sstrd 3944	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝐿))
148	147	ad3antrrr 740	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ⊆ (Base‘𝐿))
149	148	sselda 3934	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ (Base‘𝐿))
150	29, 19, 125, 138, 149	ringcld 20297	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
151		fvexd 6877	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (0g‘𝐿) ∈ V)
152		ssidd 3957	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ⊆ 𝐵)
153	58	ad3antrrr 740	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐹 ∈ (SubDRing‘𝐽))
154	11	ad2antrr 736	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐻 ∈ (SubDRing‘𝐿))
155		ovexd 7426	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐹 ↑m 𝐵) ∈ V)
156		simplr 778	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
157	154, 155, 156	elmaprd 32843	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
158	157	ffvelcdmda 7060	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
159	120, 153, 158	elmaprd 32843	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ):𝐵⟶𝐹)
160	52	breq1d 5107	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓) finSupp (0g‘𝐿) ↔ (𝑢‘ℎ) finSupp (0g‘𝐿)))
161		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → 𝑓 = ℎ)
162	52	fveq1d 6864	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓)‘𝑏) = ((𝑢‘ℎ)‘𝑏))
163	162	oveq1d 7406	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = ℎ → (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))
164	163	mpteq2dv 5191	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))
165	164	oveq2d 7407	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))
166	161, 165	eqeq12d 2777	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))) ↔ ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))))
167	160, 166	anbi12d 641	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ℎ → (((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑢‘ℎ) finSupp (0g‘𝐿) ∧ ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))))
168		simplr 778	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
169		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ ∈ 𝐻)
170	167, 168, 169	rspcdva 3581	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ) finSupp (0g‘𝐿) ∧ ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))))
171	170	simpld 498	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) finSupp (0g‘𝐿))
172	119	adantr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝐿 ∈ Ring)
173		simpr 488	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝑦 ∈ (Base‘𝐿))
174	29, 19, 5, 172, 173	ringlzd 20332	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → ((0g‘𝐿)(.r‘𝐿)𝑦) = (0g‘𝐿))
175	151, 151, 120, 152, 149, 159, 171, 174	fisuppov1 32846	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)) finSupp (0g‘𝐿))
176	29, 5, 19, 119, 120, 124, 150, 175	gsummulc2 20352	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))) = ((𝑃‘ℎ)(.r‘𝐿)(𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
177	124	adantr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑃‘ℎ) ∈ (Base‘𝐿))
178	29, 19, 125, 177, 138, 149	ringassd 20294	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))
179	178	mpteq2dva 5190	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)) = (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))))
180	179	oveq2d 7407	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
181	170	simprd 499	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))
182		fveq2 6862	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → ((𝑢‘ℎ)‘𝑏) = ((𝑢‘ℎ)‘𝑐))
183		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → 𝑏 = 𝑐)
184	182, 183	oveq12d 7409	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))
185	184	cbvmptv 5201	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)) = (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))
186	185	oveq2i 7402	. . . . . . . . . . . 12 ⊢ (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))
187	181, 186	eqtrdi 2812	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))))
188	187	oveq2d 7407	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)ℎ) = ((𝑃‘ℎ)(.r‘𝐿)(𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
189	176, 180, 188	3eqtr4rd 2807	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)ℎ) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))
190	189	mpteq2dva 5190	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ)) = (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)))))
191	190	oveq2d 7407	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
192	51, 161	oveq12d 7409	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)𝑓) = ((𝑃‘ℎ)(.r‘𝐿)ℎ))
193	192	cbvmptv 5201	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓)) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))
194	193	oveq2i 7402	. . . . . . . 8 ⊢ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ)))
195	194	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))))
196	9	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐿 ∈ CMnd)
197	8	ad4antr 742	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐿 ∈ Ring)
198	31	ad4antr 742	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐺 ⊆ (Base‘𝐿))
199	80	ffvelcdmda 7060	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ 𝐺)
200	198, 199	sseldd 3935	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ (Base‘𝐿))
201	29, 19, 197, 200, 79	ringcld 20297	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) ∈ (Base‘𝐿))
202	147	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ⊆ (Base‘𝐿))
203	202	sselda 3934	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ (Base‘𝐿))
204	203	adantr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝑐 ∈ (Base‘𝐿))
205	29, 19, 197, 201, 204	ringcld 20297	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
206	205	anasss 470	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ (𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻)) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
207	81	fsuppimpd 9309	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 supp (0g‘𝐿)) ∈ Fin)
208	207	ad2antrr 736	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑃 supp (0g‘𝐿)) ∈ Fin)
209		suppssdm 8151	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 supp (0g‘𝐿)) ⊆ dom 𝑃
210	209, 21	fssdm 6706	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 supp (0g‘𝐿)) ⊆ 𝐻)
211	210	sseld 3933	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑓 ∈ (𝑃 supp (0g‘𝐿)) → 𝑓 ∈ 𝐻))
212	211	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → (𝑓 ∈ (𝑃 supp (0g‘𝐿)) → 𝑓 ∈ 𝐻))
213		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ (𝑢‘𝑓) finSupp (0g‘𝐿)) → (𝑢‘𝑓) finSupp (0g‘𝐿))
214	213	fsuppimpd 9309	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ (𝑢‘𝑓) finSupp (0g‘𝐿)) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin)
215	214	ex 416	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → ((𝑢‘𝑓) finSupp (0g‘𝐿) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin))
216	215	adantrd 495	. . . . . . . . . . . . . . 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 3170	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → (∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))) → ∀𝑓 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin))
219	218	imp 410	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∀𝑓 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin)
220		fveq2 6862	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑖 → (𝑢‘𝑓) = (𝑢‘𝑖))
221	220	oveq1d 7406	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑖 → ((𝑢‘𝑓) supp (0g‘𝐿)) = ((𝑢‘𝑖) supp (0g‘𝐿)))
222	221	eleq1d 2846	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑖 → (((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin ↔ ((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin))
223	222	cbvralvw 3239	. . . . . . . . . . . 12 ⊢ (∀𝑓 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin ↔ ∀𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
224	219, 223	sylib 220	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∀𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
225		iunfi 9280	. . . . . . . . . . 11 ⊢ (((𝑃 supp (0g‘𝐿)) ∈ Fin ∧ ∀𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
226	208, 224, 225	syl2anc 593	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
227		xpfi 9258	. . . . . . . . . 10 ⊢ ((∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin ∧ (𝑃 supp (0g‘𝐿)) ∈ Fin) → (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))) ∈ Fin)
228	226, 208, 227	syl2anc 593	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))) ∈ Fin)
229		snssi 4741	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (𝑃 supp (0g‘𝐿)) → {𝑖} ⊆ (𝑃 supp (0g‘𝐿)))
230	229	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑃 supp (0g‘𝐿))) → {𝑖} ⊆ (𝑃 supp (0g‘𝐿)))
231	230	iunxpssiun1 32728	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ⊆ (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))))
232	231	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ⊆ (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))))
233	228, 232	ssfid 9207	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ∈ Fin)
234	21	ffnd 6687	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 Fn 𝐻)
235	234	ad6antr 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑃 Fn 𝐻)
236	11	ad6antr 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐻 ∈ (SubDRing‘𝐿))
237		fvexd 6877	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (0g‘𝐿) ∈ V)
238		simpllr 785	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ℎ ∈ 𝐻)
239		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ¬ ℎ ∈ (𝑃 supp (0g‘𝐿)))
240	238, 239	eldifd 3913	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ℎ ∈ (𝐻 ∖ (𝑃 supp (0g‘𝐿))))
241	235, 236, 237, 240	fvdifsupp 8145	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑃‘ℎ) = (0g‘𝐿))
242	241	oveq1d 7406	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = ((0g‘𝐿)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
243	8	ad6antr 746	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐿 ∈ Ring)
244	68	ad6antr 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐹 ⊆ (Base‘𝐿))
245	3	ad6antr 746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
246	58	ad6antr 746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐹 ∈ (SubDRing‘𝐽))
247		ovexd 7426	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝐹 ↑m 𝐵) ∈ V)
248		simp-6r 797	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
249	236, 247, 248	elmaprd 32843	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
250	249, 238	ffvelcdmd 7061	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
251	245, 246, 250	elmaprd 32843	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑢‘ℎ):𝐵⟶𝐹)
252		simp-4r 793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑐 ∈ 𝐵)
253	251, 252	ffvelcdmd 7061	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
254	244, 253	sseldd 3935	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
255	29, 19, 5, 243, 254	ringlzd 20332	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((0g‘𝐿)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
256	242, 255	eqtrd 2796	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
257	3	ad6antr 746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
258	58	ad6antr 746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐹 ∈ (SubDRing‘𝐽))
259	11	ad6antr 746	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐻 ∈ (SubDRing‘𝐿))
260		ovexd 7426	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝐹 ↑m 𝐵) ∈ V)
261		simp-6r 797	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
262	259, 260, 261	elmaprd 32843	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
263		simpllr 785	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ℎ ∈ 𝐻)
264	262, 263	ffvelcdmd 7061	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
265	257, 258, 264	elmaprd 32843	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ):𝐵⟶𝐹)
266	265	ffnd 6687	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ) Fn 𝐵)
267		fvexd 6877	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (0g‘𝐿) ∈ V)
268		simp-4r 793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑐 ∈ 𝐵)
269		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿)))
270	268, 269	eldifd 3913	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑐 ∈ (𝐵 ∖ ((𝑢‘ℎ) supp (0g‘𝐿))))
271	266, 257, 267, 270	fvdifsupp 8145	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) = (0g‘𝐿))
272	271	oveq2d 7407	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = ((𝑃‘ℎ)(.r‘𝐿)(0g‘𝐿)))
273	197	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐿 ∈ Ring)
274	200	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑃‘ℎ) ∈ (Base‘𝐿))
275	29, 19, 5, 273, 274	ringrzd 20333	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)(0g‘𝐿)) = (0g‘𝐿))
276	272, 275	eqtrd 2796	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
277		df-br 5098	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ ⟨𝑐, ℎ⟩ ∈ ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
278		fveq2 6862	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = 𝑖 → (𝑢‘ℎ) = (𝑢‘𝑖))
279	278	oveq1d 7406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑖 → ((𝑢‘ℎ) supp (0g‘𝐿)) = ((𝑢‘𝑖) supp (0g‘𝐿)))
280		sneq 4589	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑖 → {ℎ} = {𝑖})
281	279, 280	xpeq12d 5674	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = 𝑖 → (((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) = (((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
282	281	cbviunv 4993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) = ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})
283	282	eleq2i 2853	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑐, ℎ⟩ ∈ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) ↔ ⟨𝑐, ℎ⟩ ∈ ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
284		opeliun2xp 5711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑐, ℎ⟩ ∈ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) ↔ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
285	277, 283, 284	3bitr2i 301	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
286	285	notbii 322	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ ¬ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
287		ianor 994	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) ↔ (¬ ℎ ∈ (𝑃 supp (0g‘𝐿)) ∨ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
288	286, 287	sylbb 221	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ → (¬ ℎ ∈ (𝑃 supp (0g‘𝐿)) ∨ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
289	288	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (¬ ℎ ∈ (𝑃 supp (0g‘𝐿)) ∨ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
290	256, 276, 289	mpjaodan 971	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
291	290	oveq1d 7406	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = ((0g‘𝐿)(.r‘𝐿)𝑐))
292	118	ad3antrrr 740	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → 𝐿 ∈ Ring)
293	203	ad2antrr 736	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → 𝑐 ∈ (Base‘𝐿))
294	29, 19, 5, 292, 293	ringlzd 20332	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → ((0g‘𝐿)(.r‘𝐿)𝑐) = (0g‘𝐿))
295	291, 294	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
296	295	an42ds 1509	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
297	296	an32s 662	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
298	297	anasss 470	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ (𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻)) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
299	298	an32s 662	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ (𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻)) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
300	299	anasss 470	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ((𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ)) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
301	29, 5, 196, 4, 154, 206, 233, 300	gsumcom3 20009	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
302	191, 195, 301	3eqtr4d 2806	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
303	118	adantr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐿 ∈ Ring)
304	29, 5, 19, 303, 12, 203, 201, 86	gsummulc1 20351	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))) = ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
305	304	mpteq2dva 5190	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)))) = (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐)))
306	305	oveq2d 7407	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))))
307	117, 302, 306	3eqtrd 2800	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))))
308	51, 162	oveq12d 7409	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)))
309	308	cbvmptv 5201	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)))
310	182	oveq2d 7407	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
311	310	mpteq2dv 5191	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))
312	309, 311	eqtrid 2808	. . . . . . . . 9 ⊢ (𝑏 = 𝑐 → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))
313	312	oveq2d 7407	. . . . . . . 8 ⊢ (𝑏 = 𝑐 → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))))
314	313, 183	oveq12d 7409	. . . . . . 7 ⊢ (𝑏 = 𝑐 → ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏) = ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
315	314	cbvmptv 5201	. . . . . 6 ⊢ (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)) = (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
316	315	oveq2i 7402	. . . . 5 ⊢ (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐)))
317	307, 316	eqtr4di 2814	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))
318	115, 317	jca 519	. . 3 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))))
319	90, 110, 318	rspcedvd 3582	. 2 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))
320		breq1 5100	. . . 4 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑒 finSupp (0g‘𝐿) ↔ (𝑢‘𝑓) finSupp (0g‘𝐿)))
321		fveq1 6861	. . . . . . . 8 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑒‘𝑏) = ((𝑢‘𝑓)‘𝑏))
322	321	oveq1d 7406	. . . . . . 7 ⊢ (𝑒 = (𝑢‘𝑓) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))
323	322	mpteq2dv 5191	. . . . . 6 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))
324	323	oveq2d 7407	. . . . 5 ⊢ (𝑒 = (𝑢‘𝑓) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))
325	324	eqeq2d 2772	. . . 4 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))) ↔ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
326	320, 325	anbi12d 641	. . 3 ⊢ (𝑒 = (𝑢‘𝑓) → ((𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))))
327		ovexd 7426	. . 3 ⊢ (𝜑 → (𝐹 ↑m 𝐵) ∈ V)
328		eqid 2761	. . . . . . . . . 10 ⊢ (LSpan‘((subringAlg ‘𝐽)‘𝐹)) = (LSpan‘((subringAlg ‘𝐽)‘𝐹))
329	139, 140, 328	lbssp 21134	. . . . . . . . 9 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
330	3, 329	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
331	144, 66, 330	3eqtr4rd 2807	. . . . . . 7 ⊢ (𝜑 → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = 𝐻)
332	331	eleq2d 2847	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) ↔ 𝑓 ∈ 𝐻))
333		eqid 2761	. . . . . . 7 ⊢ (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹)))
334		eqid 2761	. . . . . . 7 ⊢ (Scalar‘((subringAlg ‘𝐽)‘𝐹)) = (Scalar‘((subringAlg ‘𝐽)‘𝐹))
335		eqid 2761	. . . . . . 7 ⊢ (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹)))
336		eqid 2761	. . . . . . 7 ⊢ ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))
337		sdrgsubrg 20828	. . . . . . . . 9 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ∈ (SubRing‘𝐽))
338	58, 337	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐽))
339		eqid 2761	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹)
340	339	sralmod 21242	. . . . . . . 8 ⊢ (𝐹 ∈ (SubRing‘𝐽) → ((subringAlg ‘𝐽)‘𝐹) ∈ LMod)
341	338, 340	syl 17	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ LMod)
342	328, 139, 333, 334, 335, 336, 341, 142	ellspds 33515	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) ↔ ∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))))
343	332, 342	bitr3d 283	. . . . 5 ⊢ (𝜑 → (𝑓 ∈ 𝐻 ↔ ∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))))
344	343	biimpa 480	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐻) → ∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))))
345		eqid 2761	. . . . . . . . . 10 ⊢ (𝐽 ↾s 𝐹) = (𝐽 ↾s 𝐹)
346	345, 59	ressbas2 17265	. . . . . . . . 9 ⊢ (𝐹 ⊆ (Base‘𝐽) → 𝐹 = (Base‘(𝐽 ↾s 𝐹)))
347	61, 346	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (Base‘(𝐽 ↾s 𝐹)))
348	143, 61	srasca 21235	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ↾s 𝐹) = (Scalar‘((subringAlg ‘𝐽)‘𝐹)))
349	348	fveq2d 6866	. . . . . . . 8 ⊢ (𝜑 → (Base‘(𝐽 ↾s 𝐹)) = (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))))
350	347, 349	eqtr2d 2797	. . . . . . 7 ⊢ (𝜑 → (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = 𝐹)
351	350	oveq1d 7406	. . . . . 6 ⊢ (𝜑 → ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵) = (𝐹 ↑m 𝐵))
352		sdrgsubrg 20828	. . . . . . . . . . . 12 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ∈ (SubRing‘𝐿))
353	11, 352	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ (SubRing‘𝐿))
354		subrgsubg 20614	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubRing‘𝐿) → 𝐻 ∈ (SubGrp‘𝐿))
355	64, 5	subg0 19165	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubGrp‘𝐿) → (0g‘𝐿) = (0g‘𝐽))
356	353, 354, 355	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝐿) = (0g‘𝐽))
357	64	sdrgdrng 20827	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐽 ∈ DivRing)
358	11, 357	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ DivRing)
359	358	drngringd 20774	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ Ring)
360	359	ringcmnd 20321	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ CMnd)
361	360	cmnmndd 19835	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ Mnd)
362		subrgsubg 20614	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubRing‘𝐽) → 𝐹 ∈ (SubGrp‘𝐽))
363		eqid 2761	. . . . . . . . . . . . 13 ⊢ (0g‘𝐽) = (0g‘𝐽)
364	363	subg0cl 19167	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubGrp‘𝐽) → (0g‘𝐽) ∈ 𝐹)
365	338, 362, 364	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝐽) ∈ 𝐹)
366	345, 59, 363	ress0g 18787	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Mnd ∧ (0g‘𝐽) ∈ 𝐹 ∧ 𝐹 ⊆ (Base‘𝐽)) → (0g‘𝐽) = (0g‘(𝐽 ↾s 𝐹)))
367	361, 365, 61, 366	syl3anc 1389	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝐽) = (0g‘(𝐽 ↾s 𝐹)))
368	348	fveq2d 6866	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘(𝐽 ↾s 𝐹)) = (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))))
369	356, 367, 368	3eqtrrd 2801	. . . . . . . . 9 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (0g‘𝐿))
370	369	breq2d 5109	. . . . . . . 8 ⊢ (𝜑 → (𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↔ 𝑒 finSupp (0g‘𝐿)))
371	370	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↔ 𝑒 finSupp (0g‘𝐿)))
372	3	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
373		subgsubm 19181	. . . . . . . . . . . 12 ⊢ (𝐻 ∈ (SubGrp‘𝐿) → 𝐻 ∈ (SubMnd‘𝐿))
374	353, 354, 373	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ (SubMnd‘𝐿))
375	374	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐻 ∈ (SubMnd‘𝐿))
376	64, 19	ressmulr 17327	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → (.r‘𝐿) = (.r‘𝐽))
377	11, 376	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐿) = (.r‘𝐽))
378	143, 61	sravsca 21236	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐽) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
379	377, 378	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
380	379	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
381	380	oveqd 7408	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) = ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))
382	353	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝐻 ∈ (SubRing‘𝐿))
383	67	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝐹 ⊆ 𝐻)
384	25	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐹 ∈ (SubDRing‘𝐼))
385	351	eleq2d 2847	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵) ↔ 𝑒 ∈ (𝐹 ↑m 𝐵)))
386	385	biimpa 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝑒 ∈ (𝐹 ↑m 𝐵))
387	372, 384, 386	elmaprd 32843	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝑒:𝐵⟶𝐹)
388	387	ffvelcdmda 7060	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (𝑒‘𝑏) ∈ 𝐹)
389	383, 388	sseldd 3935	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (𝑒‘𝑏) ∈ 𝐻)
390	146	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐵 ⊆ 𝐻)
391	390	sselda 3934	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐻)
392	19, 382, 389, 391	subrgmcld 33373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) ∈ 𝐻)
393	381, 392	eqeltrrd 2862	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏) ∈ 𝐻)
394	393	fmpttd 7091	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)):𝐵⟶𝐻)
395	372, 375, 394, 64	gsumsubm 18860	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
396	377, 378	eqtr2d 2797	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = (.r‘𝐿))
397	396	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = (.r‘𝐿))
398	397	oveqd 7408	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏) = ((𝑒‘𝑏)(.r‘𝐿)𝑏))
399	398	mpteq2dv 5191	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)) = (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))
400	399	oveq2d 7407	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))
401	3	mptexd 7203	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)) ∈ V)
402		fvexd 6877	. . . . . . . . . . 11 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ V)
403	339, 401, 358, 402, 61	gsumsra 33188	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
404	403	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
405	395, 400, 404	3eqtr3rd 2805	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))
406	405	eqeq2d 2772	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) ↔ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))))
407	371, 406	anbi12d 641	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ((𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))) ↔ (𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))))
408	351, 407	rexeqbidva 3326	. . . . 5 ⊢ (𝜑 → (∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))) ↔ ∃𝑒 ∈ (𝐹 ↑m 𝐵)(𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))))
409	408	adantr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐻) → (∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))) ↔ ∃𝑒 ∈ (𝐹 ↑m 𝐵)(𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))))
410	344, 409	mpbid 234	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐻) → ∃𝑒 ∈ (𝐹 ↑m 𝐵)(𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))))
411	326, 11, 327, 410	ac6mapd 32786	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
412	319, 411	r19.29a 3169	1 ⊢ (𝜑 → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   = wceq 1559   ∈ wcel 2141  ∀wral 3075  ∃wrex 3085  Vcvv 3453   ∪ cun 3900   ⊆ wss 3902  {csn 4579  ⟨cop 4585  ∪ ciun 4946   class class class wbr 5097   ↦ cmpt 5178   × cxp 5641   Fn wfn 6511  ⟶wf 6512  ‘cfv 6516  (class class class)co 7391   supp csupp 8134   ↑_m cmap 8802  Fincfn 8921   finSupp cfsupp 9301  Basecbs 17236   ↾_s cress 17257  ._rcmulr 17278  Scalarcsca 17280   ·_𝑠 cvsca 17281  0_gc0g 17459   Σ_g cgsu 17460  Mndcmnd 18759  SubMndcsubmnd 18807  SubGrpcsubg 19153  CMndccmn 19811  Ringcrg 20270  SubRingcsubrg 20606  RingSpancrgspn 20647  DivRingcdr 20766  Fieldcfield 20767  SubDRingcsdrg 20823  LModclmod 20915  LSpanclspn 21026  LBasisclbs 21129  subringAlg csra 21226

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-reg 9534  ax-inf2 9590  ax-ac2 10414  ax-cnex 11123  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143  ax-pre-mulgt0 11144

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4863  df-int 4903  df-iun 4948  df-iin 4949  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-se 5597  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-isom 6525  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-of 7655  df-om 7842  df-1st 7965  df-2nd 7966  df-supp 8135  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-1o 8431  df-2o 8432  df-er 8672  df-map 8804  df-ixp 8874  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-fsupp 9302  df-sup 9382  df-oi 9452  df-r1 9716  df-rank 9717  df-card 9891  df-ac 10066  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-sub 11410  df-neg 11411  df-nn 12205  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281  df-n0 12476  df-z 12563  df-dec 12683  df-uz 12834  df-fz 13507  df-fzo 13654  df-seq 14009  df-hash 14338  df-struct 17174  df-sets 17191  df-slot 17209  df-ndx 17221  df-base 17237  df-ress 17258  df-plusg 17290  df-mulr 17291  df-sca 17293  df-vsca 17294  df-ip 17295  df-tset 17296  df-ple 17297  df-ds 17299  df-hom 17301  df-cco 17302  df-0g 17461  df-gsum 17462  df-prds 17467  df-pws 17469  df-mre 17605  df-mrc 17606  df-acs 17608  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-mhm 18808  df-submnd 18809  df-grp 18969  df-minusg 18970  df-sbg 18971  df-mulg 19101  df-subg 19156  df-ghm 19245  df-cntz 19348  df-cmn 19813  df-abl 19814  df-mgp 20178  df-rng 20190  df-ur 20219  df-ring 20272  df-nzr 20550  df-subrng 20583  df-subrg 20607  df-drng 20768  df-field 20769  df-sdrg 20824  df-lmod 20917  df-lss 20987  df-lsp 21027  df-lmhm 21077  df-lbs 21130  df-sra 21228  df-rgmod 21229  df-dsmm 21772  df-frlm 21787  df-uvc 21823

This theorem is referenced by:  fldextrspunlsp  33932