Theorem fldextrspunlsplem 33678

Description: Lemma for fldextrspunlsp 33679: First direction. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)

Hypotheses

Ref	Expression
fldextrspunfld.k	⊢ 𝐾 = (𝐿 ↾s 𝐹)
fldextrspunfld.i	⊢ 𝐼 = (𝐿 ↾s 𝐺)
fldextrspunfld.j	⊢ 𝐽 = (𝐿 ↾s 𝐻)
fldextrspunfld.2	⊢ (𝜑 → 𝐿 ∈ Field)
fldextrspunfld.3	⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
fldextrspunfld.4	⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
fldextrspunfld.5	⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
fldextrspunfld.6	⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
fldextrspunlsp.n	⊢ 𝑁 = (RingSpan‘𝐿)
fldextrspunlsp.c	⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))
fldextrspunlsp.e	⊢ 𝐸 = (𝐿 ↾s 𝐶)
fldextrspunlsp.1	⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
fldextrspunlsp.2	⊢ (𝜑 → 𝐵 ∈ Fin)
fldextrspunlsplem.2	⊢ (𝜑 → 𝑃:𝐻⟶𝐺)
fldextrspunlsplem.3	⊢ (𝜑 → 𝑃 finSupp (0g‘𝐿))
fldextrspunlsplem.4	⊢ (𝜑 → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))))

Assertion

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

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

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

Proof of Theorem fldextrspunlsplem

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

