Theorem mplvrpmrhm 33691

Description: The action of permuting variables in a multivariate polynomial is a ring homomorphism. (Contributed by Thierry Arnoux, 15-Jan-2026.)

Hypotheses

Ref	Expression
mplvrpmga.1	⊢ 𝑆 = (SymGrp‘𝐼)
mplvrpmga.2	⊢ 𝑃 = (Base‘𝑆)
mplvrpmga.3	⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))
mplvrpmga.4	⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))
mplvrpmga.5	⊢ (𝜑 → 𝐼 ∈ 𝑉)
mplvrpmmhm.f	⊢ 𝐹 = (𝑓 ∈ 𝑀 ↦ (𝐷𝐴𝑓))
mplvrpmmhm.w	⊢ 𝑊 = (𝐼 mPoly 𝑅)
mplvrpmmhm.1	⊢ (𝜑 → 𝑅 ∈ Ring)
mplvrpmmhm.2	⊢ (𝜑 → 𝐷 ∈ 𝑃)

Assertion

Ref	Expression
mplvrpmrhm	⊢ (𝜑 → 𝐹 ∈ (𝑊 RingHom 𝑊))

Distinct variable groups:   𝐴,𝑑,𝑓,𝑥   𝐼,𝑑,𝑓,ℎ,𝑥   𝑀,𝑑,𝑓,𝑥   𝑃,𝑑,𝑓,𝑥   𝑥,𝑅   𝜑,𝑑,𝑓,𝑥   𝐷,𝑑,𝑓,ℎ,𝑥   𝑥,𝐹   𝑊,𝑑,𝑓,𝑥   𝑅,𝑑,𝑓,ℎ   𝑥,𝑉

Allowed substitution hints:   𝜑(ℎ)   𝐴(ℎ)   𝑃(ℎ)   𝑆(𝑥,𝑓,ℎ,𝑑)   𝐹(𝑓,ℎ,𝑑)   𝑀(ℎ)   𝑉(𝑓,ℎ,𝑑)   𝑊(ℎ)

Proof of Theorem mplvrpmrhm

