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 6836	. . 3 ⊢ (Base‘𝑊) = (Base‘(𝐼 mPoly 𝑅))
4	1, 3	eqtr4i 2761	. 2 ⊢ 𝑀 = (Base‘𝑊)
5		eqid 2735	. 2 ⊢ (1r‘𝑊) = (1r‘𝑊)
6		eqid 2735	. 2 ⊢ (.r‘𝑊) = (.r‘𝑊)
7		mplvrpmga.5	. . 3 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
8		mplvrpmmhm.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ Ring)
9	2, 7, 8	mplringd 21980	. 2 ⊢ (𝜑 → 𝑊 ∈ Ring)
10		mplvrpmmhm.f	. . 3 ⊢ 𝐹 = (𝑓 ∈ 𝑀 ↦ (𝐷𝐴𝑓))
11		oveq2 7366	. . . 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 5810	. . . . . . . . . 10 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊)) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
17	14, 16	fveq12d 6840	. . . . . . . . 9 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊)) → (𝑓‘(𝑥 ∘ 𝑑)) = ((1r‘𝑊)‘(𝑥 ∘ 𝐷)))
18	17	ad2antlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = ((1r‘𝑊)‘(𝑥 ∘ 𝐷)))
19		eqid 2735	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
20	19	psrbasfsupp 33672	. . . . . . . . . . . 12 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
21		eqid 2735	. . . . . . . . . . . 12 ⊢ (0g‘𝑅) = (0g‘𝑅)
22		eqid 2735	. . . . . . . . . . . 12 ⊢ (1r‘𝑅) = (1r‘𝑅)
23	2, 20, 21, 22, 5, 7, 8	mpl1 21969	. . . . . . . . . . 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 2739	. . . . . . . . . . . 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 19306	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ 𝑃 → 𝐷:𝐼–1-1-onto→𝐼)
31		f1ococnv2 6800	. . . . . . . . . . . . . . . . 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 5810	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ (𝐷 ∘ ◡𝐷)) = (𝑥 ∘ ( I ↾ 𝐼)))
35		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = (𝐼 × {0}))
36	35	coeq1d 5809	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝑥 ∘ 𝐷) ∘ ◡𝐷) = ((𝐼 × {0}) ∘ ◡𝐷))
37		coass 6223	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∘ 𝐷) ∘ ◡𝐷) = (𝑥 ∘ (𝐷 ∘ ◡𝐷))
38	37	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝑥 ∘ 𝐷) ∘ ◡𝐷) = (𝑥 ∘ (𝐷 ∘ ◡𝐷)))
39	26, 30	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷:𝐼–1-1-onto→𝐼)
40		f1ocnv 6785	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷:𝐼–1-1-onto→𝐼 → ◡𝐷:𝐼–1-1-onto→𝐼)
41		f1of 6773	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝐷:𝐼–1-1-onto→𝐼 → ◡𝐷:𝐼⟶𝐼)
42	39, 40, 41	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ◡𝐷:𝐼⟶𝐼)
43		0nn0 12418	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℕ0
44	43	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℕ0)
45	42, 44	constcof 32679	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐼 × {0}) ∘ ◡𝐷) = (𝐼 × {0}))
46	45	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝐼 × {0}) ∘ ◡𝐷) = (𝐼 × {0}))
47	36, 38, 46	3eqtr3d 2778	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ (𝐷 ∘ ◡𝐷)) = (𝐼 × {0}))
48	7	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
49		nn0ex 12409	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 ∈ V
50	49	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ℕ0 ∈ V)
51		ssrab2 4031	. . . . . . . . . . . . . . . . . 18 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐼)
52		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
53	51, 52	sselid 3930	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ (ℕ0 ↑m 𝐼))
54	48, 50, 53	elmaprd 32738	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥:𝐼⟶ℕ0)
55		fcoi1 6707	. . . . . . . . . . . . . . . 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 2779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → 𝑥 = (𝐼 × {0}))
59		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → 𝑥 = (𝐼 × {0}))
60	59	coeq1d 5809	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = ((𝐼 × {0}) ∘ 𝐷))
61		f1of 6773	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷:𝐼–1-1-onto→𝐼 → 𝐷:𝐼⟶𝐼)
62	26, 30, 61	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷:𝐼⟶𝐼)
63	62, 44	constcof 32679	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐼 × {0}) ∘ 𝐷) = (𝐼 × {0}))
64	63	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → ((𝐼 × {0}) ∘ 𝐷) = (𝐼 × {0}))
65	60, 64	eqtrd 2770	. . . . . . . . . . . . 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 4502	. . . . . . . . . 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 6848	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (1r‘𝑅) ∈ V)
71		fvexd 6848	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (0g‘𝑅) ∈ V)
72	70, 71	ifcld 4525	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)) ∈ V)
73	24, 68, 69, 72	fvmptd 6948	. . . . . . . . 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 2770	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅)))
76	75	mpteq2dva 5190	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1r‘𝑊))) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))))
77	4, 5, 9	ringidcld 20203	. . . . . 6 ⊢ (𝜑 → (1r‘𝑊) ∈ 𝑀)
78		ovex 7391	. . . . . . . . 9 ⊢ (ℕ0 ↑m 𝐼) ∈ V
79	78	rabex 5283	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V
80	79	a1i 11	. . . . . . 7 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V)
81	80	mptexd 7170	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))) ∈ V)
82	13, 76, 26, 77, 81	ovmpod 7510	. . . . 5 ⊢ (𝜑 → (𝐷𝐴(1r‘𝑊)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))))
83		eqid 2735	. . . . . 6 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
84		eqid 2735	. . . . . 6 ⊢ (1r‘(𝐼 mPwSer 𝑅)) = (1r‘(𝐼 mPwSer 𝑅))
85	83, 7, 8, 20, 21, 22, 84	psr1 21928	. . . . 5 ⊢ (𝜑 → (1r‘(𝐼 mPwSer 𝑅)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1r‘𝑅), (0g‘𝑅))))
86	83, 2, 4, 7, 8	mplsubrg 21962	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (SubRing‘(𝐼 mPwSer 𝑅)))
87	2, 83, 4	mplval2 21953	. . . . . . 7 ⊢ 𝑊 = ((𝐼 mPwSer 𝑅) ↾s 𝑀)
88	87, 84	subrg1 20517	. . . . . 6 ⊢ (𝑀 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → (1r‘(𝐼 mPwSer 𝑅)) = (1r‘𝑊))
89	86, 88	syl 17	. . . . 5 ⊢ (𝜑 → (1r‘(𝐼 mPwSer 𝑅)) = (1r‘𝑊))
90	82, 85, 89	3eqtr2d 2776	. . . 4 ⊢ (𝜑 → (𝐷𝐴(1r‘𝑊)) = (1r‘𝑊))
91	11, 90	sylan9eqr 2792	. . 3 ⊢ ((𝜑 ∧ 𝑓 = (1r‘𝑊)) → (𝐷𝐴𝑓) = (1r‘𝑊))
92	10, 91, 77, 77	fvmptd2 6949	. 2 ⊢ (𝜑 → (𝐹‘(1r‘𝑊)) = (1r‘𝑊))
93		nfcv 2897	. . . . . . 7 ⊢ Ⅎ𝑣((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
94		eqid 2735	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘𝑅)
95		fveq2 6833	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → (𝑖‘𝑣) = (𝑖‘(𝑦 ∘ 𝐷)))
96		oveq2 7366	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → ((𝑥 ∘ 𝐷) ∘f − 𝑣) = ((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))
97	96	fveq2d 6837	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → (𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
98	95, 97	oveq12d 7376	. . . . . . 7 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))) = ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))))
99	8	ringcmnd 20221	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ CMnd)
100	99	ad3antrrr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑅 ∈ CMnd)
101	79	rabex 5283	. . . . . . . 8 ⊢ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ∈ V
102	101	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ∈ V)
103		eqid 2735	. . . . . . . . . . . 12 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
104	2, 83, 4, 103	mplbasss 21954	. . . . . . . . . . . . . 14 ⊢ 𝑀 ⊆ (Base‘(𝐼 mPwSer 𝑅))
105		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑖 ∈ 𝑀)
106	104, 105	sselid 3930	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑖 ∈ (Base‘(𝐼 mPwSer 𝑅)))
107	106	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 ∈ (Base‘(𝐼 mPwSer 𝑅)))
108	83, 94, 20, 103, 107	psrelbas 21892	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖:{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
109	108	feqmptd 6901	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 = (𝑣 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘𝑣)))
110	105	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 ∈ 𝑀)
111	2, 4, 21, 110	mplelsfi 21952	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 finSupp (0g‘𝑅))
112	109, 111	eqbrtrrd 5121	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘𝑣)) finSupp (0g‘𝑅))
113		ssrab2 4031	. . . . . . . . . 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 6848	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (0g‘𝑅) ∈ V)
116	112, 114, 115	fmptssfisupp 9299	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ (𝑖‘𝑣)) finSupp (0g‘𝑅))
117		eqid 2735	. . . . . . . . 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 20232	. . . . . . . 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 3641	. . . . . . . . . 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 7030	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑖‘𝑣) ∈ (Base‘𝑅))
125		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑗 ∈ 𝑀)
126	104, 125	sselid 3930	. . . . . . . . . . 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 21892	. . . . . . . . 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 3930	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∈ (ℕ0 ↑m 𝐼))
133	130, 131, 132	elmaprd 32738	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣:𝐼⟶ℕ0)
134		breq1 5100	. . . . . . . . . . . 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 32553	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∘r ≤ (𝑥 ∘ 𝐷))
137	20	psrbagcon 21883	. . . . . . . . . . 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 7030	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)) ∈ (Base‘𝑅))
141	116, 120, 124, 140, 115	fsuppssov1 9289	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))) finSupp (0g‘𝑅))
142		ssidd 3956	. . . . . . 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 20197	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))) ∈ (Base‘𝑅))
145		breq1 5100	. . . . . . . 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 4031	. . . . . . . . . . 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 3930	. . . . . . . . . 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 3944	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ⊆ (ℕ0 ↑m 𝐼))
157	156	sselda 3932	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦 ∈ (ℕ0 ↑m 𝐼))
158	146, 154, 157	elmaprd 32738	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦:𝐼⟶ℕ0)
159	158	ffnd 6662	. . . . . . . . 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 6662	. . . . . . . . 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 5100	. . . . . . . . . 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 32553	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑦 ∘r ≤ 𝑥)
167	159, 162, 163, 146, 146, 166	ofrco 32668	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∘r ≤ (𝑥 ∘ 𝐷))
168	145, 153, 167	elrabd 3647	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)})
169		breq1 5100	. . . . . . . . 9 ⊢ (𝑧 = (𝑣 ∘ ◡𝐷) → (𝑧 ∘r ≤ 𝑥 ↔ (𝑣 ∘ ◡𝐷) ∘r ≤ 𝑥))
170		breq1 5100	. . . . . . . . . 10 ⊢ (ℎ = (𝑣 ∘ ◡𝐷) → (ℎ finSupp 0 ↔ (𝑣 ∘ ◡𝐷) finSupp 0))
171	42	ad4antr 733	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ◡𝐷:𝐼⟶𝐼)
172	133, 171	fcod 6686	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷):𝐼⟶ℕ0)
173	131, 130, 172	elmapdd 8780	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) ∈ (ℕ0 ↑m 𝐼))
174		breq1 5100	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑣 → (ℎ finSupp 0 ↔ 𝑣 finSupp 0))
175	174, 123	elrabrd 32553	. . . . . . . . . . 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 6772	. . . . . . . . . . . 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 9307	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) finSupp 0)
181	170, 173, 180	elrabd 3647	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
182	133	ffnd 6662	. . . . . . . . . . 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 6662	. . . . . . . . . . . 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 6698	. . . . . . . . . . . 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 32668	. . . . . . . . . 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 5810	. . . . . . . . . . . 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 2770	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ (𝐷 ∘ ◡𝐷)) = 𝑥)
193	37, 192	eqtrid 2782	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → ((𝑥 ∘ 𝐷) ∘ ◡𝐷) = 𝑥)
194	188, 193	breqtrd 5123	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ◡𝐷) ∘r ≤ 𝑥)
195	169, 181, 194	elrabd 3647	. . . . . . . 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 32787	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑣 = (𝑦 ∘ 𝐷) ↔ 𝑦 = (𝑣 ∘ ◡𝐷)))
200	195, 199	reu6dv 32527	. . . . . . 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 33122	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))) = (𝑅 Σg (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))))))
202		coeq1 5805	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑦 → (𝑡 ∘ 𝐷) = (𝑦 ∘ 𝐷))
203	202	fveq2d 6837	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → (𝑖‘(𝑡 ∘ 𝐷)) = (𝑖‘(𝑦 ∘ 𝐷)))
204		oveq2 7366	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑖 → (𝐷𝐴𝑓) = (𝐷𝐴𝑖))
205	105	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → 𝑖 ∈ 𝑀)
206		ovexd 7393	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐷𝐴𝑖) ∈ V)
207	10, 204, 205, 206	fvmptd3 6964	. . . . . . . . . . . 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 5806	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝐷 → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
211	210	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
212	209, 211	fveq12d 6840	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑖‘(𝑥 ∘ 𝐷)))
213	212	mpteq2dv 5191	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑥 ∘ 𝐷))))
214		coeq1 5805	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (𝑥 ∘ 𝐷) = (𝑡 ∘ 𝐷))
215	214	fveq2d 6837	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (𝑖‘(𝑥 ∘ 𝐷)) = (𝑖‘(𝑡 ∘ 𝐷)))
216	215	cbvmptv 5201	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑥 ∘ 𝐷))) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷)))
217	213, 216	eqtrdi 2786	. . . . . . . . . . . . . 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 7170	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))) ∈ V)
222	208, 218, 219, 205, 221	ovmpod 7510	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐷𝐴𝑖) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
223	207, 222	eqtrd 2770	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐹‘𝑖) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
224		fvexd 6848	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑖‘(𝑦 ∘ 𝐷)) ∈ V)
225	203, 223, 151, 224	fvmptd4 6965	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ((𝐹‘𝑖)‘𝑦) = (𝑖‘(𝑦 ∘ 𝐷)))
226	225	adantlr 716	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ((𝐹‘𝑖)‘𝑦) = (𝑖‘(𝑦 ∘ 𝐷)))
227		oveq2 7366	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑗 → (𝐷𝐴𝑓) = (𝐷𝐴𝑗))
228		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → 𝑓 = 𝑗)
229	210	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
230	228, 229	fveq12d 6840	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑗‘(𝑥 ∘ 𝐷)))
231	230	mpteq2dv 5191	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑥 ∘ 𝐷))))
232	214	fveq2d 6837	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (𝑗‘(𝑥 ∘ 𝐷)) = (𝑗‘(𝑡 ∘ 𝐷)))
233	232	cbvmptv 5201	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑥 ∘ 𝐷))) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷)))
234	231, 233	eqtrdi 2786	. . . . . . . . . . . . . . 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 7170	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))) ∈ V)
238	208, 235, 219, 236, 237	ovmpod 7510	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐷𝐴𝑗) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
239	227, 238	sylan9eqr 2792	. . . . . . . . . . . 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 7170	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))) ∈ V)
244	10, 240, 241, 243	fvmptd2 6949	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝐹‘𝑗) = (𝑡 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
245		coeq1 5805	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑥 ∘f − 𝑦) → (𝑡 ∘ 𝐷) = ((𝑥 ∘f − 𝑦) ∘ 𝐷))
246	245	fveq2d 6837	. . . . . . . . . . . 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 6662	. . . . . . . . . . . . 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 32738	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → 𝑦:𝐼⟶ℕ0)
254	253	ffnd 6662	. . . . . . . . . . . . 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 4178	. . . . . . . . . . . . 13 ⊢ (𝐼 ∩ 𝐼) = 𝐼
257	249, 254, 255, 250, 250, 250, 256	ofco 7647	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → ((𝑥 ∘f − 𝑦) ∘ 𝐷) = ((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))
258	257	fveq2d 6837	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → (𝑗‘((𝑥 ∘f − 𝑦) ∘ 𝐷)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
259	247, 258	eqtrd 2770	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘f − 𝑦)) → (𝑗‘(𝑡 ∘ 𝐷)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
260		breq1 5100	. . . . . . . . . . 11 ⊢ (ℎ = (𝑥 ∘f − 𝑦) → (ℎ finSupp 0 ↔ (𝑥 ∘f − 𝑦) finSupp 0))
261	162, 159, 146, 146, 256	offn 7635	. . . . . . . . . . . . 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 7639	. . . . . . . . . . . . . . . 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 7029	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑦‘𝑎) ∈ ℕ0)
269	161	ffvelcdmda 7029	. . . . . . . . . . . . . . . 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 32553	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑦 ∘r ≤ 𝑥)
272	263, 262, 264, 271, 265	fnfvor 32667	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑦‘𝑎) ≤ (𝑥‘𝑎))
273		nn0sub 12453	. . . . . . . . . . . . . . . . 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 2835	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → ((𝑥 ∘f − 𝑦)‘𝑎) ∈ ℕ0)
277	276	ralrimiva 3127	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ∀𝑎 ∈ 𝐼 ((𝑥 ∘f − 𝑦)‘𝑎) ∈ ℕ0)
278		ffnfv 7064	. . . . . . . . . . . . 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 8780	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦) ∈ (ℕ0 ↑m 𝐼))
281		ovexd 7393	. . . . . . . . . . . 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 7636	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → Fun (𝑥 ∘f − 𝑦))
284	20	psrbagfsupp 21877	. . . . . . . . . . . . 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 6663	. . . . . . . . . . . . . 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 3912	. . . . . . . . . . . . . . 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 8113	. . . . . . . . . . . . . . 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 7030	. . . . . . . . . . . . . . . 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 32553	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦 ∘r ≤ 𝑥)
300	289, 288, 290, 299, 292	fnfvor 32667	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ≤ (𝑥‘𝑎))
301	300, 295	breqtrd 5123	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ≤ 0)
302		nn0le0eq0 12431	. . . . . . . . . . . . . . . . 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 7376	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥‘𝑎) − (𝑦‘𝑎)) = (0 − 0))
306		0m0e0 12262	. . . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥 ∘f − 𝑦)‘𝑎) = 0)
309	287, 308	suppss 8136	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ((𝑥 ∘f − 𝑦) supp 0) ⊆ (𝑥 supp 0))
310	281, 282, 283, 285, 309	fsuppsssuppgd 9287	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦) finSupp 0)
311	260, 280, 310	elrabd 3647	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑥 ∘f − 𝑦) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
312		fvexd 6848	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))) ∈ V)
313	244, 259, 311, 312	fvmptd 6948	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → ((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))
314	226, 313	oveq12d 7376	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥}) → (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦))) = ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷)))))
315	314	mpteq2dva 5190	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦)))) = (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − (𝑦 ∘ 𝐷))))))
316	315	oveq2d 7374	. . . . . 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 2773	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))) = (𝑅 Σg (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦))))))
318	317	mpteq2dva 5190	. . . 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 7366	. . . . . 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 21968	. . . . . . . . . . . 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 2770	. . . . . . . . . 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 5810	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
330	326, 329	eqtrd 2770	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → 𝑢 = (𝑥 ∘ 𝐷))
331	330	breq2d 5109	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑤 ∘r ≤ 𝑢 ↔ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)))
332	331	rabbidv 3405	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ 𝑢} = {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)})
333	330	fvoveq1d 7380	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑗‘(𝑢 ∘f − 𝑣)) = (𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))
334	333	oveq2d 7374	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘(𝑢 ∘f − 𝑣))) = ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))
335	332, 334	mpteq12dv 5184	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ 𝑢} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘(𝑢 ∘f − 𝑣)))) = (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))
336	335	oveq2d 7374	. . . . . . . . 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 2835	. . . . . . . . . 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 7393	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))) ∈ V)
343	325, 336, 341, 342	fvmptd 6948	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣))))))
344	343	mpteq2dva 5190	. . . . . . 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 20197	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑖(.r‘𝑊)𝑗) ∈ 𝑀)
347	79	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V)
348	347	mptexd 7170	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))) ∈ V)
349	320, 344, 147, 346, 348	ovmpod 7510	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐷𝐴(𝑖(.r‘𝑊)𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))))
350	319, 349	sylan9eqr 2792	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑓 = (𝑖(.r‘𝑊)𝑗)) → (𝐷𝐴𝑓) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(.r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘f − 𝑣)))))))
351	10, 350, 346, 348	fvmptd2 6949	. . . 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 19226	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑆 GrpAct 𝑀) → 𝐴:(𝑃 × 𝑀)⟶𝑀)
354	352, 353	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴:(𝑃 × 𝑀)⟶𝑀)
355	354	fovcld 7485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ∈ 𝑃 ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
356	355	3expa 1119	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐷 ∈ 𝑃) ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
357	356	an32s 653	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑀) ∧ 𝐷 ∈ 𝑃) → (𝐷𝐴𝑓) ∈ 𝑀)
358	26, 357	mpidan 690	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
359	358, 10	fmptd 7059	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑀⟶𝑀)
360	359	ad2antrr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐹:𝑀⟶𝑀)
361	360, 105	ffvelcdmd 7030	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘𝑖) ∈ 𝑀)
362	360, 125	ffvelcdmd 7030	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘𝑗) ∈ 𝑀)
363	2, 4, 117, 6, 20, 361, 362	mplmul 21968	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → ((𝐹‘𝑖)(.r‘𝑊)(𝐹‘𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σg (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(.r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘f − 𝑦)))))))
364	318, 351, 363	3eqtr4d 2780	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(.r‘𝑊)𝑗)) = ((𝐹‘𝑖)(.r‘𝑊)(𝐹‘𝑗)))
365	364	anasss 466	. 2 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑀)) → (𝐹‘(𝑖(.r‘𝑊)𝑗)) = ((𝐹‘𝑖)(.r‘𝑊)(𝐹‘𝑗)))
366		eqid 2735	. 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 18720	. . . 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 20425	1 ⊢ (𝜑 → 𝐹 ∈ (𝑊 RingHom 𝑊))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3050  {crab 3398  Vcvv 3439   ∖ cdif 3897   ⊆ wss 3900  ifcif 4478  {csn 4579   class class class wbr 5097   ↦ cmpt 5178   I cid 5517   × cxp 5621  ^◡ccnv 5622   ↾ cres 5625   ∘ ccom 5627   Fn wfn 6486  ⟶wf 6487  –1-1→wf1 6488  –1-1-onto→wf1o 6490  ‘cfv 6491  (class class class)co 7358   ∈ cmpo 7360   ∘_f cof 7620   ∘_r cofr 7621   supp csupp 8102   ↑_m cmap 8765   finSupp cfsupp 9266  0cc0 11028   ≤ cle 11169   − cmin 11366  ℕ₀cn0 12403  Basecbs 17138  +_gcplusg 17179  ._rcmulr 17180  0_gc0g 17361   Σ_g cgsu 17362   MndHom cmhm 18708   GrpAct cga 19220  SymGrpcsymg 19300  CMndccmn 19711  1_rcur 20118  Ringcrg 20170   RingHom crh 20407  SubRingcsubrg 20504   mPwSer cmps 21862   mPoly cmpl 21864

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 2183  ax-ext 2707  ax-rep 5223  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3349  df-reu 3350  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4863  df-int 4902  df-iun 4947  df-iin 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-se 5577  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6258  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-isom 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7622  df-ofr 7623  df-om 7809  df-1st 7933  df-2nd 7934  df-supp 8103  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-2o 8398  df-er 8635  df-map 8767  df-pm 8768  df-ixp 8838  df-en 8886  df-dom 8887  df-sdom 8888  df-fin 8889  df-fsupp 9267  df-sup 9347  df-oi 9417  df-card 9853  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-nn 12148  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214  df-7 12215  df-8 12216  df-9 12217  df-n0 12404  df-z 12491  df-dec 12610  df-uz 12754  df-fz 13426  df-fzo 13573  df-seq 13927  df-hash 14256  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17139  df-ress 17160  df-plusg 17192  df-mulr 17193  df-sca 17195  df-vsca 17196  df-ip 17197  df-tset 17198  df-ple 17199  df-ds 17201  df-hom 17203  df-cco 17204  df-0g 17363  df-gsum 17364  df-prds 17369  df-pws 17371  df-mre 17507  df-mrc 17508  df-acs 17510  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-mhm 18710  df-submnd 18711  df-efmnd 18796  df-grp 18868  df-minusg 18869  df-mulg 19000  df-subg 19055  df-ghm 19144  df-ga 19221  df-cntz 19248  df-symg 19301  df-cmn 19713  df-abl 19714  df-mgp 20078  df-rng 20090  df-ur 20119  df-ring 20172  df-rhm 20410  df-subrng 20481  df-subrg 20505  df-psr 21867  df-mpl 21869

This theorem is referenced by:  splysubrg  33697