Step	Hyp	Ref	Expression
1		fldextrspunfld.5	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))
2	1	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐺 ∈ (SubDRing‘𝐿))
3		fldextrspunlsp.1	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
4	3	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
5		eqid 2731	. . . . . 6 ⊢ (0g‘𝐿) = (0g‘𝐿)
6		fldextrspunfld.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ Field)
7	6	flddrngd 20651	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ DivRing)
8	7	drngringd 20647	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ Ring)
9	8	ringcmnd 20197	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ CMnd)
10	9	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐿 ∈ CMnd)
11		fldextrspunfld.6	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))
12	11	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐻 ∈ (SubDRing‘𝐿))
13		sdrgsubrg 20701	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
14	1, 13	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
15		subrgsubg 20487	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐿) → 𝐺 ∈ (SubGrp‘𝐿))
16		subgsubm 19056	. . . . . . . 8 ⊢ (𝐺 ∈ (SubGrp‘𝐿) → 𝐺 ∈ (SubMnd‘𝐿))
17	14, 15, 16	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (SubMnd‘𝐿))
18	17	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐺 ∈ (SubMnd‘𝐿))
19		eqid 2731	. . . . . . . . 9 ⊢ (.r‘𝐿) = (.r‘𝐿)
20	14	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐺 ∈ (SubRing‘𝐿))
21		fldextrspunlsplem.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃:𝐻⟶𝐺)
22	21	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑃:𝐻⟶𝐺)
23		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ 𝐻)
24	22, 23	ffvelcdmd 7013	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑃‘𝑓) ∈ 𝐺)
25		fldextrspunfld.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
26		eqid 2731	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐼) = (Base‘𝐼)
27	26	sdrgss 20703	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubDRing‘𝐼) → 𝐹 ⊆ (Base‘𝐼))
28	25, 27	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐼))
29		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐿) = (Base‘𝐿)
30	29	sdrgss 20703	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
31	1, 30	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
32		fldextrspunfld.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (𝐿 ↾s 𝐺)
33	32, 29	ressbas2 17144	. . . . . . . . . . . . 13 ⊢ (𝐺 ⊆ (Base‘𝐿) → 𝐺 = (Base‘𝐼))
34	31, 33	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 = (Base‘𝐼))
35	28, 34	sseqtrrd 3967	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝐺)
36	35	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐹 ⊆ 𝐺)
37	3	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
38	25	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐹 ∈ (SubDRing‘𝐼))
39	11	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝐻 ∈ (SubDRing‘𝐿))
40		ovexd 7376	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝐹 ↑m 𝐵) ∈ V)
41		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
42	39, 40, 41	elmaprd 32653	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
43	42, 23	ffvelcdmd 7013	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑢‘𝑓) ∈ (𝐹 ↑m 𝐵))
44	37, 38, 43	elmaprd 32653	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑢‘𝑓):𝐵⟶𝐹)
45		simplr 768	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑐 ∈ 𝐵)
46	44, 45	ffvelcdmd 7013	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑢‘𝑓)‘𝑐) ∈ 𝐹)
47	36, 46	sseldd 3930	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑢‘𝑓)‘𝑐) ∈ 𝐺)
48	19, 20, 24, 47	subrgmcld 33192	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) ∈ 𝐺)
49	48	fmpttd 7043	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))):𝐻⟶𝐺)
50	49	adantlr 715	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))):𝐻⟶𝐺)
51		fveq2 6817	. . . . . . . . 9 ⊢ (𝑓 = ℎ → (𝑃‘𝑓) = (𝑃‘ℎ))
52		fveq2 6817	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → (𝑢‘𝑓) = (𝑢‘ℎ))
53	52	fveq1d 6819	. . . . . . . . 9 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓)‘𝑐) = ((𝑢‘ℎ)‘𝑐))
54	51, 53	oveq12d 7359	. . . . . . . 8 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
55	54	cbvmptv 5190	. . . . . . 7 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
56		fvexd 6832	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (0g‘𝐿) ∈ V)
57		ssidd 3953	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐻 ⊆ 𝐻)
58		fldextrspunfld.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
59		eqid 2731	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐽) = (Base‘𝐽)
60	59	sdrgss 20703	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
61	58, 60	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
62	29	sdrgss 20703	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
63	11, 62	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
64		fldextrspunfld.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = (𝐿 ↾s 𝐻)
65	64, 29	ressbas2 17144	. . . . . . . . . . . . 13 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
66	63, 65	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
67	61, 66	sseqtrrd 3967	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝐻)
68	67, 63	sstrd 3940	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
69	68	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐹 ⊆ (Base‘𝐿))
70	3	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
71	58	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐹 ∈ (SubDRing‘𝐽))
72		ovexd 7376	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐹 ↑m 𝐵) ∈ V)
73		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
74	12, 72, 73	elmaprd 32653	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
75	74	ffvelcdmda 7012	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
76	70, 71, 75	elmaprd 32653	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ):𝐵⟶𝐹)
77		simplr 768	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝑐 ∈ 𝐵)
78	76, 77	ffvelcdmd 7013	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
79	69, 78	sseldd 3930	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
80	21	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑃:𝐻⟶𝐺)
81		fldextrspunlsplem.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 finSupp (0g‘𝐿))
82	81	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑃 finSupp (0g‘𝐿))
83	8	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝐿 ∈ Ring)
84		simpr 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝑦 ∈ (Base‘𝐿))
85	29, 19, 5, 83, 84	ringlzd 20208	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → ((0g‘𝐿)(.r‘𝐿)𝑦) = (0g‘𝐿))
86	56, 56, 12, 57, 79, 80, 82, 85	fisuppov1 32656	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))) finSupp (0g‘𝐿))
87	55, 86	eqbrtrid 5121	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) finSupp (0g‘𝐿))
88	5, 10, 12, 18, 50, 87	gsumsubmcl 19826	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) ∈ 𝐺)
89	88	fmpttd 7043	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))):𝐵⟶𝐺)
90	2, 4, 89	elmapdd 8760	. . 3 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) ∈ (𝐺 ↑m 𝐵))
91		breq1 5089	. . . . . 6 ⊢ (𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) → (𝑎 finSupp (0g‘𝐿) ↔ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿)))
92	91	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑎 finSupp (0g‘𝐿) ↔ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿)))
93		simplr 768	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))))
94	93	fveq1d 6819	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → (𝑎‘𝑏) = ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏))
95		eqid 2731	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))
96		fveq2 6817	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑏 → ((𝑢‘𝑓)‘𝑐) = ((𝑢‘𝑓)‘𝑏))
97	96	oveq2d 7357	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑏 → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) = ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))
98	97	mpteq2dv 5180	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑏 → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) = (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))
99	98	oveq2d 7357	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑏 → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
100		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
101		ovexd 7376	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))) ∈ V)
102	95, 99, 100, 101	fvmptd3 6947	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
103	102	adantlr 715	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
104	94, 103	eqtrd 2766	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → (𝑎‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
105	104	oveq1d 7356	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → ((𝑎‘𝑏)(.r‘𝐿)𝑏) = ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))
106	105	mpteq2dva 5179	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))
107	106	oveq2d 7357	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))
108	107	eqeq2d 2742	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏))) ↔ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))))
109	92, 108	anbi12d 632	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → ((𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))))
110	109	adantlr 715	. . 3 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → ((𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))))
111		fldextrspunlsp.2	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ Fin)
112	111	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ∈ Fin)
113		ovexd 7376	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) ∈ V)
114		fvexd 6832	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (0g‘𝐿) ∈ V)
115	95, 112, 113, 114	fsuppmptdm 9255	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿))
116		fldextrspunlsplem.4	. . . . . . 7 ⊢ (𝜑 → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))))
117	116	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))))
118	8	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐿 ∈ Ring)
119	118	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐿 ∈ Ring)
120	3	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
121	31	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐺 ⊆ (Base‘𝐿))
122	21	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑃:𝐻⟶𝐺)
123	122	ffvelcdmda 7012	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ 𝐺)
124	121, 123	sseldd 3930	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ (Base‘𝐿))
125	119	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐿 ∈ Ring)
126	68	ad4antr 732	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐹 ⊆ (Base‘𝐿))
127	3	ad4antr 732	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
128	58	ad4antr 732	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐹 ∈ (SubDRing‘𝐽))
129	11	ad4antr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝐻 ∈ (SubDRing‘𝐿))
130		ovexd 7376	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝐹 ↑m 𝐵) ∈ V)
131		simp-4r 783	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
132	129, 130, 131	elmaprd 32653	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
133		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ℎ ∈ 𝐻)
134	132, 133	ffvelcdmd 7013	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
135	127, 128, 134	elmaprd 32653	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑢‘ℎ):𝐵⟶𝐹)
136		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵)
137	135, 136	ffvelcdmd 7013	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
138	126, 137	sseldd 3930	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
139		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
140		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
141	139, 140	lbsss 21006	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
142	3, 141	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
143		eqidd 2732	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
144	143, 61	srabase 21106	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
145	66, 144	eqtr2d 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘((subringAlg ‘𝐽)‘𝐹)) = 𝐻)
146	142, 145	sseqtrd 3966	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ⊆ 𝐻)
147	146, 63	sstrd 3940	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝐿))
148	147	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ⊆ (Base‘𝐿))
149	148	sselda 3929	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ (Base‘𝐿))
150	29, 19, 125, 138, 149	ringcld 20173	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
151		fvexd 6832	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (0g‘𝐿) ∈ V)
152		ssidd 3953	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ⊆ 𝐵)
153	58	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐹 ∈ (SubDRing‘𝐽))
154	11	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐻 ∈ (SubDRing‘𝐿))
155		ovexd 7376	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐹 ↑m 𝐵) ∈ V)
156		simplr 768	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
157	154, 155, 156	elmaprd 32653	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
158	157	ffvelcdmda 7012	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
159	120, 153, 158	elmaprd 32653	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ):𝐵⟶𝐹)
160	52	breq1d 5096	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓) finSupp (0g‘𝐿) ↔ (𝑢‘ℎ) finSupp (0g‘𝐿)))
161		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → 𝑓 = ℎ)
162	52	fveq1d 6819	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓)‘𝑏) = ((𝑢‘ℎ)‘𝑏))
163	162	oveq1d 7356	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = ℎ → (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))
164	163	mpteq2dv 5180	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))
165	164	oveq2d 7357	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))
166	161, 165	eqeq12d 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → (𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))) ↔ ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))))
167	160, 166	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ℎ → (((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑢‘ℎ) finSupp (0g‘𝐿) ∧ ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))))
168		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
169		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ ∈ 𝐻)
170	167, 168, 169	rspcdva 3573	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ) finSupp (0g‘𝐿) ∧ ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))))
171	170	simpld 494	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) finSupp (0g‘𝐿))
172	119	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝐿 ∈ Ring)
173		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → 𝑦 ∈ (Base‘𝐿))
174	29, 19, 5, 172, 173	ringlzd 20208	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → ((0g‘𝐿)(.r‘𝐿)𝑦) = (0g‘𝐿))
175	151, 151, 120, 152, 149, 159, 171, 174	fisuppov1 32656	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)) finSupp (0g‘𝐿))
176	29, 5, 19, 119, 120, 124, 150, 175	gsummulc2 20230	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))) = ((𝑃‘ℎ)(.r‘𝐿)(𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
177	124	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑃‘ℎ) ∈ (Base‘𝐿))
178	29, 19, 125, 177, 138, 149	ringassd 20170	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))
179	178	mpteq2dva 5179	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)) = (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))))
180	179	oveq2d 7357	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
181	170	simprd 495	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))
182		fveq2 6817	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → ((𝑢‘ℎ)‘𝑏) = ((𝑢‘ℎ)‘𝑐))
183		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → 𝑏 = 𝑐)
184	182, 183	oveq12d 7359	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))
185	184	cbvmptv 5190	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)) = (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))
186	185	oveq2i 7352	. . . . . . . . . . . 12 ⊢ (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))
187	181, 186	eqtrdi 2782	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))))
188	187	oveq2d 7357	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)ℎ) = ((𝑃‘ℎ)(.r‘𝐿)(𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
189	176, 180, 188	3eqtr4rd 2777	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)ℎ) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))
190	189	mpteq2dva 5179	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ)) = (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)))))
191	190	oveq2d 7357	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
192	51, 161	oveq12d 7359	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)𝑓) = ((𝑃‘ℎ)(.r‘𝐿)ℎ))
193	192	cbvmptv 5190	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓)) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))
194	193	oveq2i 7352	. . . . . . . 8 ⊢ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ)))
195	194	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))))
196	9	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐿 ∈ CMnd)
197	8	ad4antr 732	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐿 ∈ Ring)
198	31	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝐺 ⊆ (Base‘𝐿))
199	80	ffvelcdmda 7012	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ 𝐺)
200	198, 199	sseldd 3930	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ (Base‘𝐿))
201	29, 19, 197, 200, 79	ringcld 20173	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) ∈ (Base‘𝐿))
202	147	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ⊆ (Base‘𝐿))
203	202	sselda 3929	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ (Base‘𝐿))
204	203	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝑐 ∈ (Base‘𝐿))
205	29, 19, 197, 201, 204	ringcld 20173	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
206	205	anasss 466	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ (𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻)) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
207	81	fsuppimpd 9248	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 supp (0g‘𝐿)) ∈ Fin)
208	207	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑃 supp (0g‘𝐿)) ∈ Fin)
209		suppssdm 8102	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 supp (0g‘𝐿)) ⊆ dom 𝑃
210	209, 21	fssdm 6665	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 supp (0g‘𝐿)) ⊆ 𝐻)
211	210	sseld 3928	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑓 ∈ (𝑃 supp (0g‘𝐿)) → 𝑓 ∈ 𝐻))
212	211	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → (𝑓 ∈ (𝑃 supp (0g‘𝐿)) → 𝑓 ∈ 𝐻))
213		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ (𝑢‘𝑓) finSupp (0g‘𝐿)) → (𝑢‘𝑓) finSupp (0g‘𝐿))
214	213	fsuppimpd 9248	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ (𝑢‘𝑓) finSupp (0g‘𝐿)) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin)
215	214	ex 412	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → ((𝑢‘𝑓) finSupp (0g‘𝐿) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin))
216	215	adantrd 491	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → (((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin))
217	212, 216	imim12d 81	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → ((𝑓 ∈ 𝐻 → ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑓 ∈ (𝑃 supp (0g‘𝐿)) → ((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin)))
218	217	ralimdv2 3141	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) → (∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))) → ∀𝑓 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin))
219	218	imp 406	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∀𝑓 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin)
220		fveq2 6817	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑖 → (𝑢‘𝑓) = (𝑢‘𝑖))
221	220	oveq1d 7356	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑖 → ((𝑢‘𝑓) supp (0g‘𝐿)) = ((𝑢‘𝑖) supp (0g‘𝐿)))
222	221	eleq1d 2816	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑖 → (((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin ↔ ((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin))
223	222	cbvralvw 3210	. . . . . . . . . . . 12 ⊢ (∀𝑓 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin ↔ ∀𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
224	219, 223	sylib 218	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∀𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
225		iunfi 9222	. . . . . . . . . . 11 ⊢ (((𝑃 supp (0g‘𝐿)) ∈ Fin ∧ ∀𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
226	208, 224, 225	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin)
227		xpfi 9199	. . . . . . . . . 10 ⊢ ((∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin ∧ (𝑃 supp (0g‘𝐿)) ∈ Fin) → (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))) ∈ Fin)
228	226, 208, 227	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))) ∈ Fin)
229		snssi 4755	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (𝑃 supp (0g‘𝐿)) → {𝑖} ⊆ (𝑃 supp (0g‘𝐿)))
230	229	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑃 supp (0g‘𝐿))) → {𝑖} ⊆ (𝑃 supp (0g‘𝐿)))
231	230	iunxpssiun1 32540	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ⊆ (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))))
232	231	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ⊆ (∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))((𝑢‘𝑖) supp (0g‘𝐿)) × (𝑃 supp (0g‘𝐿))))
233	228, 232	ssfid 9148	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ∈ Fin)
234	21	ffnd 6647	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑃 Fn 𝐻)
235	234	ad6antr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑃 Fn 𝐻)
236	11	ad6antr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐻 ∈ (SubDRing‘𝐿))
237		fvexd 6832	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (0g‘𝐿) ∈ V)
238		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ℎ ∈ 𝐻)
239		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ¬ ℎ ∈ (𝑃 supp (0g‘𝐿)))
240	238, 239	eldifd 3908	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ℎ ∈ (𝐻 ∖ (𝑃 supp (0g‘𝐿))))
241	235, 236, 237, 240	fvdifsupp 8096	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑃‘ℎ) = (0g‘𝐿))
242	241	oveq1d 7356	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = ((0g‘𝐿)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
243	8	ad6antr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐿 ∈ Ring)
244	68	ad6antr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐹 ⊆ (Base‘𝐿))
245	3	ad6antr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
246	58	ad6antr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝐹 ∈ (SubDRing‘𝐽))
247		ovexd 7376	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝐹 ↑m 𝐵) ∈ V)
248		simp-6r 787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
249	236, 247, 248	elmaprd 32653	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
250	249, 238	ffvelcdmd 7013	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
251	245, 246, 250	elmaprd 32653	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑢‘ℎ):𝐵⟶𝐹)
252		simp-4r 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑐 ∈ 𝐵)
253	251, 252	ffvelcdmd 7013	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
254	244, 253	sseldd 3930	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
255	29, 19, 5, 243, 254	ringlzd 20208	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((0g‘𝐿)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
256	242, 255	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
257	3	ad6antr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
258	58	ad6antr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐹 ∈ (SubDRing‘𝐽))
259	11	ad6antr 736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐻 ∈ (SubDRing‘𝐿))
260		ovexd 7376	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝐹 ↑m 𝐵) ∈ V)
261		simp-6r 787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
262	259, 260, 261	elmaprd 32653	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
263		simpllr 775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ℎ ∈ 𝐻)
264	262, 263	ffvelcdmd 7013	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
265	257, 258, 264	elmaprd 32653	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ):𝐵⟶𝐹)
266	265	ffnd 6647	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ) Fn 𝐵)
267		fvexd 6832	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (0g‘𝐿) ∈ V)
268		simp-4r 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑐 ∈ 𝐵)
269		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿)))
270	268, 269	eldifd 3908	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑐 ∈ (𝐵 ∖ ((𝑢‘ℎ) supp (0g‘𝐿))))
271	266, 257, 267, 270	fvdifsupp 8096	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) = (0g‘𝐿))
272	271	oveq2d 7357	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = ((𝑃‘ℎ)(.r‘𝐿)(0g‘𝐿)))
273	197	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝐿 ∈ Ring)
274	200	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑃‘ℎ) ∈ (Base‘𝐿))
275	29, 19, 5, 273, 274	ringrzd 20209	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)(0g‘𝐿)) = (0g‘𝐿))
276	272, 275	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
277		df-br 5087	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ ⟨𝑐, ℎ⟩ ∈ ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
278		fveq2 6817	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = 𝑖 → (𝑢‘ℎ) = (𝑢‘𝑖))
279	278	oveq1d 7356	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑖 → ((𝑢‘ℎ) supp (0g‘𝐿)) = ((𝑢‘𝑖) supp (0g‘𝐿)))
280		sneq 4581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑖 → {ℎ} = {𝑖})
281	279, 280	xpeq12d 5642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = 𝑖 → (((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) = (((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
282	281	cbviunv 4984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) = ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})
283	282	eleq2i 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑐, ℎ⟩ ∈ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) ↔ ⟨𝑐, ℎ⟩ ∈ ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
284		opeliun2xp 5679	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑐, ℎ⟩ ∈ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) ↔ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
285	277, 283, 284	3bitr2i 299	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
286	285	notbii 320	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ ¬ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
287		ianor 983	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (ℎ ∈ (𝑃 supp (0g‘𝐿)) ∧ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) ↔ (¬ ℎ ∈ (𝑃 supp (0g‘𝐿)) ∨ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
288	286, 287	sylbb 219	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ → (¬ ℎ ∈ (𝑃 supp (0g‘𝐿)) ∨ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
289	288	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (¬ ℎ ∈ (𝑃 supp (0g‘𝐿)) ∨ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))))
290	256, 276, 289	mpjaodan 960	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
291	290	oveq1d 7356	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = ((0g‘𝐿)(.r‘𝐿)𝑐))
292	118	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → 𝐿 ∈ Ring)
293	203	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → 𝑐 ∈ (Base‘𝐿))
294	29, 19, 5, 292, 293	ringlzd 20208	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → ((0g‘𝐿)(.r‘𝐿)𝑐) = (0g‘𝐿))
295	291, 294	eqtrd 2766	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
296	295	an42ds 1491	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
297	296	an32s 652	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
298	297	anasss 466	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ (𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻)) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
299	298	an32s 652	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ (𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻)) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
300	299	anasss 466	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ((𝑐 ∈ 𝐵 ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ)) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
301	29, 5, 196, 4, 154, 206, 233, 300	gsumcom3 19885	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
302	191, 195, 301	3eqtr4d 2776	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
303	118	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐿 ∈ Ring)
304	29, 5, 19, 303, 12, 203, 201, 86	gsummulc1 20229	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))) = ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
305	304	mpteq2dva 5179	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)))) = (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐)))
306	305	oveq2d 7357	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))))
307	117, 302, 306	3eqtrd 2770	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))))
308	51, 162	oveq12d 7359	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)))
309	308	cbvmptv 5190	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)))
310	182	oveq2d 7357	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
311	310	mpteq2dv 5180	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))
312	309, 311	eqtrid 2778	. . . . . . . . 9 ⊢ (𝑏 = 𝑐 → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))
313	312	oveq2d 7357	. . . . . . . 8 ⊢ (𝑏 = 𝑐 → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))))
314	313, 183	oveq12d 7359	. . . . . . 7 ⊢ (𝑏 = 𝑐 → ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏) = ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
315	314	cbvmptv 5190	. . . . . 6 ⊢ (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)) = (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
316	315	oveq2i 7352	. . . . 5 ⊢ (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐)))
317	307, 316	eqtr4di 2784	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))
318	115, 317	jca 511	. . 3 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))))
319	90, 110, 318	rspcedvd 3574	. 2 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))
320		breq1 5089	. . . 4 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑒 finSupp (0g‘𝐿) ↔ (𝑢‘𝑓) finSupp (0g‘𝐿)))
321		fveq1 6816	. . . . . . . 8 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑒‘𝑏) = ((𝑢‘𝑓)‘𝑏))
322	321	oveq1d 7356	. . . . . . 7 ⊢ (𝑒 = (𝑢‘𝑓) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))
323	322	mpteq2dv 5180	. . . . . 6 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))
324	323	oveq2d 7357	. . . . 5 ⊢ (𝑒 = (𝑢‘𝑓) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))
325	324	eqeq2d 2742	. . . 4 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))) ↔ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
326	320, 325	anbi12d 632	. . 3 ⊢ (𝑒 = (𝑢‘𝑓) → ((𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))))
327		ovexd 7376	. . 3 ⊢ (𝜑 → (𝐹 ↑m 𝐵) ∈ V)
328		eqid 2731	. . . . . . . . . 10 ⊢ (LSpan‘((subringAlg ‘𝐽)‘𝐹)) = (LSpan‘((subringAlg ‘𝐽)‘𝐹))
329	139, 140, 328	lbssp 21008	. . . . . . . . 9 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
330	3, 329	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
331	144, 66, 330	3eqtr4rd 2777	. . . . . . 7 ⊢ (𝜑 → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = 𝐻)
332	331	eleq2d 2817	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) ↔ 𝑓 ∈ 𝐻))
333		eqid 2731	. . . . . . 7 ⊢ (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹)))
334		eqid 2731	. . . . . . 7 ⊢ (Scalar‘((subringAlg ‘𝐽)‘𝐹)) = (Scalar‘((subringAlg ‘𝐽)‘𝐹))
335		eqid 2731	. . . . . . 7 ⊢ (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹)))
336		eqid 2731	. . . . . . 7 ⊢ ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))
337		sdrgsubrg 20701	. . . . . . . . 9 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ∈ (SubRing‘𝐽))
338	58, 337	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐽))
339		eqid 2731	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹)
340	339	sralmod 21116	. . . . . . . 8 ⊢ (𝐹 ∈ (SubRing‘𝐽) → ((subringAlg ‘𝐽)‘𝐹) ∈ LMod)
341	338, 340	syl 17	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ LMod)
342	328, 139, 333, 334, 335, 336, 341, 142	ellspds 33325	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) ↔ ∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))))
343	332, 342	bitr3d 281	. . . . 5 ⊢ (𝜑 → (𝑓 ∈ 𝐻 ↔ ∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))))
344	343	biimpa 476	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐻) → ∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))))
345		eqid 2731	. . . . . . . . . 10 ⊢ (𝐽 ↾s 𝐹) = (𝐽 ↾s 𝐹)
346	345, 59	ressbas2 17144	. . . . . . . . 9 ⊢ (𝐹 ⊆ (Base‘𝐽) → 𝐹 = (Base‘(𝐽 ↾s 𝐹)))
347	61, 346	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (Base‘(𝐽 ↾s 𝐹)))
348	143, 61	srasca 21109	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ↾s 𝐹) = (Scalar‘((subringAlg ‘𝐽)‘𝐹)))
349	348	fveq2d 6821	. . . . . . . 8 ⊢ (𝜑 → (Base‘(𝐽 ↾s 𝐹)) = (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))))
350	347, 349	eqtr2d 2767	. . . . . . 7 ⊢ (𝜑 → (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = 𝐹)
351	350	oveq1d 7356	. . . . . 6 ⊢ (𝜑 → ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵) = (𝐹 ↑m 𝐵))
352		sdrgsubrg 20701	. . . . . . . . . . . 12 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ∈ (SubRing‘𝐿))
353	11, 352	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ (SubRing‘𝐿))
354		subrgsubg 20487	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubRing‘𝐿) → 𝐻 ∈ (SubGrp‘𝐿))
355	64, 5	subg0 19040	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubGrp‘𝐿) → (0g‘𝐿) = (0g‘𝐽))
356	353, 354, 355	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝐿) = (0g‘𝐽))
357	64	sdrgdrng 20700	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐽 ∈ DivRing)
358	11, 357	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ DivRing)
359	358	drngringd 20647	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ Ring)
360	359	ringcmnd 20197	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ CMnd)
361	360	cmnmndd 19711	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ Mnd)
362		subrgsubg 20487	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubRing‘𝐽) → 𝐹 ∈ (SubGrp‘𝐽))
363		eqid 2731	. . . . . . . . . . . . 13 ⊢ (0g‘𝐽) = (0g‘𝐽)
364	363	subg0cl 19042	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubGrp‘𝐽) → (0g‘𝐽) ∈ 𝐹)
365	338, 362, 364	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝐽) ∈ 𝐹)
366	345, 59, 363	ress0g 18665	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Mnd ∧ (0g‘𝐽) ∈ 𝐹 ∧ 𝐹 ⊆ (Base‘𝐽)) → (0g‘𝐽) = (0g‘(𝐽 ↾s 𝐹)))
367	361, 365, 61, 366	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝐽) = (0g‘(𝐽 ↾s 𝐹)))
368	348	fveq2d 6821	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘(𝐽 ↾s 𝐹)) = (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))))
369	356, 367, 368	3eqtrrd 2771	. . . . . . . . 9 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (0g‘𝐿))
370	369	breq2d 5098	. . . . . . . 8 ⊢ (𝜑 → (𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↔ 𝑒 finSupp (0g‘𝐿)))
371	370	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↔ 𝑒 finSupp (0g‘𝐿)))
372	3	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))
373		subgsubm 19056	. . . . . . . . . . . 12 ⊢ (𝐻 ∈ (SubGrp‘𝐿) → 𝐻 ∈ (SubMnd‘𝐿))
374	353, 354, 373	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ (SubMnd‘𝐿))
375	374	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐻 ∈ (SubMnd‘𝐿))
376	64, 19	ressmulr 17206	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → (.r‘𝐿) = (.r‘𝐽))
377	11, 376	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐿) = (.r‘𝐽))
378	143, 61	sravsca 21110	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐽) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
379	377, 378	eqtrd 2766	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
380	379	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
381	380	oveqd 7358	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) = ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))
382	353	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝐻 ∈ (SubRing‘𝐿))
383	67	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝐹 ⊆ 𝐻)
384	25	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐹 ∈ (SubDRing‘𝐼))
385	351	eleq2d 2817	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵) ↔ 𝑒 ∈ (𝐹 ↑m 𝐵)))
386	385	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝑒 ∈ (𝐹 ↑m 𝐵))
387	372, 384, 386	elmaprd 32653	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝑒:𝐵⟶𝐹)
388	387	ffvelcdmda 7012	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (𝑒‘𝑏) ∈ 𝐹)
389	383, 388	sseldd 3930	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (𝑒‘𝑏) ∈ 𝐻)
390	146	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐵 ⊆ 𝐻)
391	390	sselda 3929	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐻)
392	19, 382, 389, 391	subrgmcld 33192	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) ∈ 𝐻)
393	381, 392	eqeltrrd 2832	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏) ∈ 𝐻)
394	393	fmpttd 7043	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)):𝐵⟶𝐻)
395	372, 375, 394, 64	gsumsubm 18738	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
396	377, 378	eqtr2d 2767	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = (.r‘𝐿))
397	396	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = (.r‘𝐿))
398	397	oveqd 7358	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏) = ((𝑒‘𝑏)(.r‘𝐿)𝑏))
399	398	mpteq2dv 5180	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)) = (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))
400	399	oveq2d 7357	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))
401	3	mptexd 7153	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)) ∈ V)
402		fvexd 6832	. . . . . . . . . . 11 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ V)
403	339, 401, 358, 402, 61	gsumsra 33019	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
404	403	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
405	395, 400, 404	3eqtr3rd 2775	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))
406	405	eqeq2d 2742	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) ↔ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))))
407	371, 406	anbi12d 632	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ((𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))) ↔ (𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))))
408	351, 407	rexeqbidva 3299	. . . . 5 ⊢ (𝜑 → (∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))) ↔ ∃𝑒 ∈ (𝐹 ↑m 𝐵)(𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))))
409	408	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐻) → (∃𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)(𝑒 finSupp (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ∧ 𝑓 = (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)))) ↔ ∃𝑒 ∈ (𝐹 ↑m 𝐵)(𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))))
410	344, 409	mpbid 232	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐻) → ∃𝑒 ∈ (𝐹 ↑m 𝐵)(𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))))
411	326, 11, 327, 410	ac6mapd 32598	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
412	319, 411	r19.29a 3140	1 ⊢ (𝜑 → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056  Vcvv 3436   ∪ cun 3895   ⊆ wss 3897  {csn 4571  ⟨cop 4577  ∪ ciun 4936   class class class wbr 5086   ↦ cmpt 5167   × cxp 5609   Fn wfn 6471  ⟶wf 6472  ‘cfv 6476  (class class class)co 7341   supp csupp 8085   ↑_m cmap 8745  Fincfn 8864   finSupp cfsupp 9240  Basecbs 17115   ↾_s cress 17136  ._rcmulr 17157  Scalarcsca 17159   ·_𝑠 cvsca 17160  0_gc0g 17338   Σ_g cgsu 17339  Mndcmnd 18637  SubMndcsubmnd 18685  SubGrpcsubg 19028  CMndccmn 19687  Ringcrg 20146  SubRingcsubrg 20479  RingSpancrgspn 20520  DivRingcdr 20639  Fieldcfield 20640  SubDRingcsdrg 20696  LModclmod 20788  LSpanclspn 20899  LBasisclbs 21003  subringAlg csra 21100

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

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

This theorem is referenced by:  fldextrspunlsp  33679