Dummy variables 𝑎 𝑦 𝑖 𝑗 𝑡 𝑧 𝑣 𝑛 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mplvrpmga.3	. . 3 ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))
2		mplvrpmmhm.w	. . . 4 ⊢ 𝑊 = (𝐼 mPoly 𝑅)
3	2	fveq2i 6843	. . 3 ⊢ (Base‘𝑊) = (Base‘(𝐼 mPoly 𝑅))
4	1, 3	eqtr4i 2762	. 2 ⊢ 𝑀 = (Base‘𝑊)
5		eqid 2736	. 2 ⊢ (1r‘𝑊) = (1r‘𝑊)
6		eqid 2736	. 2 ⊢ (.r‘𝑊) = (.r‘𝑊)
7		mplvrpmga.5	. . 3 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
8		mplvrpmmhm.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ Ring)
9	2, 7, 8	mplringd 22001	. 2 ⊢ (𝜑 → 𝑊 ∈ Ring)
10		mplvrpmmhm.f	. . 3 ⊢ 𝐹 = (𝑓 ∈ 𝑀 ↦ (𝐷𝐴𝑓))
11		oveq2 7375	. . . 4 ⊢ (𝑓 = (1r‘𝑊) → (𝐷𝐴𝑓) = (𝐷𝐴(1r‘𝑊)))
12		mplvrpmga.4	. . . . . . 7 ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))
13	12	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
14		simpr 484	. . . . . . . . . 10 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊)) → 𝑓 = (1r‘𝑊))
15		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊)) → 𝑑 = 𝐷)
16	15	coeq2d 5817	. . . . . . . . . 10 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊)) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
17	14, 16	fveq12d 6847	. . . . . . . . 9 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊)) → (𝑓‘(𝑥 ∘ 𝑑)) = ((1r‘𝑊)‘(𝑥 ∘ 𝐷)))
18	17	ad2antlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = ((1r‘𝑊)‘(𝑥 ∘ 𝐷)))
19		eqid 2736	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
20	19	psrbasfsupp 33672	. . . . . . . . . . . 12 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
21		eqid 2736	. . . . . . . . . . . 12 ⊢ (0g‘𝑅) = (0g‘𝑅)
22		eqid 2736	. . . . . . . . . . . 12 ⊢ (1r‘𝑅) = (1r‘𝑅)
23	2, 20, 21, 22, 5, 7, 8	mpl1 21990	. . . . . . . . . . 11 ⊢ (𝜑 → (1r‘𝑊) = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑦 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))))
24	23	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (1r‘𝑊) = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑦 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))))
25		eqeq1 2740	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥 ∘ 𝐷) → (𝑦 = (𝐼 × {0}) ↔ (𝑥 ∘ 𝐷) = (𝐼 × {0})))
26		mplvrpmmhm.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
27	26	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐷 ∈ 𝑃)
28		mplvrpmga.1	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (SymGrp‘𝐼)
29		mplvrpmga.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑃 = (Base‘𝑆)
30	28, 29	symgbasf1o 19350	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ 𝑃 → 𝐷:𝐼–1-1-onto→𝐼)
31		f1ococnv2 6807	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷:𝐼–1-1-onto→𝐼 → (𝐷 ∘ ◡𝐷) = ( I ↾ 𝐼))
32	27, 30, 31	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝐷 ∘ ◡𝐷) = ( I ↾ 𝐼))
33	32	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝐷 ∘ ◡𝐷) = ( I ↾ 𝐼))
34	33	coeq2d 5817	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ (𝐷 ∘ ◡𝐷)) = (𝑥 ∘ ( I ↾ 𝐼)))
35		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = (𝐼 × {0}))
36	35	coeq1d 5816	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝑥 ∘ 𝐷) ∘ ◡𝐷) = ((𝐼 × {0}) ∘ ◡𝐷))
37		coass 6230	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∘ 𝐷) ∘ ◡𝐷) = (𝑥 ∘ (𝐷 ∘ ◡𝐷))
38	37	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝑥 ∘ 𝐷) ∘ ◡𝐷) = (𝑥 ∘ (𝐷 ∘ ◡𝐷)))
39	26, 30	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷:𝐼–1-1-onto→𝐼)
40		f1ocnv 6792	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷:𝐼–1-1-onto→𝐼 → ◡𝐷:𝐼–1-1-onto→𝐼)
41		f1of 6780	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝐷:𝐼–1-1-onto→𝐼 → ◡𝐷:𝐼⟶𝐼)
42	39, 40, 41	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ◡𝐷:𝐼⟶𝐼)
43		0nn0 12452	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℕ0
44	43	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℕ0)
45	42, 44	constcof 32694	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐼 × {0}) ∘ ◡𝐷) = (𝐼 × {0}))
46	45	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝐼 × {0}) ∘ ◡𝐷) = (𝐼 × {0}))
47	36, 38, 46	3eqtr3d 2779	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ (𝐷 ∘ ◡𝐷)) = (𝐼 × {0}))
48	7	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
49		nn0ex 12443	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 ∈ V
50	49	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ℕ0 ∈ V)
51		ssrab2 4020	. . . . . . . . . . . . . . . . . 18 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐼)
52		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
53	51, 52	sselid 3919	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ (ℕ0 ↑m 𝐼))
54	48, 50, 53	elmaprd 32753	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥:𝐼⟶ℕ0)
55		fcoi1 6714	. . . . . . . . . . . . . . . 16 ⊢ (𝑥:𝐼⟶ℕ0 → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
56	54, 55	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
57	56	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
58	34, 47, 57	3eqtr3rd 2780	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → 𝑥 = (𝐼 × {0}))
59		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → 𝑥 = (𝐼 × {0}))
60	59	coeq1d 5816	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = ((𝐼 × {0}) ∘ 𝐷))
61		f1of 6780	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷:𝐼–1-1-onto→𝐼 → 𝐷:𝐼⟶𝐼)
62	26, 30, 61	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷:𝐼⟶𝐼)
63	62, 44	constcof 32694	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐼 × {0}) ∘ 𝐷) = (𝐼 × {0}))
64	63	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → ((𝐼 × {0}) ∘ 𝐷) = (𝐼 × {0}))
65	60, 64	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = (𝐼 × {0}))
66	58, 65	impbida 801	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ((𝑥 ∘ 𝐷) = (𝐼 × {0}) ↔ 𝑥 = (𝐼 × {0})))
67	25, 66	sylan9bbr 510	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 = (𝑥 ∘ 𝐷)) → (𝑦 = (𝐼 × {0}) ↔ 𝑥 = (𝐼 × {0})))
68	67	ifbid 4490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 = (𝑥 ∘ 𝐷)) → if(𝑦 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)) = if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)))
69	28, 29, 48, 27, 52	mplvrpmlem 33687	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
70		fvexd 6855	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (1r‘𝑅) ∈ V)
71		fvexd 6855	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (0g‘𝑅) ∈ V)
72	70, 71	ifcld 4513	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)) ∈ V)
73	24, 68, 69, 72	fvmptd 6955	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ((1r‘𝑊)‘(𝑥 ∘ 𝐷)) = if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)))
74	73	adantlr 716	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ((1r‘𝑊)‘(𝑥 ∘ 𝐷)) = if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)))
75	18, 74	eqtrd 2771	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)))
76	75	mpteq2dva 5178	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊))) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))))
77	4, 5, 9	ringidcld 20247	. . . . . 6 ⊢ (𝜑 → (1r‘𝑊) ∈ 𝑀)
78		ovex 7400	. . . . . . . . 9 ⊢ (ℕ0 ↑m 𝐼) ∈ V
79	78	rabex 5280	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V
80	79	a1i 11	. . . . . . 7 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V)
81	80	mptexd 7179	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) ∈ V)
82	13, 76, 26, 77, 81	ovmpod 7519	. . . . 5 ⊢ (𝜑 → (𝐷𝐴(1r‘𝑊)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))))
83		eqid 2736	. . . . . 6 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
84		eqid 2736	. . . . . 6 ⊢ (1r‘(𝐼 mPwSer 𝑅)) = (1r‘(𝐼 mPwSer 𝑅))
85	83, 7, 8, 20, 21, 22, 84	psr1 21949	. . . . 5 ⊢ (𝜑 → (1r‘(𝐼 mPwSer 𝑅)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))))
86	83, 2, 4, 7, 8	mplsubrg 21983	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (SubRing‘(𝐼 mPwSer 𝑅)))
87	2, 83, 4	mplval2 21974	. . . . . . 7 ⊢ 𝑊 = ((𝐼 mPwSer 𝑅) ↾s 𝑀)
88	87, 84	subrg1 20559	. . . . . 6 ⊢ (𝑀 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → (1r‘(𝐼 mPwSer 𝑅)) = (1r‘𝑊))
89	86, 88	syl 17	. . . . 5 ⊢ (𝜑 → (1r‘(𝐼 mPwSer 𝑅)) = (1r‘𝑊))
90	82, 85, 89	3eqtr2d 2777	. . . 4 ⊢ (𝜑 → (𝐷𝐴(1r‘𝑊)) = (1r‘𝑊))
91	11, 90	sylan9eqr 2793	. . 3 ⊢ ((𝜑 ∧ 𝑓 = (1r‘𝑊)) → (𝐷𝐴𝑓) = (1r‘𝑊))
92	10, 91, 77, 77	fvmptd2 6956	. 2 ⊢ (𝜑 → (𝐹‘(1r‘𝑊)) = (1r‘𝑊))
93		nfcv 2898	. . . . . . 7 ⊢ Ⅎ𝑣((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
94		eqid 2736	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘𝑅)
95		fveq2 6840	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → (𝑖‘𝑣) = (𝑖‘(𝑦 ∘ 𝐷)))
96		oveq2 7375	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → ((𝑥 ∘ 𝐷) ∘f − 𝑣) = ((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))
97	96	fveq2d 6844	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → (𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
98	95, 97	oveq12d 7385	. . . . . . 7 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))) = ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))))
99	8	ringcmnd 20265	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ CMnd)
100	99	ad3antrrr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑅 ∈ CMnd)
101	79	rabex 5280	. . . . . . . 8 ⊢ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ∈ V
102	101	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ∈ V)
103		eqid 2736	. . . . . . . . . . . 12 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
104	2, 83, 4, 103	mplbasss 21975	. . . . . . . . . . . . . 14 ⊢ 𝑀 ⊆ (Base‘(𝐼 mPwSer 𝑅))
105		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑖 ∈ 𝑀)
106	104, 105	sselid 3919	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑖 ∈ (Base‘(𝐼 mPwSer 𝑅)))
107	106	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 ∈ (Base‘(𝐼 mPwSer 𝑅)))
108	83, 94, 20, 103, 107	psrelbas 21914	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖:{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
109	108	feqmptd 6908	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 = (𝑣 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘𝑣)))
110	105	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 ∈ 𝑀)
111	2, 4, 21, 110	mplelsfi 21973	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 finSupp (0g‘𝑅))
112	109, 111	eqbrtrrd 5109	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘𝑣)) finSupp (0g‘𝑅))
113		ssrab2 4020	. . . . . . . . . 10 ⊢ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ⊆ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
114	113	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ⊆ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
115		fvexd 6855	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (0g‘𝑅) ∈ V)
116	112, 114, 115	fmptssfisupp 9307	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ (𝑖‘𝑣)) finSupp (0g‘𝑅))
117		eqid 2736	. . . . . . . . 9 ⊢ (.r‘𝑅) = (.r‘𝑅)
118	8	ad4antr 733	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑛 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring)
119		simpr 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑛 ∈ (Base‘𝑅)) → 𝑛 ∈ (Base‘𝑅))
120	94, 117, 21, 118, 119	ringlzd 20276	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑛 ∈ (Base‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)𝑛) = (0g‘𝑅))
121	108	adantr 480	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑖:{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
122		elrabi 3630	. . . . . . . . . 10 ⊢ (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} → 𝑣 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
123	122	adantl 481	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
124	121, 123	ffvelcdmd 7037	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑖‘𝑣) ∈ (Base‘𝑅))
125		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑗 ∈ 𝑀)
126	104, 125	sselid 3919	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑗 ∈ (Base‘(𝐼 mPwSer 𝑅)))
127	126	ad2antrr 727	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑗 ∈ (Base‘(𝐼 mPwSer 𝑅)))
128	83, 94, 20, 103, 127	psrelbas 21914	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑗:{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
129	69	ad5ant14 758	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ 𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
130	7	ad4antr 733	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝐼 ∈ 𝑉)
131	49	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ℕ0 ∈ V)
132	51, 123	sselid 3919	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∈ (ℕ0 ↑m 𝐼))
133	130, 131, 132	elmaprd 32753	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣:𝐼⟶ℕ0)
134		breq1 5088	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑤 ∘r ≤ (𝑥 ∘ 𝐷) ↔ 𝑣 ∘r ≤ (𝑥 ∘ 𝐷)))
135		simpr 484	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)})
136	134, 135	elrabrd 32568	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∘r ≤ (𝑥 ∘ 𝐷))
137	20	psrbagcon 21905	. . . . . . . . . . 11 ⊢ (((𝑥 ∘ 𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∧ 𝑣:𝐼⟶ℕ0 ∧ 𝑣 ∘r ≤ (𝑥 ∘ 𝐷)) → (((𝑥 ∘ 𝐷) ∘f − 𝑣) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∧ ((𝑥 ∘ 𝐷) ∘f − 𝑣) ∘r ≤ (𝑥 ∘ 𝐷)))
138	129, 133, 136, 137	syl3anc 1374	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (((𝑥 ∘ 𝐷) ∘f − 𝑣) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∧ ((𝑥 ∘ 𝐷) ∘f − 𝑣) ∘r ≤ (𝑥 ∘ 𝐷)))
139	138	simpld 494	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ((𝑥 ∘ 𝐷) ∘f − 𝑣) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
140	128, 139	ffvelcdmd 7037	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)) ∈ (Base‘𝑅))
141	116, 120, 124, 140, 115	fsuppssov1 9297	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))) finSupp (0g‘𝑅))
142		ssidd 3945	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (Base‘𝑅) ⊆ (Base‘𝑅))
143	8	ad4antr 733	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑅 ∈ Ring)
144	94, 117, 143, 124, 140	ringcld 20241	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))) ∈ (Base‘𝑅))
145		breq1 5088	. . . . . . . 8 ⊢ (𝑤 = (𝑦 ∘ 𝐷) → (𝑤 ∘r ≤ (𝑥 ∘ 𝐷) ↔ (𝑦 ∘ 𝐷) ∘r ≤ (𝑥 ∘ 𝐷)))
146	7	ad4antr 733	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝐼 ∈ 𝑉)
147	26	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐷 ∈ 𝑃)
148	147	ad2antrr 727	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝐷 ∈ 𝑃)
149		ssrab2 4020	. . . . . . . . . . 11 ⊢ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ⊆ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
150		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥})
151	149, 150	sselid 3919	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
152	151	adantlr 716	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
153	28, 29, 146, 148, 152	mplvrpmlem 33687	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
154	49	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ℕ0 ∈ V)
155	51	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐼))
156	149, 155	sstrid 3933	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ⊆ (ℕ0 ↑m 𝐼))
157	156	sselda 3921	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦 ∈ (ℕ0 ↑m 𝐼))
158	146, 154, 157	elmaprd 32753	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦:𝐼⟶ℕ0)
159	158	ffnd 6669	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦 Fn 𝐼)
160	54	ad4ant14 753	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥:𝐼⟶ℕ0)
161	160	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑥:𝐼⟶ℕ0)
162	161	ffnd 6669	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑥 Fn 𝐼)
163	62	ad4antr 733	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝐷:𝐼⟶𝐼)
164		breq1 5088	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → (𝑧 ∘r ≤ 𝑥 ↔ 𝑦 ∘r ≤ 𝑥))
165		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥})
166	164, 165	elrabrd 32568	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦 ∘r ≤ 𝑥)
167	159, 162, 163, 146, 146, 166	ofrco 32683	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∘r ≤ (𝑥 ∘ 𝐷))
168	145, 153, 167	elrabd 3636	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)})
169		breq1 5088	. . . . . . . . 9 ⊢ (𝑧 = (𝑣 ∘ ◡𝐷) → (𝑧 ∘r ≤ 𝑥 ↔ (𝑣 ∘ ◡𝐷) ∘r ≤ 𝑥))
170		breq1 5088	. . . . . . . . . 10 ⊢ (ℎ = (𝑣 ∘ ◡𝐷) → (ℎ finSupp 0 ↔ (𝑣 ∘ ◡𝐷) finSupp 0))
171	42	ad4antr 733	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ◡𝐷:𝐼⟶𝐼)
172	133, 171	fcod 6693	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷):𝐼⟶ℕ0)
173	131, 130, 172	elmapdd 8788	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) ∈ (ℕ0 ↑m 𝐼))
174		breq1 5088	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑣 → (ℎ finSupp 0 ↔ 𝑣 finSupp 0))
175	174, 123	elrabrd 32568	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 finSupp 0)
176	39	ad4antr 733	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝐷:𝐼–1-1-onto→𝐼)
177		f1of1 6779	. . . . . . . . . . . 12 ⊢ (◡𝐷:𝐼–1-1-onto→𝐼 → ◡𝐷:𝐼–1-1→𝐼)
178	176, 40, 177	3syl 18	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ◡𝐷:𝐼–1-1→𝐼)
179	43	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 0 ∈ ℕ0)
180	175, 178, 179, 123	fsuppco 9315	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) finSupp 0)
181	170, 173, 180	elrabd 3636	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
182	133	ffnd 6669	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 Fn 𝐼)
183	160	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑥:𝐼⟶ℕ0)
184	183	ffnd 6669	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑥 Fn 𝐼)
185	62	ad4antr 733	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝐷:𝐼⟶𝐼)
186		fnfco 6705	. . . . . . . . . . . 12 ⊢ ((𝑥 Fn 𝐼 ∧ 𝐷:𝐼⟶𝐼) → (𝑥 ∘ 𝐷) Fn 𝐼)
187	184, 185, 186	syl2anc 585	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ 𝐷) Fn 𝐼)
188	182, 187, 171, 130, 130, 136	ofrco 32683	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) ∘r ≤ ((𝑥 ∘ 𝐷) ∘ ◡𝐷))
189	176, 31	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝐷 ∘ ◡𝐷) = ( I ↾ 𝐼))
190	189	coeq2d 5817	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ (𝐷 ∘ ◡𝐷)) = (𝑥 ∘ ( I ↾ 𝐼)))
191	183, 55	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
192	190, 191	eqtrd 2771	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ (𝐷 ∘ ◡𝐷)) = 𝑥)
193	37, 192	eqtrid 2783	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ((𝑥 ∘ 𝐷) ∘ ◡𝐷) = 𝑥)
194	188, 193	breqtrd 5111	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) ∘r ≤ 𝑥)
195	169, 181, 194	elrabd 3636	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥})
196	133	adantr 480	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑣:𝐼⟶ℕ0)
197	158	adantlr 716	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦:𝐼⟶ℕ0)
198	39	ad5antr 735	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝐷:𝐼–1-1-onto→𝐼)
199	196, 197, 198	cocnvf1o 32802	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑣 = (𝑦 ∘ 𝐷) ↔ 𝑦 = (𝑣 ∘ ◡𝐷)))
200	195, 199	reu6dv 32542	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ∃!𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}𝑣 = (𝑦 ∘ 𝐷))
201	93, 94, 21, 98, 100, 102, 141, 142, 144, 168, 200	gsummptfsf1o 33121	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))) = (𝑅 Σg (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))))))
202		coeq1 5812	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑦 → (𝑡 ∘ 𝐷) = (𝑦 ∘ 𝐷))
203	202	fveq2d 6844	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → (𝑖‘(𝑡 ∘ 𝐷)) = (𝑖‘(𝑦 ∘ 𝐷)))
204		oveq2 7375	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑖 → (𝐷𝐴𝑓) = (𝐷𝐴𝑖))
205	105	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑖 ∈ 𝑀)
206		ovexd 7402	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐷𝐴𝑖) ∈ V)
207	10, 204, 205, 206	fvmptd3 6971	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐹‘𝑖) = (𝐷𝐴𝑖))
208	12	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
209		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → 𝑓 = 𝑖)
210		coeq2 5813	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝐷 → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
211	210	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
212	209, 211	fveq12d 6847	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑖‘(𝑥 ∘ 𝐷)))
213	212	mpteq2dv 5179	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑥 ∘ 𝐷))))
214		coeq1 5812	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (𝑥 ∘ 𝐷) = (𝑡 ∘ 𝐷))
215	214	fveq2d 6844	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (𝑖‘(𝑥 ∘ 𝐷)) = (𝑖‘(𝑡 ∘ 𝐷)))
216	215	cbvmptv 5189	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑥 ∘ 𝐷))) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷)))
217	213, 216	eqtrdi 2787	. . . . . . . . . . . . . 14 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
218	217	adantl 481	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ (𝑑 = 𝐷 ∧ 𝑓 = 𝑖)) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
219	147	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝐷 ∈ 𝑃)
220	79	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V)
221	220	mptexd 7179	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))) ∈ V)
222	208, 218, 219, 205, 221	ovmpod 7519	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐷𝐴𝑖) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
223	207, 222	eqtrd 2771	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐹‘𝑖) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
224		fvexd 6855	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑖‘(𝑦 ∘ 𝐷)) ∈ V)
225	203, 223, 151, 224	fvmptd4 6972	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ((𝐹‘𝑖)‘𝑦) = (𝑖‘(𝑦 ∘ 𝐷)))
226	225	adantlr 716	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ((𝐹‘𝑖)‘𝑦) = (𝑖‘(𝑦 ∘ 𝐷)))
227		oveq2 7375	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑗 → (𝐷𝐴𝑓) = (𝐷𝐴𝑗))
228		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → 𝑓 = 𝑗)
229	210	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
230	228, 229	fveq12d 6847	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑗‘(𝑥 ∘ 𝐷)))
231	230	mpteq2dv 5179	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑥 ∘ 𝐷))))
232	214	fveq2d 6844	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (𝑗‘(𝑥 ∘ 𝐷)) = (𝑗‘(𝑡 ∘ 𝐷)))
233	232	cbvmptv 5189	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑥 ∘ 𝐷))) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷)))
234	231, 233	eqtrdi 2787	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
235	234	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ (𝑑 = 𝐷 ∧ 𝑓 = 𝑗)) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
236		simplr 769	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑗 ∈ 𝑀)
237	220	mptexd 7179	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))) ∈ V)
238	208, 235, 219, 236, 237	ovmpod 7519	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐷𝐴𝑗) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
239	227, 238	sylan9eqr 2793	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑓 = 𝑗) → (𝐷𝐴𝑓) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
240	239	adantllr 720	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑓 = 𝑗) → (𝐷𝐴𝑓) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
241	125	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑗 ∈ 𝑀)
242	79	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V)
243	242	mptexd 7179	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))) ∈ V)
244	10, 240, 241, 243	fvmptd2 6956	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐹‘𝑗) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
245		coeq1 5812	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑥 ∘f − 𝑦) → (𝑡 ∘ 𝐷) = ((𝑥 ∘f − 𝑦) ∘ 𝐷))
246	245	fveq2d 6844	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑥 ∘f − 𝑦) → (𝑗‘(𝑡 ∘ 𝐷)) = (𝑗‘((𝑥 ∘f − 𝑦) ∘ 𝐷)))
247	246	adantl 481	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → (𝑗‘(𝑡 ∘ 𝐷)) = (𝑗‘((𝑥 ∘f − 𝑦) ∘ 𝐷)))
248	160	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → 𝑥:𝐼⟶ℕ0)
249	248	ffnd 6669	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → 𝑥 Fn 𝐼)
250	7	ad5antr 735	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → 𝐼 ∈ 𝑉)
251	49	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → ℕ0 ∈ V)
252	157	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → 𝑦 ∈ (ℕ0 ↑m 𝐼))
253	250, 251, 252	elmaprd 32753	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → 𝑦:𝐼⟶ℕ0)
254	253	ffnd 6669	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → 𝑦 Fn 𝐼)
255	62	ad5antr 735	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → 𝐷:𝐼⟶𝐼)
256		inidm 4167	. . . . . . . . . . . . 13 ⊢ (𝐼 ∩ 𝐼) = 𝐼
257	249, 254, 255, 250, 250, 250, 256	ofco 7656	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → ((𝑥 ∘f − 𝑦) ∘ 𝐷) = ((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))
258	257	fveq2d 6844	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → (𝑗‘((𝑥 ∘f − 𝑦) ∘ 𝐷)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
259	247, 258	eqtrd 2771	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → (𝑗‘(𝑡 ∘ 𝐷)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
260		breq1 5088	. . . . . . . . . . 11 ⊢ (ℎ = (𝑥 ∘f − 𝑦) → (ℎ finSupp 0 ↔ (𝑥 ∘f − 𝑦) finSupp 0))
261	162, 159, 146, 146, 256	offn 7644	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦) Fn 𝐼)
262	162	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑥 Fn 𝐼)
263	159	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑦 Fn 𝐼)
264	146	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝐼 ∈ 𝑉)
265		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑎 ∈ 𝐼)
266		fnfvof 7648	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 Fn 𝐼 ∧ 𝑦 Fn 𝐼) ∧ (𝐼 ∈ 𝑉 ∧ 𝑎 ∈ 𝐼)) → ((𝑥 ∘f − 𝑦)‘𝑎) = ((𝑥‘𝑎) − (𝑦‘𝑎)))
267	262, 263, 264, 265, 266	syl22anc 839	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → ((𝑥 ∘f − 𝑦)‘𝑎) = ((𝑥‘𝑎) − (𝑦‘𝑎)))
268	158	ffvelcdmda 7036	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑦‘𝑎) ∈ ℕ0)
269	161	ffvelcdmda 7036	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑥‘𝑎) ∈ ℕ0)
270		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥})
271	164, 270	elrabrd 32568	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑦 ∘r ≤ 𝑥)
272	263, 262, 264, 271, 265	fnfvor 32682	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑦‘𝑎) ≤ (𝑥‘𝑎))
273		nn0sub 12487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦‘𝑎) ∈ ℕ0 ∧ (𝑥‘𝑎) ∈ ℕ0) → ((𝑦‘𝑎) ≤ (𝑥‘𝑎) ↔ ((𝑥‘𝑎) − (𝑦‘𝑎)) ∈ ℕ0))
274	273	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦‘𝑎) ∈ ℕ0 ∧ (𝑥‘𝑎) ∈ ℕ0) ∧ (𝑦‘𝑎) ≤ (𝑥‘𝑎)) → ((𝑥‘𝑎) − (𝑦‘𝑎)) ∈ ℕ0)
275	268, 269, 272, 274	syl21anc 838	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → ((𝑥‘𝑎) − (𝑦‘𝑎)) ∈ ℕ0)
276	267, 275	eqeltrd 2836	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → ((𝑥 ∘f − 𝑦)‘𝑎) ∈ ℕ0)
277	276	ralrimiva 3129	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ∀𝑎 ∈ 𝐼 ((𝑥 ∘f − 𝑦)‘𝑎) ∈ ℕ0)
278		ffnfv 7071	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∘f − 𝑦):𝐼⟶ℕ0 ↔ ((𝑥 ∘f − 𝑦) Fn 𝐼 ∧ ∀𝑎 ∈ 𝐼 ((𝑥 ∘f − 𝑦)‘𝑎) ∈ ℕ0))
279	261, 277, 278	sylanbrc 584	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦):𝐼⟶ℕ0)
280	154, 146, 279	elmapdd 8788	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦) ∈ (ℕ0 ↑m 𝐼))
281		ovexd 7402	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦) ∈ V)
282	43	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 0 ∈ ℕ0)
283	162, 159, 146, 146	offun 7645	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → Fun (𝑥 ∘f − 𝑦))
284	20	psrbagfsupp 21899	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} → 𝑥 finSupp 0)
285	284	ad2antlr 728	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑥 finSupp 0)
286		dffn2 6670	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∘f − 𝑦) Fn 𝐼 ↔ (𝑥 ∘f − 𝑦):𝐼⟶V)
287	261, 286	sylib 218	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦):𝐼⟶V)
288	162	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑥 Fn 𝐼)
289	159	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦 Fn 𝐼)
290	146	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝐼 ∈ 𝑉)
291		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0)))
292	291	eldifad 3901	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑎 ∈ 𝐼)
293	288, 289, 290, 292, 266	syl22anc 839	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥 ∘f − 𝑦)‘𝑎) = ((𝑥‘𝑎) − (𝑦‘𝑎)))
294	43	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 0 ∈ ℕ0)
295	288, 290, 294, 291	fvdifsupp 8121	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑥‘𝑎) = 0)
296	158	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦:𝐼⟶ℕ0)
297	296, 292	ffvelcdmd 7037	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ∈ ℕ0)
298		simplr 769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥})
299	164, 298	elrabrd 32568	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦 ∘r ≤ 𝑥)
300	289, 288, 290, 299, 292	fnfvor 32682	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ≤ (𝑥‘𝑎))
301	300, 295	breqtrd 5111	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ≤ 0)
302		nn0le0eq0 12465	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦‘𝑎) ∈ ℕ0 → ((𝑦‘𝑎) ≤ 0 ↔ (𝑦‘𝑎) = 0))
303	302	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦‘𝑎) ∈ ℕ0 ∧ (𝑦‘𝑎) ≤ 0) → (𝑦‘𝑎) = 0)
304	297, 301, 303	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) = 0)
305	295, 304	oveq12d 7385	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥‘𝑎) − (𝑦‘𝑎)) = (0 − 0))
306		0m0e0 12296	. . . . . . . . . . . . . . 15 ⊢ (0 − 0) = 0
307	306	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (0 − 0) = 0)
308	293, 305, 307	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥 ∘f − 𝑦)‘𝑎) = 0)
309	287, 308	suppss 8144	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ((𝑥 ∘f − 𝑦) supp 0) ⊆ (𝑥 supp 0))
310	281, 282, 283, 285, 309	fsuppsssuppgd 9295	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦) finSupp 0)
311	260, 280, 310	elrabd 3636	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
312		fvexd 6855	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))) ∈ V)
313	244, 259, 311, 312	fvmptd 6955	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
314	226, 313	oveq12d 7385	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦))) = ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))))
315	314	mpteq2dva 5178	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦)))) = (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))))
316	315	oveq2d 7383	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σg (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦))))) = (𝑅 Σg (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))))))
317	201, 316	eqtr4d 2774	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))) = (𝑅 Σg (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦))))))
318	317	mpteq2dva 5178	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦)))))))
319		oveq2 7375	. . . . . 6 ⊢ (𝑓 = (𝑖(.r‘𝑊)𝑗) → (𝐷𝐴𝑓) = (𝐷𝐴(𝑖(.r‘𝑊)𝑗)))
320	12	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
321		simprr 773	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) → 𝑓 = (𝑖(.r‘𝑊)𝑗))
322	2, 4, 117, 6, 20, 105, 125	mplmul 21989	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑖(.r‘𝑊)𝑗) = (𝑢 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ 𝑢} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘(𝑢 ∘f − 𝑣)))))))
323	322	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) → (𝑖(.r‘𝑊)𝑗) = (𝑢 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ 𝑢} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘(𝑢 ∘f − 𝑣)))))))
324	321, 323	eqtrd 2771	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) → 𝑓 = (𝑢 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ 𝑢} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘(𝑢 ∘f − 𝑣)))))))
325	324	adantr 480	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑓 = (𝑢 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ 𝑢} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘(𝑢 ∘f − 𝑣)))))))
326		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → 𝑢 = (𝑥 ∘ 𝑑))
327		simplrl 777	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑑 = 𝐷)
328	327	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → 𝑑 = 𝐷)
329	328	coeq2d 5817	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
330	326, 329	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → 𝑢 = (𝑥 ∘ 𝐷))
331	330	breq2d 5097	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑤 ∘r ≤ 𝑢 ↔ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)))
332	331	rabbidv 3396	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ 𝑢} = {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)})
333	330	fvoveq1d 7389	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑗‘(𝑢 ∘f − 𝑣)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))
334	333	oveq2d 7383	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘(𝑢 ∘f − 𝑣))) = ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))
335	332, 334	mpteq12dv 5172	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ 𝑢} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘(𝑢 ∘f − 𝑣)))) = (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))
336	335	oveq2d 7383	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ 𝑢} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘(𝑢 ∘f − 𝑣))))) = (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))))
337	7	ad4antr 733	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
338	26	ad4antr 733	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐷 ∈ 𝑃)
339	327, 338	eqeltrd 2836	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑑 ∈ 𝑃)
340		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
341	28, 29, 337, 339, 340	mplvrpmlem 33687	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝑑) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
342		ovexd 7402	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))) ∈ V)
343	325, 336, 341, 342	fvmptd 6955	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))))
344	343	mpteq2dva 5178	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))))
345	9	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑊 ∈ Ring)
346	4, 6, 345, 105, 125	ringcld 20241	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑖(.r‘𝑊)𝑗) ∈ 𝑀)
347	79	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V)
348	347	mptexd 7179	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))) ∈ V)
349	320, 344, 147, 346, 348	ovmpod 7519	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐷𝐴(𝑖(.r‘𝑊)𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))))
350	319, 349	sylan9eqr 2793	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗)) → (𝐷𝐴𝑓) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))))
351	10, 350, 346, 348	fvmptd2 6956	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(.r‘𝑊)𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))))
352	28, 29, 1, 12, 7	mplvrpmga 33689	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ (𝑆 GrpAct 𝑀))
353	29	gaf 19270	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑆 GrpAct 𝑀) → 𝐴:(𝑃 × 𝑀)⟶𝑀)
354	352, 353	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴:(𝑃 × 𝑀)⟶𝑀)
355	354	fovcld 7494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ∈ 𝑃 ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
356	355	3expa 1119	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐷 ∈ 𝑃) ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
357	356	an32s 653	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑀) ∧ 𝐷 ∈ 𝑃) → (𝐷𝐴𝑓) ∈ 𝑀)
358	26, 357	mpidan 690	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
359	358, 10	fmptd 7066	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑀⟶𝑀)
360	359	ad2antrr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐹:𝑀⟶𝑀)
361	360, 105	ffvelcdmd 7037	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘𝑖) ∈ 𝑀)
362	360, 125	ffvelcdmd 7037	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘𝑗) ∈ 𝑀)
363	2, 4, 117, 6, 20, 361, 362	mplmul 21989	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → ((𝐹‘𝑖)(.r‘𝑊)(𝐹‘𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦)))))))
364	318, 351, 363	3eqtr4d 2781	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(.r‘𝑊)𝑗)) = ((𝐹‘𝑖)(.r‘𝑊)(𝐹‘𝑗)))
365	364	anasss 466	. 2 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑀)) → (𝐹‘(𝑖(.r‘𝑊)𝑗)) = ((𝐹‘𝑖)(.r‘𝑊)(𝐹‘𝑗)))
366		eqid 2736	. 2 ⊢ (+g‘𝑊) = (+g‘𝑊)
367	28, 29, 1, 12, 7, 10, 2, 8, 26	mplvrpmmhm 33690	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (𝑊 MndHom 𝑊))
368	367	ad2antrr 727	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐹 ∈ (𝑊 MndHom 𝑊))
369	4, 366, 366	mhmlin 18761	. . . 4 ⊢ ((𝐹 ∈ (𝑊 MndHom 𝑊) ∧ 𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(+g‘𝑊)𝑗)) = ((𝐹‘𝑖)(+g‘𝑊)(𝐹‘𝑗)))
370	368, 105, 125, 369	syl3anc 1374	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(+g‘𝑊)𝑗)) = ((𝐹‘𝑖)(+g‘𝑊)(𝐹‘𝑗)))
371	370	anasss 466	. 2 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑀)) → (𝐹‘(𝑖(+g‘𝑊)𝑗)) = ((𝐹‘𝑖)(+g‘𝑊)(𝐹‘𝑗)))
372	4, 5, 5, 6, 6, 9, 9, 92, 365, 4, 366, 366, 359, 371	isrhmd 20467	1 ⊢ (𝜑 → 𝐹 ∈ (𝑊 RingHom 𝑊))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3051  {crab 3389  Vcvv 3429   ∖ cdif 3886   ⊆ wss 3889  ifcif 4466  {csn 4567   class class class wbr 5085   ↦ cmpt 5166   I cid 5525   × cxp 5629  ^◡ccnv 5630   ↾ cres 5633   ∘ ccom 5635   Fn wfn 6493  ⟶wf 6494  –1-1→wf1 6495  –1-1-onto→wf1o 6497  ‘cfv 6498  (class class class)co 7367   ∈ cmpo 7369   ∘_f cof 7629   ∘_r cofr 7630   supp csupp 8110   ↑_m cmap 8773   finSupp cfsupp 9274  0cc0 11038   ≤ cle 11180   − cmin 11377  ℕ₀cn0 12437  Basecbs 17179  +_gcplusg 17220  ._rcmulr 17221  0_gc0g 17402   Σ_g cgsu 17403   MndHom cmhm 18749   GrpAct cga 19264  SymGrpcsymg 19344  CMndccmn 19755  1_rcur 20162  Ringcrg 20214   RingHom crh 20449  SubRingcsubrg 20546   mPwSer cmps 21884   mPoly cmpl 21886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-iin 4936  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-of 7631  df-ofr 7632  df-om 7818  df-1st 7942  df-2nd 7943  df-supp 8111  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-er 8643  df-map 8775  df-pm 8776  df-ixp 8846  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fsupp 9275  df-sup 9355  df-oi 9425  df-card 9863  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-n0 12438  df-z 12525  df-dec 12645  df-uz 12789  df-fz 13462  df-fzo 13609  df-seq 13964  df-hash 14293  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-sca 17236  df-vsca 17237  df-ip 17238  df-tset 17239  df-ple 17240  df-ds 17242  df-hom 17244  df-cco 17245  df-0g 17404  df-gsum 17405  df-prds 17410  df-pws 17412  df-mre 17548  df-mrc 17549  df-acs 17551  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-mhm 18751  df-submnd 18752  df-efmnd 18837  df-grp 18912  df-minusg 18913  df-mulg 19044  df-subg 19099  df-ghm 19188  df-ga 19265  df-cntz 19292  df-symg 19345  df-cmn 19757  df-abl 19758  df-mgp 20122  df-rng 20134  df-ur 20163  df-ring 20216  df-rhm 20452  df-subrng 20523  df-subrg 20547  df-psr 21889  df-mpl 21891

This theorem is referenced by:  splysubrg  33704