Theorem fldextrspunlsplem 33665

Description: Lemma for fldextrspunlsp 33666: 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 2734	. . . . . 6 ⊢ (0g‘𝐿) = (0g‘𝐿)
6		fldextrspunfld.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ Field)
7	6	flddrngd 20710	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ DivRing)
8	7	drngringd 20706	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ Ring)
9	8	ringcmnd 20250	. . . . . . 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 20761	. . . . . . . . 9 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ∈ (SubRing‘𝐿))
14	1, 13	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (SubRing‘𝐿))
15		subrgsubg 20546	. . . . . . . 8 ⊢ (𝐺 ∈ (SubRing‘𝐿) → 𝐺 ∈ (SubGrp‘𝐿))
16		subgsubm 19136	. . . . . . . 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 2734	. . . . . . . . 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 7085	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑃‘𝑓) ∈ 𝐺)
25		fldextrspunfld.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))
26		eqid 2734	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐼) = (Base‘𝐼)
27	26	sdrgss 20763	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubDRing‘𝐼) → 𝐹 ⊆ (Base‘𝐼))
28	25, 27	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐼))
29		eqid 2734	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝐿) = (Base‘𝐿)
30	29	sdrgss 20763	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ (SubDRing‘𝐿) → 𝐺 ⊆ (Base‘𝐿))
31	1, 30	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ⊆ (Base‘𝐿))
32		fldextrspunfld.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (𝐿 ↾s 𝐺)
33	32, 29	ressbas2 17262	. . . . . . . . . . . . 13 ⊢ (𝐺 ⊆ (Base‘𝐿) → 𝐺 = (Base‘𝐼))
34	31, 33	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 = (Base‘𝐼))
35	28, 34	sseqtrrd 4001	. . . . . . . . . . 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 7448	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝐹 ↑m 𝐵) ∈ V)
41		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻))
42	39, 40, 41	elmaprd 32625	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
43	42, 23	ffvelcdmd 7085	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑢‘𝑓) ∈ (𝐹 ↑m 𝐵))
44	37, 38, 43	elmaprd 32625	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → (𝑢‘𝑓):𝐵⟶𝐹)
45		simplr 768	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → 𝑐 ∈ 𝐵)
46	44, 45	ffvelcdmd 7085	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑢‘𝑓)‘𝑐) ∈ 𝐹)
47	36, 46	sseldd 3964	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑢‘𝑓)‘𝑐) ∈ 𝐺)
48	19, 20, 24, 47	subrgmcld 33181	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) ∧ 𝑓 ∈ 𝐻) → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) ∈ 𝐺)
49	48	fmpttd 7115	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))):𝐻⟶𝐺)
50	49	adantlr 715	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))):𝐻⟶𝐺)
51		fveq2 6886	. . . . . . . . 9 ⊢ (𝑓 = ℎ → (𝑃‘𝑓) = (𝑃‘ℎ))
52		fveq2 6886	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → (𝑢‘𝑓) = (𝑢‘ℎ))
53	52	fveq1d 6888	. . . . . . . . 9 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓)‘𝑐) = ((𝑢‘ℎ)‘𝑐))
54	51, 53	oveq12d 7431	. . . . . . . 8 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
55	54	cbvmptv 5235	. . . . . . 7 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
56		fvexd 6901	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (0g‘𝐿) ∈ V)
57		ssidd 3987	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝐻 ⊆ 𝐻)
58		fldextrspunfld.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))
59		eqid 2734	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐽) = (Base‘𝐽)
60	59	sdrgss 20763	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ⊆ (Base‘𝐽))
61	58, 60	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐽))
62	29	sdrgss 20763	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ⊆ (Base‘𝐿))
63	11, 62	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ⊆ (Base‘𝐿))
64		fldextrspunfld.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = (𝐿 ↾s 𝐻)
65	64, 29	ressbas2 17262	. . . . . . . . . . . . 13 ⊢ (𝐻 ⊆ (Base‘𝐿) → 𝐻 = (Base‘𝐽))
66	63, 65	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 = (Base‘𝐽))
67	61, 66	sseqtrrd 4001	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝐻)
68	67, 63	sstrd 3974	. . . . . . . . . 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 7448	. . . . . . . . . . . . 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 32625	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
75	74	ffvelcdmda 7084	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
76	70, 71, 75	elmaprd 32625	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ):𝐵⟶𝐹)
77		simplr 768	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → 𝑐 ∈ 𝐵)
78	76, 77	ffvelcdmd 7085	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
79	69, 78	sseldd 3964	. . . . . . . 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 20261	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ 𝑦 ∈ (Base‘𝐿)) → ((0g‘𝐿)(.r‘𝐿)𝑦) = (0g‘𝐿))
86	56, 56, 12, 57, 79, 80, 82, 85	fisuppov1 32628	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))) finSupp (0g‘𝐿))
87	55, 86	eqbrtrid 5158	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) finSupp (0g‘𝐿))
88	5, 10, 12, 18, 50, 87	gsumsubmcl 19906	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) ∈ 𝐺)
89	88	fmpttd 7115	. . . 4 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))):𝐵⟶𝐺)
90	2, 4, 89	elmapdd 8863	. . 3 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) ∈ (𝐺 ↑m 𝐵))
91		breq1 5126	. . . . . 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 6888	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → (𝑎‘𝑏) = ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏))
95		eqid 2734	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))))) = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))
96		fveq2 6886	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑏 → ((𝑢‘𝑓)‘𝑐) = ((𝑢‘𝑓)‘𝑏))
97	96	oveq2d 7429	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑏 → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)) = ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))
98	97	mpteq2dv 5224	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑏 → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐))) = (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))
99	98	oveq2d 7429	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑏 → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
100		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
101		ovexd 7448	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))) ∈ V)
102	95, 99, 100, 101	fvmptd3 7019	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑏 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
103	102	adantlr 715	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
104	94, 103	eqtrd 2769	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → (𝑎‘𝑏) = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))))
105	104	oveq1d 7428	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) ∧ 𝑏 ∈ 𝐵) → ((𝑎‘𝑏)(.r‘𝐿)𝑏) = ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))
106	105	mpteq2dva 5222	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)))
107	106	oveq2d 7429	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ 𝑎 = (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))))) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))))
108	107	eqeq2d 2745	. . . . 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 7448	. . . . 5 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑐)))) ∈ V)
114		fvexd 6901	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (0g‘𝐿) ∈ V)
115	95, 112, 113, 114	fsuppmptdm 9398	. . . 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 7084	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ 𝐺)
124	121, 123	sseldd 3964	. . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . . 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 32625	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
133		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ℎ ∈ 𝐻)
134	132, 133	ffvelcdmd 7085	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
135	127, 128, 134	elmaprd 32625	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (𝑢‘ℎ):𝐵⟶𝐹)
136		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵)
137	135, 136	ffvelcdmd 7085	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
138	126, 137	sseldd 3964	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
139		eqid 2734	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘((subringAlg ‘𝐽)‘𝐹)) = (Base‘((subringAlg ‘𝐽)‘𝐹))
140		eqid 2734	. . . . . . . . . . . . . . . . . 18 ⊢ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) = (LBasis‘((subringAlg ‘𝐽)‘𝐹))
141	139, 140	lbsss 21045	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
142	3, 141	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ⊆ (Base‘((subringAlg ‘𝐽)‘𝐹)))
143		eqidd 2735	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹))
144	143, 61	srabase 21145	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Base‘𝐽) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
145	66, 144	eqtr2d 2770	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘((subringAlg ‘𝐽)‘𝐹)) = 𝐻)
146	142, 145	sseqtrd 4000	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ⊆ 𝐻)
147	146, 63	sstrd 3974	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝐿))
148	147	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → 𝐵 ⊆ (Base‘𝐿))
149	148	sselda 3963	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ (Base‘𝐿))
150	29, 19, 125, 138, 149	ringcld 20226	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐) ∈ (Base‘𝐿))
151		fvexd 6901	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (0g‘𝐿) ∈ V)
152		ssidd 3987	. . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . 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 32625	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
158	157	ffvelcdmda 7084	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
159	120, 153, 158	elmaprd 32625	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑢‘ℎ):𝐵⟶𝐹)
160	52	breq1d 5133	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓) finSupp (0g‘𝐿) ↔ (𝑢‘ℎ) finSupp (0g‘𝐿)))
161		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → 𝑓 = ℎ)
162	52	fveq1d 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = ℎ → ((𝑢‘𝑓)‘𝑏) = ((𝑢‘ℎ)‘𝑏))
163	162	oveq1d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = ℎ → (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))
164	163	mpteq2dv 5224	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ℎ → (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)))
165	164	oveq2d 7429	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ℎ → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))))
166	161, 165	eqeq12d 2750	. . . . . . . . . . . . . . 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 3606	. . . . . . . . . . . . 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 20261	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑦 ∈ (Base‘𝐿)) → ((0g‘𝐿)(.r‘𝐿)𝑦) = (0g‘𝐿))
175	151, 151, 120, 152, 149, 159, 171, 174	fisuppov1 32628	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)) finSupp (0g‘𝐿))
176	29, 5, 19, 119, 120, 124, 150, 175	gsummulc2 20283	. . . . . . . . . 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 20223	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) ∧ 𝑐 ∈ 𝐵) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))
179	178	mpteq2dva 5222	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)) = (𝑐 ∈ 𝐵 ↦ ((𝑃‘ℎ)(.r‘𝐿)(((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))))
180	179	oveq2d 7429	. . . . . . . . . 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 6886	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → ((𝑢‘ℎ)‘𝑏) = ((𝑢‘ℎ)‘𝑐))
183		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑐 → 𝑏 = 𝑐)
184	182, 183	oveq12d 7431	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑐 → (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))
185	184	cbvmptv 5235	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏)) = (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))
186	185	oveq2i 7424	. . . . . . . . . . . 12 ⊢ (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))
187	181, 186	eqtrdi 2785	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ℎ = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐))))
188	187	oveq2d 7429	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)ℎ) = ((𝑃‘ℎ)(.r‘𝐿)(𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑢‘ℎ)‘𝑐)(.r‘𝐿)𝑐)))))
189	176, 180, 188	3eqtr4rd 2780	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)ℎ) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))
190	189	mpteq2dva 5222	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ)) = (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)))))
191	190	oveq2d 7429	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
192	51, 161	oveq12d 7431	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)𝑓) = ((𝑃‘ℎ)(.r‘𝐿)ℎ))
193	192	cbvmptv 5235	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓)) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)ℎ))
194	193	oveq2i 7424	. . . . . . . 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 7084	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ 𝐺)
200	198, 199	sseldd 3964	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → (𝑃‘ℎ) ∈ (Base‘𝐿))
201	29, 19, 197, 200, 79	ringcld 20226	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) ∈ (Base‘𝐿))
202	147	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝐵 ⊆ (Base‘𝐿))
203	202	sselda 3963	. . . . . . . . . . 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 20226	. . . . . . . . 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 9391	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 supp (0g‘𝐿)) ∈ Fin)
208	207	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑃 supp (0g‘𝐿)) ∈ Fin)
209		suppssdm 8184	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 supp (0g‘𝐿)) ⊆ dom 𝑃
210	209, 21	fssdm 6735	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 supp (0g‘𝐿)) ⊆ 𝐻)
211	210	sseld 3962	. . . . . . . . . . . . . . . 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 9391	. . . . . . . . . . . . . . . . 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 3150	. . . . . . . . . . . . 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 6886	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑖 → (𝑢‘𝑓) = (𝑢‘𝑖))
221	220	oveq1d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑖 → ((𝑢‘𝑓) supp (0g‘𝐿)) = ((𝑢‘𝑖) supp (0g‘𝐿)))
222	221	eleq1d 2818	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑖 → (((𝑢‘𝑓) supp (0g‘𝐿)) ∈ Fin ↔ ((𝑢‘𝑖) supp (0g‘𝐿)) ∈ Fin))
223	222	cbvralvw 3223	. . . . . . . . . . . 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 9365	. . . . . . . . . . 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 9340	. . . . . . . . . 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 4788	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (𝑃 supp (0g‘𝐿)) → {𝑖} ⊆ (𝑃 supp (0g‘𝐿)))
230	229	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑃 supp (0g‘𝐿))) → {𝑖} ⊆ (𝑃 supp (0g‘𝐿)))
231	230	iunxpssiun1 32517	. . . . . . . . . 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 9283	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}) ∈ Fin)
234	21	ffnd 6717	. . . . . . . . . . . . . . . . . . . 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 6901	. . . . . . . . . . . . . . . . . . 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 3942	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ℎ ∈ (𝐻 ∖ (𝑃 supp (0g‘𝐿))))
241	235, 236, 237, 240	fvdifsupp 8178	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑃‘ℎ) = (0g‘𝐿))
242	241	oveq1d 7428	. . . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . . . . . . . . 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 32625	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → 𝑢:𝐻⟶(𝐹 ↑m 𝐵))
250	249, 238	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
251	245, 246, 250	elmaprd 32625	. . . . . . . . . . . . . . . . . . . 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 7085	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) ∈ 𝐹)
254	244, 253	sseldd 3964	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) ∈ (Base‘𝐿))
255	29, 19, 5, 243, 254	ringlzd 20261	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ ℎ ∈ (𝑃 supp (0g‘𝐿))) → ((0g‘𝐿)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
256	242, 255	eqtrd 2769	. . . . . . . . . . . . . . . 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 7448	. . . . . . . . . . . . . . . . . . . . . . 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 32625	. . . . . . . . . . . . . . . . . . . . . 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 7085	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ) ∈ (𝐹 ↑m 𝐵))
265	257, 258, 264	elmaprd 32625	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ):𝐵⟶𝐹)
266	265	ffnd 6717	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → (𝑢‘ℎ) Fn 𝐵)
267		fvexd 6901	. . . . . . . . . . . . . . . . . . 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 3942	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → 𝑐 ∈ (𝐵 ∖ ((𝑢‘ℎ) supp (0g‘𝐿))))
271	266, 257, 267, 270	fvdifsupp 8178	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑢‘ℎ)‘𝑐) = (0g‘𝐿))
272	271	oveq2d 7429	. . . . . . . . . . . . . . . . 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 20262	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)(0g‘𝐿)) = (0g‘𝐿))
276	272, 275	eqtrd 2769	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) ∧ ¬ 𝑐 ∈ ((𝑢‘ℎ) supp (0g‘𝐿))) → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)) = (0g‘𝐿))
277		df-br 5124	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ ↔ ⟨𝑐, ℎ⟩ ∈ ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
278		fveq2 6886	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ = 𝑖 → (𝑢‘ℎ) = (𝑢‘𝑖))
279	278	oveq1d 7428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑖 → ((𝑢‘ℎ) supp (0g‘𝐿)) = ((𝑢‘𝑖) supp (0g‘𝐿)))
280		sneq 4616	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ = 𝑖 → {ℎ} = {𝑖})
281	279, 280	xpeq12d 5696	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ = 𝑖 → (((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) = (((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
282	281	cbviunv 5020	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) = ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})
283	282	eleq2i 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑐, ℎ⟩ ∈ ∪ ℎ ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘ℎ) supp (0g‘𝐿)) × {ℎ}) ↔ ⟨𝑐, ℎ⟩ ∈ ∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖}))
284		opeliun2xp 5733	. . . . . . . . . . . . . . . . . . . 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 7428	. . . . . . . . . . . . . 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 20261	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → ((0g‘𝐿)(.r‘𝐿)𝑐) = (0g‘𝐿))
295	291, 294	eqtrd 2769	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) ∧ ℎ ∈ 𝐻) ∧ ¬ 𝑐∪ 𝑖 ∈ (𝑃 supp (0g‘𝐿))(((𝑢‘𝑖) supp (0g‘𝐿)) × {𝑖})ℎ) → (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐) = (0g‘𝐿))
296	295	an42ds 32398	. . . . . . . . . . . 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 19965	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))))
302	191, 195, 301	3eqtr4d 2779	. . . . . 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 20282	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) ∧ 𝑐 ∈ 𝐵) → (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))) = ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
305	304	mpteq2dva 5222	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐)))) = (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐)))
306	305	oveq2d 7429	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → (𝐿 Σg (𝑐 ∈ 𝐵 ↦ (𝐿 Σg (ℎ ∈ 𝐻 ↦ (((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))(.r‘𝐿)𝑐))))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))))
307	117, 302, 306	3eqtrd 2773	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → 𝑋 = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))))
308	51, 162	oveq12d 7431	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)))
309	308	cbvmptv 5235	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)))
310	182	oveq2d 7429	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏)) = ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))
311	310	mpteq2dv 5224	. . . . . . . . . 10 ⊢ (𝑏 = 𝑐 → (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))
312	309, 311	eqtrid 2781	. . . . . . . . 9 ⊢ (𝑏 = 𝑐 → (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))) = (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))
313	312	oveq2d 7429	. . . . . . . 8 ⊢ (𝑏 = 𝑐 → (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏)))) = (𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐)))))
314	313, 183	oveq12d 7431	. . . . . . 7 ⊢ (𝑏 = 𝑐 → ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏) = ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
315	314	cbvmptv 5235	. . . . . 6 ⊢ (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏)) = (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐))
316	315	oveq2i 7424	. . . . 5 ⊢ (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)((𝑢‘𝑓)‘𝑏))))(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑐 ∈ 𝐵 ↦ ((𝐿 Σg (ℎ ∈ 𝐻 ↦ ((𝑃‘ℎ)(.r‘𝐿)((𝑢‘ℎ)‘𝑐))))(.r‘𝐿)𝑐)))
317	307, 316	eqtr4di 2787	. . . 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 3607	. 2 ⊢ (((𝜑 ∧ 𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)) ∧ ∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))) → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))
320		breq1 5126	. . . 4 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑒 finSupp (0g‘𝐿) ↔ (𝑢‘𝑓) finSupp (0g‘𝐿)))
321		fveq1 6885	. . . . . . . 8 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑒‘𝑏) = ((𝑢‘𝑓)‘𝑏))
322	321	oveq1d 7428	. . . . . . 7 ⊢ (𝑒 = (𝑢‘𝑓) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) = (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))
323	322	mpteq2dv 5224	. . . . . 6 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)) = (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))
324	323	oveq2d 7429	. . . . 5 ⊢ (𝑒 = (𝑢‘𝑓) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))
325	324	eqeq2d 2745	. . . 4 ⊢ (𝑒 = (𝑢‘𝑓) → (𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))) ↔ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
326	320, 325	anbi12d 632	. . 3 ⊢ (𝑒 = (𝑢‘𝑓) → ((𝑒 finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))) ↔ ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏))))))
327		ovexd 7448	. . 3 ⊢ (𝜑 → (𝐹 ↑m 𝐵) ∈ V)
328		eqid 2734	. . . . . . . . . 10 ⊢ (LSpan‘((subringAlg ‘𝐽)‘𝐹)) = (LSpan‘((subringAlg ‘𝐽)‘𝐹))
329	139, 140, 328	lbssp 21047	. . . . . . . . 9 ⊢ (𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)) → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
330	3, 329	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = (Base‘((subringAlg ‘𝐽)‘𝐹)))
331	144, 66, 330	3eqtr4rd 2780	. . . . . . 7 ⊢ (𝜑 → ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) = 𝐻)
332	331	eleq2d 2819	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ ((LSpan‘((subringAlg ‘𝐽)‘𝐹))‘𝐵) ↔ 𝑓 ∈ 𝐻))
333		eqid 2734	. . . . . . 7 ⊢ (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹)))
334		eqid 2734	. . . . . . 7 ⊢ (Scalar‘((subringAlg ‘𝐽)‘𝐹)) = (Scalar‘((subringAlg ‘𝐽)‘𝐹))
335		eqid 2734	. . . . . . 7 ⊢ (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹)))
336		eqid 2734	. . . . . . 7 ⊢ ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))
337		sdrgsubrg 20761	. . . . . . . . 9 ⊢ (𝐹 ∈ (SubDRing‘𝐽) → 𝐹 ∈ (SubRing‘𝐽))
338	58, 337	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐽))
339		eqid 2734	. . . . . . . . 9 ⊢ ((subringAlg ‘𝐽)‘𝐹) = ((subringAlg ‘𝐽)‘𝐹)
340	339	sralmod 21157	. . . . . . . 8 ⊢ (𝐹 ∈ (SubRing‘𝐽) → ((subringAlg ‘𝐽)‘𝐹) ∈ LMod)
341	338, 340	syl 17	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ LMod)
342	328, 139, 333, 334, 335, 336, 341, 142	ellspds 33336	. . . . . 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 2734	. . . . . . . . . 10 ⊢ (𝐽 ↾s 𝐹) = (𝐽 ↾s 𝐹)
346	345, 59	ressbas2 17262	. . . . . . . . 9 ⊢ (𝐹 ⊆ (Base‘𝐽) → 𝐹 = (Base‘(𝐽 ↾s 𝐹)))
347	61, 346	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (Base‘(𝐽 ↾s 𝐹)))
348	143, 61	srasca 21148	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ↾s 𝐹) = (Scalar‘((subringAlg ‘𝐽)‘𝐹)))
349	348	fveq2d 6890	. . . . . . . 8 ⊢ (𝜑 → (Base‘(𝐽 ↾s 𝐹)) = (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))))
350	347, 349	eqtr2d 2770	. . . . . . 7 ⊢ (𝜑 → (Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = 𝐹)
351	350	oveq1d 7428	. . . . . 6 ⊢ (𝜑 → ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵) = (𝐹 ↑m 𝐵))
352		sdrgsubrg 20761	. . . . . . . . . . . 12 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐻 ∈ (SubRing‘𝐿))
353	11, 352	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ (SubRing‘𝐿))
354		subrgsubg 20546	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubRing‘𝐿) → 𝐻 ∈ (SubGrp‘𝐿))
355	64, 5	subg0 19120	. . . . . . . . . . 11 ⊢ (𝐻 ∈ (SubGrp‘𝐿) → (0g‘𝐿) = (0g‘𝐽))
356	353, 354, 355	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝐿) = (0g‘𝐽))
357	64	sdrgdrng 20760	. . . . . . . . . . . . . . 15 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → 𝐽 ∈ DivRing)
358	11, 357	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ DivRing)
359	358	drngringd 20706	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ Ring)
360	359	ringcmnd 20250	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ CMnd)
361	360	cmnmndd 19791	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ Mnd)
362		subrgsubg 20546	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubRing‘𝐽) → 𝐹 ∈ (SubGrp‘𝐽))
363		eqid 2734	. . . . . . . . . . . . 13 ⊢ (0g‘𝐽) = (0g‘𝐽)
364	363	subg0cl 19122	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubGrp‘𝐽) → (0g‘𝐽) ∈ 𝐹)
365	338, 362, 364	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝐽) ∈ 𝐹)
366	345, 59, 363	ress0g 18745	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Mnd ∧ (0g‘𝐽) ∈ 𝐹 ∧ 𝐹 ⊆ (Base‘𝐽)) → (0g‘𝐽) = (0g‘(𝐽 ↾s 𝐹)))
367	361, 365, 61, 366	syl3anc 1372	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝐽) = (0g‘(𝐽 ↾s 𝐹)))
368	348	fveq2d 6890	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘(𝐽 ↾s 𝐹)) = (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))))
369	356, 367, 368	3eqtrrd 2774	. . . . . . . . 9 ⊢ (𝜑 → (0g‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) = (0g‘𝐿))
370	369	breq2d 5135	. . . . . . . 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 19136	. . . . . . . . . . . 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 17324	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ (SubDRing‘𝐿) → (.r‘𝐿) = (.r‘𝐽))
377	11, 376	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐿) = (.r‘𝐽))
378	143, 61	sravsca 21150	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (.r‘𝐽) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
379	377, 378	eqtrd 2769	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
380	379	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (.r‘𝐿) = ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)))
381	380	oveqd 7430	. . . . . . . . . . . 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 2819	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵) ↔ 𝑒 ∈ (𝐹 ↑m 𝐵)))
386	385	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝑒 ∈ (𝐹 ↑m 𝐵))
387	372, 384, 386	elmaprd 32625	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝑒:𝐵⟶𝐹)
388	387	ffvelcdmda 7084	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (𝑒‘𝑏) ∈ 𝐹)
389	383, 388	sseldd 3964	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → (𝑒‘𝑏) ∈ 𝐻)
390	146	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → 𝐵 ⊆ 𝐻)
391	390	sselda 3963	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐻)
392	19, 382, 389, 391	subrgmcld 33181	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)(.r‘𝐿)𝑏) ∈ 𝐻)
393	381, 392	eqeltrrd 2834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) ∧ 𝑏 ∈ 𝐵) → ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏) ∈ 𝐻)
394	393	fmpttd 7115	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)):𝐵⟶𝐻)
395	372, 375, 394, 64	gsumsubm 18818	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐽 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))))
396	377, 378	eqtr2d 2770	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = (.r‘𝐿))
397	396	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹)) = (.r‘𝐿))
398	397	oveqd 7430	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏) = ((𝑒‘𝑏)(.r‘𝐿)𝑏))
399	398	mpteq2dv 5224	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)) = (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏)))
400	399	oveq2d 7429	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))
401	3	mptexd 7226	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏)) ∈ V)
402		fvexd 6901	. . . . . . . . . . 11 ⊢ (𝜑 → ((subringAlg ‘𝐽)‘𝐹) ∈ V)
403	339, 401, 358, 402, 61	gsumsra 32994	. . . . . . . . . 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 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐽)‘𝐹))) ↑m 𝐵)) → (((subringAlg ‘𝐽)‘𝐹) Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)( ·𝑠 ‘((subringAlg ‘𝐽)‘𝐹))𝑏))) = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑒‘𝑏)(.r‘𝐿)𝑏))))
406	405	eqeq2d 2745	. . . . . . 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 3316	. . . . 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 32571	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ((𝐹 ↑m 𝐵) ↑m 𝐻)∀𝑓 ∈ 𝐻 ((𝑢‘𝑓) finSupp (0g‘𝐿) ∧ 𝑓 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ (((𝑢‘𝑓)‘𝑏)(.r‘𝐿)𝑏)))))
412	319, 411	r19.29a 3149	1 ⊢ (𝜑 → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1539   ∈ wcel 2107  ∀wral 3050  ∃wrex 3059  Vcvv 3463   ∪ cun 3929   ⊆ wss 3931  {csn 4606  ⟨cop 4612  ∪ ciun 4971   class class class wbr 5123   ↦ cmpt 5205   × cxp 5663   Fn wfn 6536  ⟶wf 6537  ‘cfv 6541  (class class class)co 7413   supp csupp 8167   ↑_m cmap 8848  Fincfn 8967   finSupp cfsupp 9383  Basecbs 17230   ↾_s cress 17253  ._rcmulr 17275  Scalarcsca 17277   ·_𝑠 cvsca 17278  0_gc0g 17456   Σ_g cgsu 17457  Mndcmnd 18717  SubMndcsubmnd 18765  SubGrpcsubg 19108  CMndccmn 19767  Ringcrg 20199  SubRingcsubrg 20538  RingSpancrgspn 20579  DivRingcdr 20698  Fieldcfield 20699  SubDRingcsdrg 20756  LModclmod 20827  LSpanclspn 20938  LBasisclbs 21042  subringAlg csra 21139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-reg 9614  ax-inf2 9663  ax-ac2 10485  ax-cnex 11193  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213  ax-pre-mulgt0 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-uni 4888  df-int 4927  df-iun 4973  df-iin 4974  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-se 5618  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-om 7870  df-1st 7996  df-2nd 7997  df-supp 8168  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-er 8727  df-map 8850  df-ixp 8920  df-en 8968  df-dom 8969  df-sdom 8970  df-fin 8971  df-fsupp 9384  df-sup 9464  df-oi 9532  df-r1 9786  df-rank 9787  df-card 9961  df-ac 10138  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-sub 11476  df-neg 11477  df-nn 12249  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315  df-7 12316  df-8 12317  df-9 12318  df-n0 12510  df-z 12597  df-dec 12717  df-uz 12861  df-fz 13530  df-fzo 13677  df-seq 14025  df-hash 14353  df-struct 17167  df-sets 17184  df-slot 17202  df-ndx 17214  df-base 17231  df-ress 17254  df-plusg 17287  df-mulr 17288  df-sca 17290  df-vsca 17291  df-ip 17292  df-tset 17293  df-ple 17294  df-ds 17296  df-hom 17298  df-cco 17299  df-0g 17458  df-gsum 17459  df-prds 17464  df-pws 17466  df-mre 17601  df-mrc 17602  df-acs 17604  df-mgm 18623  df-sgrp 18702  df-mnd 18718  df-mhm 18766  df-submnd 18767  df-grp 18924  df-minusg 18925  df-sbg 18926  df-mulg 19056  df-subg 19111  df-ghm 19201  df-cntz 19305  df-cmn 19769  df-abl 19770  df-mgp 20107  df-rng 20119  df-ur 20148  df-ring 20201  df-nzr 20482  df-subrng 20515  df-subrg 20539  df-drng 20700  df-field 20701  df-sdrg 20757  df-lmod 20829  df-lss 20899  df-lsp 20939  df-lmhm 20990  df-lbs 21043  df-sra 21141  df-rgmod 21142  df-dsmm 21707  df-frlm 21722  df-uvc 21758

This theorem is referenced by:  fldextrspunlsp  33666