Theorem mplvrpmrhm 33710

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 6839	. . 3 ⊢ (Base‘𝑊) = (Base‘(𝐼 mPoly 𝑅))
4	1, 3	eqtr4i 2763	. 2 ⊢ 𝑀 = (Base‘𝑊)
5		eqid 2737	. 2 ⊢ (1r‘𝑊) = (1r‘𝑊)
6		eqid 2737	. 2 ⊢ (.r‘𝑊) = (.r‘𝑊)
7		mplvrpmga.5	. . 3 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
8		mplvrpmmhm.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ Ring)
9	2, 7, 8	mplringd 22015	. 2 ⊢ (𝜑 → 𝑊 ∈ Ring)
10		mplvrpmmhm.f	. . 3 ⊢ 𝐹 = (𝑓 ∈ 𝑀 ↦ (𝐷𝐴𝑓))
11		oveq2 7370	. . . 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 5813	. . . . . . . . . 10 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊)) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
17	14, 16	fveq12d 6843	. . . . . . . . 9 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊)) → (𝑓‘(𝑥 ∘ 𝑑)) = ((1r‘𝑊)‘(𝑥 ∘ 𝐷)))
18	17	ad2antlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = ((1r‘𝑊)‘(𝑥 ∘ 𝐷)))
19		eqid 2737	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
20	19	psrbasfsupp 33691	. . . . . . . . . . . 12 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
21		eqid 2737	. . . . . . . . . . . 12 ⊢ (0g‘𝑅) = (0g‘𝑅)
22		eqid 2737	. . . . . . . . . . . 12 ⊢ (1r‘𝑅) = (1r‘𝑅)
23	2, 20, 21, 22, 5, 7, 8	mpl1 22004	. . . . . . . . . . 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 2741	. . . . . . . . . . . 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 19345	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ 𝑃 → 𝐷:𝐼–1-1-onto→𝐼)
31		f1ococnv2 6803	. . . . . . . . . . . . . . . . 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 5813	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ (𝐷 ∘ ◡𝐷)) = (𝑥 ∘ ( I ↾ 𝐼)))
35		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = (𝐼 × {0}))
36	35	coeq1d 5812	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝑥 ∘ 𝐷) ∘ ◡𝐷) = ((𝐼 × {0}) ∘ ◡𝐷))
37		coass 6226	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∘ 𝐷) ∘ ◡𝐷) = (𝑥 ∘ (𝐷 ∘ ◡𝐷))
38	37	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝑥 ∘ 𝐷) ∘ ◡𝐷) = (𝑥 ∘ (𝐷 ∘ ◡𝐷)))
39	26, 30	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷:𝐼–1-1-onto→𝐼)
40		f1ocnv 6788	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷:𝐼–1-1-onto→𝐼 → ◡𝐷:𝐼–1-1-onto→𝐼)
41		f1of 6776	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝐷:𝐼–1-1-onto→𝐼 → ◡𝐷:𝐼⟶𝐼)
42	39, 40, 41	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ◡𝐷:𝐼⟶𝐼)
43		0nn0 12447	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℕ0
44	43	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℕ0)
45	42, 44	constcof 32713	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐼 × {0}) ∘ ◡𝐷) = (𝐼 × {0}))
46	45	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝐼 × {0}) ∘ ◡𝐷) = (𝐼 × {0}))
47	36, 38, 46	3eqtr3d 2780	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ (𝐷 ∘ ◡𝐷)) = (𝐼 × {0}))
48	7	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
49		nn0ex 12438	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 ∈ V
50	49	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ℕ0 ∈ V)
51		ssrab2 4021	. . . . . . . . . . . . . . . . . 18 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐼)
52		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
53	51, 52	sselid 3920	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ (ℕ0 ↑m 𝐼))
54	48, 50, 53	elmaprd 32772	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥:𝐼⟶ℕ0)
55		fcoi1 6710	. . . . . . . . . . . . . . . 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 2781	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → 𝑥 = (𝐼 × {0}))
59		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → 𝑥 = (𝐼 × {0}))
60	59	coeq1d 5812	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = ((𝐼 × {0}) ∘ 𝐷))
61		f1of 6776	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷:𝐼–1-1-onto→𝐼 → 𝐷:𝐼⟶𝐼)
62	26, 30, 61	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷:𝐼⟶𝐼)
63	62, 44	constcof 32713	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐼 × {0}) ∘ 𝐷) = (𝐼 × {0}))
64	63	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → ((𝐼 × {0}) ∘ 𝐷) = (𝐼 × {0}))
65	60, 64	eqtrd 2772	. . . . . . . . . . . . 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 4491	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 = (𝑥 ∘ 𝐷)) → if(𝑦 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)) = if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)))
69	28, 29, 48, 27, 52	mplvrpmlem 33706	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
70		fvexd 6851	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (1r‘𝑅) ∈ V)
71		fvexd 6851	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (0g‘𝑅) ∈ V)
72	70, 71	ifcld 4514	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)) ∈ V)
73	24, 68, 69, 72	fvmptd 6951	. . . . . . . . 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 2772	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)))
76	75	mpteq2dva 5179	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊))) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))))
77	4, 5, 9	ringidcld 20242	. . . . . 6 ⊢ (𝜑 → (1r‘𝑊) ∈ 𝑀)
78		ovex 7395	. . . . . . . . 9 ⊢ (ℕ0 ↑m 𝐼) ∈ V
79	78	rabex 5277	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V
80	79	a1i 11	. . . . . . 7 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V)
81	80	mptexd 7174	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) ∈ V)
82	13, 76, 26, 77, 81	ovmpod 7514	. . . . 5 ⊢ (𝜑 → (𝐷𝐴(1r‘𝑊)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))))
83		eqid 2737	. . . . . 6 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
84		eqid 2737	. . . . . 6 ⊢ (1r‘(𝐼 mPwSer 𝑅)) = (1r‘(𝐼 mPwSer 𝑅))
85	83, 7, 8, 20, 21, 22, 84	psr1 21963	. . . . 5 ⊢ (𝜑 → (1r‘(𝐼 mPwSer 𝑅)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))))
86	83, 2, 4, 7, 8	mplsubrg 21997	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (SubRing‘(𝐼 mPwSer 𝑅)))
87	2, 83, 4	mplval2 21988	. . . . . . 7 ⊢ 𝑊 = ((𝐼 mPwSer 𝑅) ↾s 𝑀)
88	87, 84	subrg1 20554	. . . . . 6 ⊢ (𝑀 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → (1r‘(𝐼 mPwSer 𝑅)) = (1r‘𝑊))
89	86, 88	syl 17	. . . . 5 ⊢ (𝜑 → (1r‘(𝐼 mPwSer 𝑅)) = (1r‘𝑊))
90	82, 85, 89	3eqtr2d 2778	. . . 4 ⊢ (𝜑 → (𝐷𝐴(1r‘𝑊)) = (1r‘𝑊))
91	11, 90	sylan9eqr 2794	. . 3 ⊢ ((𝜑 ∧ 𝑓 = (1r‘𝑊)) → (𝐷𝐴𝑓) = (1r‘𝑊))
92	10, 91, 77, 77	fvmptd2 6952	. 2 ⊢ (𝜑 → (𝐹‘(1r‘𝑊)) = (1r‘𝑊))
93		nfcv 2899	. . . . . . 7 ⊢ Ⅎ𝑣((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
94		eqid 2737	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘𝑅)
95		fveq2 6836	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → (𝑖‘𝑣) = (𝑖‘(𝑦 ∘ 𝐷)))
96		oveq2 7370	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → ((𝑥 ∘ 𝐷) ∘f − 𝑣) = ((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))
97	96	fveq2d 6840	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → (𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
98	95, 97	oveq12d 7380	. . . . . . 7 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))) = ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))))
99	8	ringcmnd 20260	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ CMnd)
100	99	ad3antrrr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑅 ∈ CMnd)
101	79	rabex 5277	. . . . . . . 8 ⊢ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ∈ V
102	101	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ∈ V)
103		eqid 2737	. . . . . . . . . . . 12 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
104	2, 83, 4, 103	mplbasss 21989	. . . . . . . . . . . . . 14 ⊢ 𝑀 ⊆ (Base‘(𝐼 mPwSer 𝑅))
105		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑖 ∈ 𝑀)
106	104, 105	sselid 3920	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑖 ∈ (Base‘(𝐼 mPwSer 𝑅)))
107	106	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 ∈ (Base‘(𝐼 mPwSer 𝑅)))
108	83, 94, 20, 103, 107	psrelbas 21928	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖:{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
109	108	feqmptd 6904	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 = (𝑣 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘𝑣)))
110	105	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 ∈ 𝑀)
111	2, 4, 21, 110	mplelsfi 21987	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 finSupp (0g‘𝑅))
112	109, 111	eqbrtrrd 5110	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘𝑣)) finSupp (0g‘𝑅))
113		ssrab2 4021	. . . . . . . . . 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 6851	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (0g‘𝑅) ∈ V)
116	112, 114, 115	fmptssfisupp 9302	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ (𝑖‘𝑣)) finSupp (0g‘𝑅))
117		eqid 2737	. . . . . . . . 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 20271	. . . . . . . 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 3631	. . . . . . . . . 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 7033	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑖‘𝑣) ∈ (Base‘𝑅))
125		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑗 ∈ 𝑀)
126	104, 125	sselid 3920	. . . . . . . . . . 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 21928	. . . . . . . . 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 3920	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∈ (ℕ0 ↑m 𝐼))
133	130, 131, 132	elmaprd 32772	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣:𝐼⟶ℕ0)
134		breq1 5089	. . . . . . . . . . . 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 32587	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∘r ≤ (𝑥 ∘ 𝐷))
137	20	psrbagcon 21919	. . . . . . . . . . 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 7033	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)) ∈ (Base‘𝑅))
141	116, 120, 124, 140, 115	fsuppssov1 9292	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))) finSupp (0g‘𝑅))
142		ssidd 3946	. . . . . . 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 20236	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))) ∈ (Base‘𝑅))
145		breq1 5089	. . . . . . . 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 4021	. . . . . . . . . . 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 3920	. . . . . . . . . 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 33706	. . . . . . . 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 3934	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ⊆ (ℕ0 ↑m 𝐼))
157	156	sselda 3922	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦 ∈ (ℕ0 ↑m 𝐼))
158	146, 154, 157	elmaprd 32772	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦:𝐼⟶ℕ0)
159	158	ffnd 6665	. . . . . . . . 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 6665	. . . . . . . . 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 5089	. . . . . . . . . 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 32587	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦 ∘r ≤ 𝑥)
167	159, 162, 163, 146, 146, 166	ofrco 32702	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∘r ≤ (𝑥 ∘ 𝐷))
168	145, 153, 167	elrabd 3637	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)})
169		breq1 5089	. . . . . . . . 9 ⊢ (𝑧 = (𝑣 ∘ ◡𝐷) → (𝑧 ∘r ≤ 𝑥 ↔ (𝑣 ∘ ◡𝐷) ∘r ≤ 𝑥))
170		breq1 5089	. . . . . . . . . 10 ⊢ (ℎ = (𝑣 ∘ ◡𝐷) → (ℎ finSupp 0 ↔ (𝑣 ∘ ◡𝐷) finSupp 0))
171	42	ad4antr 733	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ◡𝐷:𝐼⟶𝐼)
172	133, 171	fcod 6689	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷):𝐼⟶ℕ0)
173	131, 130, 172	elmapdd 8783	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) ∈ (ℕ0 ↑m 𝐼))
174		breq1 5089	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑣 → (ℎ finSupp 0 ↔ 𝑣 finSupp 0))
175	174, 123	elrabrd 32587	. . . . . . . . . . 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 6775	. . . . . . . . . . . 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 9310	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) finSupp 0)
181	170, 173, 180	elrabd 3637	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
182	133	ffnd 6665	. . . . . . . . . . 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 6665	. . . . . . . . . . . 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 6701	. . . . . . . . . . . 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 32702	. . . . . . . . . 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 5813	. . . . . . . . . . . 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 2772	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ (𝐷 ∘ ◡𝐷)) = 𝑥)
193	37, 192	eqtrid 2784	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ((𝑥 ∘ 𝐷) ∘ ◡𝐷) = 𝑥)
194	188, 193	breqtrd 5112	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) ∘r ≤ 𝑥)
195	169, 181, 194	elrabd 3637	. . . . . . . 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 32821	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑣 = (𝑦 ∘ 𝐷) ↔ 𝑦 = (𝑣 ∘ ◡𝐷)))
200	195, 199	reu6dv 32561	. . . . . . 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 33140	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))) = (𝑅 Σg (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))))))
202		coeq1 5808	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑦 → (𝑡 ∘ 𝐷) = (𝑦 ∘ 𝐷))
203	202	fveq2d 6840	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → (𝑖‘(𝑡 ∘ 𝐷)) = (𝑖‘(𝑦 ∘ 𝐷)))
204		oveq2 7370	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑖 → (𝐷𝐴𝑓) = (𝐷𝐴𝑖))
205	105	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑖 ∈ 𝑀)
206		ovexd 7397	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐷𝐴𝑖) ∈ V)
207	10, 204, 205, 206	fvmptd3 6967	. . . . . . . . . . . 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 5809	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝐷 → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
211	210	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
212	209, 211	fveq12d 6843	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑖‘(𝑥 ∘ 𝐷)))
213	212	mpteq2dv 5180	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑥 ∘ 𝐷))))
214		coeq1 5808	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (𝑥 ∘ 𝐷) = (𝑡 ∘ 𝐷))
215	214	fveq2d 6840	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (𝑖‘(𝑥 ∘ 𝐷)) = (𝑖‘(𝑡 ∘ 𝐷)))
216	215	cbvmptv 5190	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑥 ∘ 𝐷))) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷)))
217	213, 216	eqtrdi 2788	. . . . . . . . . . . . . 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 7174	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))) ∈ V)
222	208, 218, 219, 205, 221	ovmpod 7514	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐷𝐴𝑖) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
223	207, 222	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐹‘𝑖) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
224		fvexd 6851	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑖‘(𝑦 ∘ 𝐷)) ∈ V)
225	203, 223, 151, 224	fvmptd4 6968	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ((𝐹‘𝑖)‘𝑦) = (𝑖‘(𝑦 ∘ 𝐷)))
226	225	adantlr 716	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ((𝐹‘𝑖)‘𝑦) = (𝑖‘(𝑦 ∘ 𝐷)))
227		oveq2 7370	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑗 → (𝐷𝐴𝑓) = (𝐷𝐴𝑗))
228		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → 𝑓 = 𝑗)
229	210	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
230	228, 229	fveq12d 6843	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑗‘(𝑥 ∘ 𝐷)))
231	230	mpteq2dv 5180	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑥 ∘ 𝐷))))
232	214	fveq2d 6840	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (𝑗‘(𝑥 ∘ 𝐷)) = (𝑗‘(𝑡 ∘ 𝐷)))
233	232	cbvmptv 5190	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑥 ∘ 𝐷))) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷)))
234	231, 233	eqtrdi 2788	. . . . . . . . . . . . . . 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 7174	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))) ∈ V)
238	208, 235, 219, 236, 237	ovmpod 7514	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐷𝐴𝑗) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
239	227, 238	sylan9eqr 2794	. . . . . . . . . . . 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 7174	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))) ∈ V)
244	10, 240, 241, 243	fvmptd2 6952	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐹‘𝑗) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
245		coeq1 5808	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑥 ∘f − 𝑦) → (𝑡 ∘ 𝐷) = ((𝑥 ∘f − 𝑦) ∘ 𝐷))
246	245	fveq2d 6840	. . . . . . . . . . . 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 6665	. . . . . . . . . . . . 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 32772	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → 𝑦:𝐼⟶ℕ0)
254	253	ffnd 6665	. . . . . . . . . . . . 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 4168	. . . . . . . . . . . . 13 ⊢ (𝐼 ∩ 𝐼) = 𝐼
257	249, 254, 255, 250, 250, 250, 256	ofco 7651	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → ((𝑥 ∘f − 𝑦) ∘ 𝐷) = ((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))
258	257	fveq2d 6840	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → (𝑗‘((𝑥 ∘f − 𝑦) ∘ 𝐷)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
259	247, 258	eqtrd 2772	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → (𝑗‘(𝑡 ∘ 𝐷)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
260		breq1 5089	. . . . . . . . . . 11 ⊢ (ℎ = (𝑥 ∘f − 𝑦) → (ℎ finSupp 0 ↔ (𝑥 ∘f − 𝑦) finSupp 0))
261	162, 159, 146, 146, 256	offn 7639	. . . . . . . . . . . . 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 7643	. . . . . . . . . . . . . . . 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 7032	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑦‘𝑎) ∈ ℕ0)
269	161	ffvelcdmda 7032	. . . . . . . . . . . . . . . 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 32587	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑦 ∘r ≤ 𝑥)
272	263, 262, 264, 271, 265	fnfvor 32701	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑦‘𝑎) ≤ (𝑥‘𝑎))
273		nn0sub 12482	. . . . . . . . . . . . . . . . 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 2837	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → ((𝑥 ∘f − 𝑦)‘𝑎) ∈ ℕ0)
277	276	ralrimiva 3130	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ∀𝑎 ∈ 𝐼 ((𝑥 ∘f − 𝑦)‘𝑎) ∈ ℕ0)
278		ffnfv 7067	. . . . . . . . . . . . 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 8783	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦) ∈ (ℕ0 ↑m 𝐼))
281		ovexd 7397	. . . . . . . . . . . 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 7640	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → Fun (𝑥 ∘f − 𝑦))
284	20	psrbagfsupp 21913	. . . . . . . . . . . . 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 6666	. . . . . . . . . . . . . 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 3902	. . . . . . . . . . . . . . 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 8116	. . . . . . . . . . . . . . 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 7033	. . . . . . . . . . . . . . . 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 32587	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦 ∘r ≤ 𝑥)
300	289, 288, 290, 299, 292	fnfvor 32701	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ≤ (𝑥‘𝑎))
301	300, 295	breqtrd 5112	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ≤ 0)
302		nn0le0eq0 12460	. . . . . . . . . . . . . . . . 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 7380	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥‘𝑎) − (𝑦‘𝑎)) = (0 − 0))
306		0m0e0 12291	. . . . . . . . . . . . . . 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 2776	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥 ∘f − 𝑦)‘𝑎) = 0)
309	287, 308	suppss 8139	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ((𝑥 ∘f − 𝑦) supp 0) ⊆ (𝑥 supp 0))
310	281, 282, 283, 285, 309	fsuppsssuppgd 9290	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦) finSupp 0)
311	260, 280, 310	elrabd 3637	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
312		fvexd 6851	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))) ∈ V)
313	244, 259, 311, 312	fvmptd 6951	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
314	226, 313	oveq12d 7380	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦))) = ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))))
315	314	mpteq2dva 5179	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦)))) = (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))))
316	315	oveq2d 7378	. . . . . 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 2775	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))) = (𝑅 Σg (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦))))))
318	317	mpteq2dva 5179	. . . 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 7370	. . . . . 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 22003	. . . . . . . . . . . 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 2772	. . . . . . . . . 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 5813	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
330	326, 329	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → 𝑢 = (𝑥 ∘ 𝐷))
331	330	breq2d 5098	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑤 ∘r ≤ 𝑢 ↔ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)))
332	331	rabbidv 3397	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ 𝑢} = {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)})
333	330	fvoveq1d 7384	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑗‘(𝑢 ∘f − 𝑣)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))
334	333	oveq2d 7378	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘(𝑢 ∘f − 𝑣))) = ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))
335	332, 334	mpteq12dv 5173	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ 𝑢} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘(𝑢 ∘f − 𝑣)))) = (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))
336	335	oveq2d 7378	. . . . . . . . 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 2837	. . . . . . . . . 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 33706	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝑑) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
342		ovexd 7397	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))) ∈ V)
343	325, 336, 341, 342	fvmptd 6951	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))))
344	343	mpteq2dva 5179	. . . . . . 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 20236	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑖(.r‘𝑊)𝑗) ∈ 𝑀)
347	79	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V)
348	347	mptexd 7174	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))) ∈ V)
349	320, 344, 147, 346, 348	ovmpod 7514	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐷𝐴(𝑖(.r‘𝑊)𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))))
350	319, 349	sylan9eqr 2794	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗)) → (𝐷𝐴𝑓) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))))
351	10, 350, 346, 348	fvmptd2 6952	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(.r‘𝑊)𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))))
352	28, 29, 1, 12, 7	mplvrpmga 33708	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ (𝑆 GrpAct 𝑀))
353	29	gaf 19265	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑆 GrpAct 𝑀) → 𝐴:(𝑃 × 𝑀)⟶𝑀)
354	352, 353	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴:(𝑃 × 𝑀)⟶𝑀)
355	354	fovcld 7489	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ∈ 𝑃 ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
356	355	3expa 1119	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐷 ∈ 𝑃) ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
357	356	an32s 653	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑀) ∧ 𝐷 ∈ 𝑃) → (𝐷𝐴𝑓) ∈ 𝑀)
358	26, 357	mpidan 690	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
359	358, 10	fmptd 7062	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑀⟶𝑀)
360	359	ad2antrr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐹:𝑀⟶𝑀)
361	360, 105	ffvelcdmd 7033	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘𝑖) ∈ 𝑀)
362	360, 125	ffvelcdmd 7033	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘𝑗) ∈ 𝑀)
363	2, 4, 117, 6, 20, 361, 362	mplmul 22003	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → ((𝐹‘𝑖)(.r‘𝑊)(𝐹‘𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦)))))))
364	318, 351, 363	3eqtr4d 2782	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(.r‘𝑊)𝑗)) = ((𝐹‘𝑖)(.r‘𝑊)(𝐹‘𝑗)))
365	364	anasss 466	. 2 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑀)) → (𝐹‘(𝑖(.r‘𝑊)𝑗)) = ((𝐹‘𝑖)(.r‘𝑊)(𝐹‘𝑗)))
366		eqid 2737	. 2 ⊢ (+g‘𝑊) = (+g‘𝑊)
367	28, 29, 1, 12, 7, 10, 2, 8, 26	mplvrpmmhm 33709	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (𝑊 MndHom 𝑊))
368	367	ad2antrr 727	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐹 ∈ (𝑊 MndHom 𝑊))
369	4, 366, 366	mhmlin 18756	. . . 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 20462	1 ⊢ (𝜑 → 𝐹 ∈ (𝑊 RingHom 𝑊))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  {crab 3390  Vcvv 3430   ∖ cdif 3887   ⊆ wss 3890  ifcif 4467  {csn 4568   class class class wbr 5086   ↦ cmpt 5167   I cid 5520   × cxp 5624  ^◡ccnv 5625   ↾ cres 5628   ∘ ccom 5630   Fn wfn 6489  ⟶wf 6490  –1-1→wf1 6491  –1-1-onto→wf1o 6493  ‘cfv 6494  (class class class)co 7362   ∈ cmpo 7364   ∘_f cof 7624   ∘_r cofr 7625   supp csupp 8105   ↑_m cmap 8768   finSupp cfsupp 9269  0cc0 11033   ≤ cle 11175   − cmin 11372  ℕ₀cn0 12432  Basecbs 17174  +_gcplusg 17215  ._rcmulr 17216  0_gc0g 17397   Σ_g cgsu 17398   MndHom cmhm 18744   GrpAct cga 19259  SymGrpcsymg 19339  CMndccmn 19750  1_rcur 20157  Ringcrg 20209   RingHom crh 20444  SubRingcsubrg 20541   mPwSer cmps 21898   mPoly cmpl 21900

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 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5521  df-eprel 5526  df-po 5534  df-so 5535  df-fr 5579  df-se 5580  df-we 5581  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-pred 6261  df-ord 6322  df-on 6323  df-lim 6324  df-suc 6325  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-isom 6503  df-riota 7319  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7626  df-ofr 7627  df-om 7813  df-1st 7937  df-2nd 7938  df-supp 8106  df-frecs 8226  df-wrecs 8257  df-recs 8306  df-rdg 8344  df-1o 8400  df-2o 8401  df-er 8638  df-map 8770  df-pm 8771  df-ixp 8841  df-en 8889  df-dom 8890  df-sdom 8891  df-fin 8892  df-fsupp 9270  df-sup 9350  df-oi 9420  df-card 9858  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-nn 12170  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243  df-7 12244  df-8 12245  df-9 12246  df-n0 12433  df-z 12520  df-dec 12640  df-uz 12784  df-fz 13457  df-fzo 13604  df-seq 13959  df-hash 14288  df-struct 17112  df-sets 17129  df-slot 17147  df-ndx 17159  df-base 17175  df-ress 17196  df-plusg 17228  df-mulr 17229  df-sca 17231  df-vsca 17232  df-ip 17233  df-tset 17234  df-ple 17235  df-ds 17237  df-hom 17239  df-cco 17240  df-0g 17399  df-gsum 17400  df-prds 17405  df-pws 17407  df-mre 17543  df-mrc 17544  df-acs 17546  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-mhm 18746  df-submnd 18747  df-efmnd 18832  df-grp 18907  df-minusg 18908  df-mulg 19039  df-subg 19094  df-ghm 19183  df-ga 19260  df-cntz 19287  df-symg 19340  df-cmn 19752  df-abl 19753  df-mgp 20117  df-rng 20129  df-ur 20158  df-ring 20211  df-rhm 20447  df-subrng 20518  df-subrg 20542  df-psr 21903  df-mpl 21905

This theorem is referenced by:  splysubrg  33723