mplvrpmrhm - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mplvrpmrhm		Structured version Visualization version GIF version

Theorem mplvrpmrhm 34246

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	⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_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 6908	. . 3 ⊢ (Base‘𝑊) = (Base‘(𝐼 mPoly 𝑅))
4	1, 3	eqtr4i 2789	. 2 ⊢ 𝑀 = (Base‘𝑊)
5		eqid 2763	. 2 ⊢ (1_r‘𝑊) = (1_r‘𝑊)
6		eqid 2763	. 2 ⊢ (._r‘𝑊) = (._r‘𝑊)
7		mplvrpmga.5	. . 3 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
8		mplvrpmmhm.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ Ring)
9	2, 7, 8	mplringd 22357	. 2 ⊢ (𝜑 → 𝑊 ∈ Ring)
10		mplvrpmmhm.f	. . 3 ⊢ 𝐹 = (𝑓 ∈ 𝑀 ↦ (𝐷𝐴𝑓))
11		oveq2 7448	. . . 4 ⊢ (𝑓 = (1_r‘𝑊) → (𝐷𝐴𝑓) = (𝐷𝐴(1_r‘𝑊)))
12		mplvrpmga.4	. . . . . . 7 ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))
13	12	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
14		simpr 490	. . . . . . . . . 10 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊)) → 𝑓 = (1_r‘𝑊))
15		simpl 488	. . . . . . . . . . 11 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊)) → 𝑑 = 𝐷)
16	15	coeq2d 5845	. . . . . . . . . 10 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊)) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
17	14, 16	fveq12d 6912	. . . . . . . . 9 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊)) → (𝑓‘(𝑥 ∘ 𝑑)) = ((1_r‘𝑊)‘(𝑥 ∘ 𝐷)))
18	17	ad2antlr 740	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = ((1_r‘𝑊)‘(𝑥 ∘ 𝐷)))
19		eqid 2763	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}
20	19	psrbasfsupp 34210	. . . . . . . . . . . 12 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}
21		eqid 2763	. . . . . . . . . . . 12 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
22		eqid 2763	. . . . . . . . . . . 12 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
23	2, 20, 21, 22, 5, 7, 8	mpl1 22346	. . . . . . . . . . 11 ⊢ (𝜑 → (1_r‘𝑊) = (𝑦 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑦 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅))))
24	23	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (1_r‘𝑊) = (𝑦 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑦 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅))))
25		eqeq1 2767	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥 ∘ 𝐷) → (𝑦 = (𝐼 × {0}) ↔ (𝑥 ∘ 𝐷) = (𝐼 × {0})))
26		mplvrpmmhm.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
27	26	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝐷 ∈ 𝑃)
28		mplvrpmga.1	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (SymGrp‘𝐼)
29		mplvrpmga.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑃 = (Base‘𝑆)
30	28, 29	symgbasf1o 19616	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ 𝑃 → 𝐷:𝐼⟶1-1onto𝐼)
31		f1ococnv2 6872	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷:𝐼⟶1-1onto𝐼 → (𝐷 ∘ ^◡𝐷) = ( I ↾ 𝐼))
32	27, 30, 31	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝐷 ∘ ^◡𝐷) = ( I ↾ 𝐼))
33	32	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝐷 ∘ ^◡𝐷) = ( I ↾ 𝐼))
34	33	coeq2d 5845	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ (𝐷 ∘ ^◡𝐷)) = (𝑥 ∘ ( I ↾ 𝐼)))
35		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = (𝐼 × {0}))
36	35	coeq1d 5844	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝑥 ∘ 𝐷) ∘ ^◡𝐷) = ((𝐼 × {0}) ∘ ^◡𝐷))
37		coass 6281	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∘ 𝐷) ∘ ^◡𝐷) = (𝑥 ∘ (𝐷 ∘ ^◡𝐷))
38	37	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝑥 ∘ 𝐷) ∘ ^◡𝐷) = (𝑥 ∘ (𝐷 ∘ ^◡𝐷)))
39	26, 30	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷:𝐼⟶1-1onto𝐼)
40		f1ocnv 6856	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷:𝐼⟶1-1onto𝐼 → ^◡𝐷:𝐼⟶1-1onto𝐼)
41		f1of 6843	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐷:𝐼⟶1-1onto𝐼 → ^◡𝐷:𝐼⟶𝐼)
42	39, 40, 41	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ^◡𝐷:𝐼⟶𝐼)
43		0nn0 12645	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℕ₀
44	43	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℕ₀)
45	42, 44	constcof 33284	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐼 × {0}) ∘ ^◡𝐷) = (𝐼 × {0}))
46	45	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝐼 × {0}) ∘ ^◡𝐷) = (𝐼 × {0}))
47	36, 38, 46	3eqtr3d 2806	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ (𝐷 ∘ ^◡𝐷)) = (𝐼 × {0}))
48		ssrab2 4008	. . . . . . . . . . . . . . . . . 18 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ₀ ↑_m 𝐼)
49		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
50	48, 49	sselid 3911	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ (ℕ₀ ↑_m 𝐼))
51	50	elmaprd 8895	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑥:𝐼⟶ℕ₀)
52		fcoi1 6775	. . . . . . . . . . . . . . . 16 ⊢ (𝑥:𝐼⟶ℕ₀ → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
53	51, 52	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
54	53	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
55	34, 47, 54	3eqtr3rd 2807	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → 𝑥 = (𝐼 × {0}))
56		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → 𝑥 = (𝐼 × {0}))
57	56	coeq1d 5844	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = ((𝐼 × {0}) ∘ 𝐷))
58		f1of 6843	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷:𝐼⟶1-1onto𝐼 → 𝐷:𝐼⟶𝐼)
59	26, 30, 58	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷:𝐼⟶𝐼)
60	59, 44	constcof 33284	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐼 × {0}) ∘ 𝐷) = (𝐼 × {0}))
61	60	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → ((𝐼 × {0}) ∘ 𝐷) = (𝐼 × {0}))
62	57, 61	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = (𝐼 × {0}))
63	55, 62	impbida 813	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → ((𝑥 ∘ 𝐷) = (𝐼 × {0}) ↔ 𝑥 = (𝐼 × {0})))
64	25, 63	sylan9bbr 520	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 = (𝑥 ∘ 𝐷)) → (𝑦 = (𝐼 × {0}) ↔ 𝑥 = (𝐼 × {0})))
65	64	ifbid 4509	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 = (𝑥 ∘ 𝐷)) → if(𝑦 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅)) = if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅)))
66	7	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
67	28, 29, 66, 27, 49	mplvrpmlem 34242	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝐷) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
68		fvexd 6920	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (1_r‘𝑅) ∈ V)
69		fvexd 6920	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (0_g‘𝑅) ∈ V)
70	68, 69	ifcld 4532	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅)) ∈ V)
71	24, 65, 67, 70	fvmptd 7021	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → ((1_r‘𝑊)‘(𝑥 ∘ 𝐷)) = if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅)))
72	71	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → ((1_r‘𝑊)‘(𝑥 ∘ 𝐷)) = if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅)))
73	18, 72	eqtrd 2798	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅)))
74	73	mpteq2dva 5201	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊))) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅))))
75	4, 5, 9	ringidcld 20522	. . . . . 6 ⊢ (𝜑 → (1_r‘𝑊) ∈ 𝑀)
76		ovex 7473	. . . . . . . . 9 ⊢ (ℕ₀ ↑_m 𝐼) ∈ V
77	76	rabex 5304	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∈ V
78	77	a1i 11	. . . . . . 7 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∈ V)
79	78	mptexd 7250	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅))) ∈ V)
80	13, 74, 26, 75, 79	ovmpod 7593	. . . . 5 ⊢ (𝜑 → (𝐷𝐴(1_r‘𝑊)) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅))))
81		eqid 2763	. . . . . 6 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
82		eqid 2763	. . . . . 6 ⊢ (1_r‘(𝐼 mPwSer 𝑅)) = (1_r‘(𝐼 mPwSer 𝑅))
83	81, 7, 8, 20, 21, 22, 82	psr1 22305	. . . . 5 ⊢ (𝜑 → (1_r‘(𝐼 mPwSer 𝑅)) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅))))
84	81, 2, 4, 7, 8	mplsubrg 22339	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (SubRing‘(𝐼 mPwSer 𝑅)))
85	2, 81, 4	mplval2 22330	. . . . . . 7 ⊢ 𝑊 = ((𝐼 mPwSer 𝑅) ↾_s 𝑀)
86	85, 82	subrg1 20861	. . . . . 6 ⊢ (𝑀 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → (1_r‘(𝐼 mPwSer 𝑅)) = (1_r‘𝑊))
87	84, 86	syl 18	. . . . 5 ⊢ (𝜑 → (1_r‘(𝐼 mPwSer 𝑅)) = (1_r‘𝑊))
88	80, 83, 87	3eqtr2d 2804	. . . 4 ⊢ (𝜑 → (𝐷𝐴(1_r‘𝑊)) = (1_r‘𝑊))
89	11, 88	sylan9eqr 2820	. . 3 ⊢ ((𝜑 ∧ 𝑓 = (1_r‘𝑊)) → (𝐷𝐴𝑓) = (1_r‘𝑊))
90	10, 89, 75, 75	fvmptd2 7022	. 2 ⊢ (𝜑 → (𝐹‘(1_r‘𝑊)) = (1_r‘𝑊))
91		nfcv 2926	. . . . . . 7 ⊢ Ⅎ𝑣((𝑖‘(𝑦 ∘ 𝐷))(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))))
92		eqid 2763	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘𝑅)
93		fveq2 6905	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → (𝑖‘𝑣) = (𝑖‘(𝑦 ∘ 𝐷)))
94		oveq2 7448	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → ((𝑥 ∘ 𝐷) ∘_f − 𝑣) = ((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷)))
95	94	fveq2d 6909	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → (𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)) = (𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))))
96	93, 95	oveq12d 7458	. . . . . . 7 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))) = ((𝑖‘(𝑦 ∘ 𝐷))(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷)))))
97	8	ringcmnd 20540	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ CMnd)
98	97	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑅 ∈ CMnd)
99	77	rabex 5304	. . . . . . . 8 ⊢ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ∈ V
100	99	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ∈ V)
101		eqid 2763	. . . . . . . . . . . 12 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
102	2, 81, 4, 101	mplbasss 22331	. . . . . . . . . . . . . 14 ⊢ 𝑀 ⊆ (Base‘(𝐼 mPwSer 𝑅))
103		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑖 ∈ 𝑀)
104	102, 103	sselid 3911	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑖 ∈ (Base‘(𝐼 mPwSer 𝑅)))
105	104	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 ∈ (Base‘(𝐼 mPwSer 𝑅)))
106	81, 92, 20, 101, 105	psrelbas 22270	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑖:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
107	106	feqmptd 6973	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 = (𝑣 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘𝑣)))
108	103	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 ∈ 𝑀)
109	2, 4, 21, 108	mplelsfi 22329	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 finSupp (0_g‘𝑅))
110	107, 109	eqbrtrrd 5132	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘𝑣)) finSupp (0_g‘𝑅))
111		ssrab2 4008	. . . . . . . . . 10 ⊢ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ⊆ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}
112	111	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ⊆ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
113		fvexd 6920	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (0_g‘𝑅) ∈ V)
114	110, 112, 113	fmptssfisupp 9410	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ (𝑖‘𝑣)) finSupp (0_g‘𝑅))
115		eqid 2763	. . . . . . . . 9 ⊢ (._r‘𝑅) = (._r‘𝑅)
116	8	ad4antr 745	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑛 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring)
117		simpr 490	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑛 ∈ (Base‘𝑅)) → 𝑛 ∈ (Base‘𝑅))
118	92, 115, 21, 116, 117	ringlzd 20553	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑛 ∈ (Base‘𝑅)) → ((0_g‘𝑅)(._r‘𝑅)𝑛) = (0_g‘𝑅))
119	106	adantr 486	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑖:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
120		elrabi 3644	. . . . . . . . . 10 ⊢ (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} → 𝑣 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
121	120	adantl 487	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
122	119, 121	ffvelcdmd 7106	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑖‘𝑣) ∈ (Base‘𝑅))
123		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑗 ∈ 𝑀)
124	102, 123	sselid 3911	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑗 ∈ (Base‘(𝐼 mPwSer 𝑅)))
125	124	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑗 ∈ (Base‘(𝐼 mPwSer 𝑅)))
126	81, 92, 20, 101, 125	psrelbas 22270	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑗:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
127	67	ad5ant14 770	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ 𝐷) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
128	48, 121	sselid 3911	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∈ (ℕ₀ ↑_m 𝐼))
129	128	elmaprd 8895	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣:𝐼⟶ℕ₀)
130		breq1 5109	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑤 ∘_r ≤ (𝑥 ∘ 𝐷) ↔ 𝑣 ∘_r ≤ (𝑥 ∘ 𝐷)))
131		simpr 490	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)})
132	130, 131	elrabrd 3651	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∘_r ≤ (𝑥 ∘ 𝐷))
133	20	psrbagcon 22260	. . . . . . . . . . 11 ⊢ (((𝑥 ∘ 𝐷) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∧ 𝑣:𝐼⟶ℕ₀ ∧ 𝑣 ∘_r ≤ (𝑥 ∘ 𝐷)) → (((𝑥 ∘ 𝐷) ∘_f − 𝑣) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∧ ((𝑥 ∘ 𝐷) ∘_f − 𝑣) ∘_r ≤ (𝑥 ∘ 𝐷)))
134	127, 129, 132, 133	syl3anc 1399	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (((𝑥 ∘ 𝐷) ∘_f − 𝑣) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∧ ((𝑥 ∘ 𝐷) ∘_f − 𝑣) ∘_r ≤ (𝑥 ∘ 𝐷)))
135	134	simpld 500	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ((𝑥 ∘ 𝐷) ∘_f − 𝑣) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
136	126, 135	ffvelcdmd 7106	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)) ∈ (Base‘𝑅))
137	114, 118, 122, 136, 113	fsuppssov1 9400	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))) finSupp (0_g‘𝑅))
138		ssidd 3936	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (Base‘𝑅) ⊆ (Base‘𝑅))
139	8	ad4antr 745	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑅 ∈ Ring)
140	92, 115, 139, 122, 136	ringcld 20511	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))) ∈ (Base‘𝑅))
141		breq1 5109	. . . . . . . 8 ⊢ (𝑤 = (𝑦 ∘ 𝐷) → (𝑤 ∘_r ≤ (𝑥 ∘ 𝐷) ↔ (𝑦 ∘ 𝐷) ∘_r ≤ (𝑥 ∘ 𝐷)))
142	7	ad4antr 745	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝐼 ∈ 𝑉)
143	26	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐷 ∈ 𝑃)
144	143	ad2antrr 739	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝐷 ∈ 𝑃)
145		ssrab2 4008	. . . . . . . . . . 11 ⊢ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ⊆ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}
146		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥})
147	145, 146	sselid 3911	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
148	147	adantlr 728	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
149	28, 29, 142, 144, 148	mplvrpmlem 34242	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
150	48	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ₀ ↑_m 𝐼))
151	145, 150	sstrid 3924	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ⊆ (ℕ₀ ↑_m 𝐼))
152	151	sselda 3913	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 ∈ (ℕ₀ ↑_m 𝐼))
153	152	elmaprd 8895	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦:𝐼⟶ℕ₀)
154	153	ffnd 6729	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 Fn 𝐼)
155	51	ad4ant14 765	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑥:𝐼⟶ℕ₀)
156	155	adantr 486	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑥:𝐼⟶ℕ₀)
157	156	ffnd 6729	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑥 Fn 𝐼)
158	59	ad4antr 745	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝐷:𝐼⟶𝐼)
159		breq1 5109	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → (𝑧 ∘_r ≤ 𝑥 ↔ 𝑦 ∘_r ≤ 𝑥))
160		simpr 490	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥})
161	159, 160	elrabrd 3651	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 ∘_r ≤ 𝑥)
162	154, 157, 158, 142, 142, 161	ofrco 33273	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∘_r ≤ (𝑥 ∘ 𝐷))
163	141, 149, 162	elrabd 3650	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)})
164		breq1 5109	. . . . . . . . 9 ⊢ (𝑧 = (𝑣 ∘ ^◡𝐷) → (𝑧 ∘_r ≤ 𝑥 ↔ (𝑣 ∘ ^◡𝐷) ∘_r ≤ 𝑥))
165		breq1 5109	. . . . . . . . . 10 ⊢ (ℎ = (𝑣 ∘ ^◡𝐷) → (ℎ finSupp 0 ↔ (𝑣 ∘ ^◡𝐷) finSupp 0))
166		nn0ex 12636	. . . . . . . . . . . 12 ⊢ ℕ₀ ∈ V
167	166	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ℕ₀ ∈ V)
168	7	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝐼 ∈ 𝑉)
169	42	ad4antr 745	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ^◡𝐷:𝐼⟶𝐼)
170	129, 169	fcod 6754	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷):𝐼⟶ℕ₀)
171	167, 168, 170	elmapdd 8886	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷) ∈ (ℕ₀ ↑_m 𝐼))
172		breq1 5109	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑣 → (ℎ finSupp 0 ↔ 𝑣 finSupp 0))
173	172, 121	elrabrd 3651	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 finSupp 0)
174	39	ad4antr 745	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝐷:𝐼⟶1-1onto𝐼)
175		f1of1 6842	. . . . . . . . . . . 12 ⊢ (^◡𝐷:𝐼⟶1-1onto𝐼 → ^◡𝐷:𝐼⟶1-1𝐼)
176	174, 40, 175	3syl 19	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ^◡𝐷:𝐼⟶1-1𝐼)
177	43	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 0 ∈ ℕ₀)
178	173, 176, 177, 121	fsuppco 9418	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷) finSupp 0)
179	165, 171, 178	elrabd 3650	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
180	129	ffnd 6729	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 Fn 𝐼)
181	155	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑥:𝐼⟶ℕ₀)
182	181	ffnd 6729	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑥 Fn 𝐼)
183	59	ad4antr 745	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝐷:𝐼⟶𝐼)
184		fnfco 6766	. . . . . . . . . . . 12 ⊢ ((𝑥 Fn 𝐼 ∧ 𝐷:𝐼⟶𝐼) → (𝑥 ∘ 𝐷) Fn 𝐼)
185	182, 183, 184	syl2anc 596	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ 𝐷) Fn 𝐼)
186	180, 185, 169, 168, 168, 132	ofrco 33273	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷) ∘_r ≤ ((𝑥 ∘ 𝐷) ∘ ^◡𝐷))
187	174, 31	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝐷 ∘ ^◡𝐷) = ( I ↾ 𝐼))
188	187	coeq2d 5845	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ (𝐷 ∘ ^◡𝐷)) = (𝑥 ∘ ( I ↾ 𝐼)))
189	181, 52	syl 18	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
190	188, 189	eqtrd 2798	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ (𝐷 ∘ ^◡𝐷)) = 𝑥)
191	37, 190	eqtrid 2810	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ((𝑥 ∘ 𝐷) ∘ ^◡𝐷) = 𝑥)
192	186, 191	breqtrd 5134	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷) ∘_r ≤ 𝑥)
193	164, 179, 192	elrabd 3650	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷) ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥})
194	129	adantr 486	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑣:𝐼⟶ℕ₀)
195	153	adantlr 728	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦:𝐼⟶ℕ₀)
196	39	ad5antr 747	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝐷:𝐼⟶1-1onto𝐼)
197	194, 195, 196	cocnvf1o 33388	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑣 = (𝑦 ∘ 𝐷) ↔ 𝑦 = (𝑣 ∘ ^◡𝐷)))
198	193, 197	reu6dv 33138	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ∃!𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}𝑣 = (𝑦 ∘ 𝐷))
199	91, 92, 21, 96, 98, 100, 137, 138, 140, 163, 198	gsummptfsf1o 33688	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))))) = (𝑅 Σ_g (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷)))))))
200		coeq1 5840	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑦 → (𝑡 ∘ 𝐷) = (𝑦 ∘ 𝐷))
201	200	fveq2d 6909	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → (𝑖‘(𝑡 ∘ 𝐷)) = (𝑖‘(𝑦 ∘ 𝐷)))
202		oveq2 7448	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑖 → (𝐷𝐴𝑓) = (𝐷𝐴𝑖))
203	103	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑖 ∈ 𝑀)
204		ovexd 7475	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝐷𝐴𝑖) ∈ V)
205	10, 202, 203, 204	fvmptd3 7037	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝐹‘𝑖) = (𝐷𝐴𝑖))
206	12	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
207		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → 𝑓 = 𝑖)
208		coeq2 5841	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝐷 → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
209	208	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
210	207, 209	fveq12d 6912	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑖‘(𝑥 ∘ 𝐷)))
211	210	mpteq2dv 5202	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑥 ∘ 𝐷))))
212		coeq1 5840	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (𝑥 ∘ 𝐷) = (𝑡 ∘ 𝐷))
213	212	fveq2d 6909	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (𝑖‘(𝑥 ∘ 𝐷)) = (𝑖‘(𝑡 ∘ 𝐷)))
214	213	cbvmptv 5212	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑥 ∘ 𝐷))) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷)))
215	211, 214	eqtrdi 2814	. . . . . . . . . . . . . 14 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
216	215	adantl 487	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ (𝑑 = 𝐷 ∧ 𝑓 = 𝑖)) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
217	143	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝐷 ∈ 𝑃)
218	77	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∈ V)
219	218	mptexd 7250	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))) ∈ V)
220	206, 216, 217, 203, 219	ovmpod 7593	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝐷𝐴𝑖) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
221	205, 220	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝐹‘𝑖) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
222		fvexd 6920	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑖‘(𝑦 ∘ 𝐷)) ∈ V)
223	201, 221, 147, 222	fvmptd4 7038	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → ((𝐹‘𝑖)‘𝑦) = (𝑖‘(𝑦 ∘ 𝐷)))
224	223	adantlr 728	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → ((𝐹‘𝑖)‘𝑦) = (𝑖‘(𝑦 ∘ 𝐷)))
225		oveq2 7448	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑗 → (𝐷𝐴𝑓) = (𝐷𝐴𝑗))
226		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → 𝑓 = 𝑗)
227	208	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
228	226, 227	fveq12d 6912	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑗‘(𝑥 ∘ 𝐷)))
229	228	mpteq2dv 5202	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑥 ∘ 𝐷))))
230	212	fveq2d 6909	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (𝑗‘(𝑥 ∘ 𝐷)) = (𝑗‘(𝑡 ∘ 𝐷)))
231	230	cbvmptv 5212	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑥 ∘ 𝐷))) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷)))
232	229, 231	eqtrdi 2814	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
233	232	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ (𝑑 = 𝐷 ∧ 𝑓 = 𝑗)) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
234		simplr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑗 ∈ 𝑀)
235	218	mptexd 7250	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))) ∈ V)
236	206, 233, 217, 234, 235	ovmpod 7593	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝐷𝐴𝑗) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
237	225, 236	sylan9eqr 2820	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑓 = 𝑗) → (𝐷𝐴𝑓) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
238	237	adantllr 732	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑓 = 𝑗) → (𝐷𝐴𝑓) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
239	123	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑗 ∈ 𝑀)
240	77	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∈ V)
241	240	mptexd 7250	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))) ∈ V)
242	10, 238, 239, 241	fvmptd2 7022	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝐹‘𝑗) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
243		coeq1 5840	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑥 ∘_f − 𝑦) → (𝑡 ∘ 𝐷) = ((𝑥 ∘_f − 𝑦) ∘ 𝐷))
244	243	fveq2d 6909	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑥 ∘_f − 𝑦) → (𝑗‘(𝑡 ∘ 𝐷)) = (𝑗‘((𝑥 ∘_f − 𝑦) ∘ 𝐷)))
245	244	adantl 487	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → (𝑗‘(𝑡 ∘ 𝐷)) = (𝑗‘((𝑥 ∘_f − 𝑦) ∘ 𝐷)))
246	155	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝑥:𝐼⟶ℕ₀)
247	246	ffnd 6729	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝑥 Fn 𝐼)
248	152	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝑦 ∈ (ℕ₀ ↑_m 𝐼))
249	248	elmaprd 8895	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝑦:𝐼⟶ℕ₀)
250	249	ffnd 6729	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝑦 Fn 𝐼)
251	59	ad5antr 747	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝐷:𝐼⟶𝐼)
252	7	ad5antr 747	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝐼 ∈ 𝑉)
253		inidm 4126	. . . . . . . . . . . . 13 ⊢ (𝐼 ∩ 𝐼) = 𝐼
254	247, 250, 251, 252, 252, 252, 253	ofco 7739	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → ((𝑥 ∘_f − 𝑦) ∘ 𝐷) = ((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷)))
255	254	fveq2d 6909	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → (𝑗‘((𝑥 ∘_f − 𝑦) ∘ 𝐷)) = (𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))))
256	245, 255	eqtrd 2798	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → (𝑗‘(𝑡 ∘ 𝐷)) = (𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))))
257		breq1 5109	. . . . . . . . . . 11 ⊢ (ℎ = (𝑥 ∘_f − 𝑦) → (ℎ finSupp 0 ↔ (𝑥 ∘_f − 𝑦) finSupp 0))
258	166	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → ℕ₀ ∈ V)
259	157, 154, 142, 142, 253	offn 7727	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦) Fn 𝐼)
260	157	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑥 Fn 𝐼)
261	154	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑦 Fn 𝐼)
262	142	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝐼 ∈ 𝑉)
263		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑎 ∈ 𝐼)
264		fnfvof 7731	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 Fn 𝐼 ∧ 𝑦 Fn 𝐼) ∧ (𝐼 ∈ 𝑉 ∧ 𝑎 ∈ 𝐼)) → ((𝑥 ∘_f − 𝑦)‘𝑎) = ((𝑥‘𝑎) − (𝑦‘𝑎)))
265	260, 261, 262, 263, 264	syl22anc 852	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → ((𝑥 ∘_f − 𝑦)‘𝑎) = ((𝑥‘𝑎) − (𝑦‘𝑎)))
266	153	ffvelcdmda 7105	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑦‘𝑎) ∈ ℕ₀)
267	156	ffvelcdmda 7105	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑥‘𝑎) ∈ ℕ₀)
268		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥})
269	159, 268	elrabrd 3651	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑦 ∘_r ≤ 𝑥)
270	261, 260, 262, 269, 263	fnfvor 33272	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑦‘𝑎) ≤ (𝑥‘𝑎))
271		nn0sub 12680	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦‘𝑎) ∈ ℕ₀ ∧ (𝑥‘𝑎) ∈ ℕ₀) → ((𝑦‘𝑎) ≤ (𝑥‘𝑎) ↔ ((𝑥‘𝑎) − (𝑦‘𝑎)) ∈ ℕ₀))
272	271	biimpa 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦‘𝑎) ∈ ℕ₀ ∧ (𝑥‘𝑎) ∈ ℕ₀) ∧ (𝑦‘𝑎) ≤ (𝑥‘𝑎)) → ((𝑥‘𝑎) − (𝑦‘𝑎)) ∈ ℕ₀)
273	266, 267, 270, 272	syl21anc 851	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → ((𝑥‘𝑎) − (𝑦‘𝑎)) ∈ ℕ₀)
274	265, 273	eqeltrd 2864	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → ((𝑥 ∘_f − 𝑦)‘𝑎) ∈ ℕ₀)
275	274	ralrimiva 3158	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → ∀𝑎 ∈ 𝐼 ((𝑥 ∘_f − 𝑦)‘𝑎) ∈ ℕ₀)
276		ffnfv 7140	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∘_f − 𝑦):𝐼⟶ℕ₀ ↔ ((𝑥 ∘_f − 𝑦) Fn 𝐼 ∧ ∀𝑎 ∈ 𝐼 ((𝑥 ∘_f − 𝑦)‘𝑎) ∈ ℕ₀))
277	259, 275, 276	sylanbrc 595	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦):𝐼⟶ℕ₀)
278	258, 142, 277	elmapdd 8886	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦) ∈ (ℕ₀ ↑_m 𝐼))
279		ovexd 7475	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦) ∈ V)
280	43	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 0 ∈ ℕ₀)
281	157, 154, 142, 142	offun 7728	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → Fun (𝑥 ∘_f − 𝑦))
282	20	psrbagfsupp 22254	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} → 𝑥 finSupp 0)
283	282	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑥 finSupp 0)
284		dffn2 6730	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∘_f − 𝑦) Fn 𝐼 ↔ (𝑥 ∘_f − 𝑦):𝐼⟶V)
285	259, 284	sylib 221	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦):𝐼⟶V)
286	157	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑥 Fn 𝐼)
287	154	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦 Fn 𝐼)
288	142	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝐼 ∈ 𝑉)
289		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0)))
290	289	eldifad 4054	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑎 ∈ 𝐼)
291	286, 287, 288, 290, 264	syl22anc 852	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥 ∘_f − 𝑦)‘𝑎) = ((𝑥‘𝑎) − (𝑦‘𝑎)))
292	43	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 0 ∈ ℕ₀)
293	286, 288, 292, 289	fvdifsupp 8213	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑥‘𝑎) = 0)
294	153	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦:𝐼⟶ℕ₀)
295	294, 290	ffvelcdmd 7106	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ∈ ℕ₀)
296		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥})
297	159, 296	elrabrd 3651	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦 ∘_r ≤ 𝑥)
298	287, 286, 288, 297, 290	fnfvor 33272	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ≤ (𝑥‘𝑎))
299	298, 293	breqtrd 5134	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ≤ 0)
300		nn0le0eq0 12658	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦‘𝑎) ∈ ℕ₀ → ((𝑦‘𝑎) ≤ 0 ↔ (𝑦‘𝑎) = 0))
301	300	biimpa 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦‘𝑎) ∈ ℕ₀ ∧ (𝑦‘𝑎) ≤ 0) → (𝑦‘𝑎) = 0)
302	295, 299, 301	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) = 0)
303	293, 302	oveq12d 7458	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥‘𝑎) − (𝑦‘𝑎)) = (0 − 0))
304		0m0e0 12485	. . . . . . . . . . . . . . 15 ⊢ (0 − 0) = 0
305	304	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (0 − 0) = 0)
306	291, 303, 305	3eqtrd 2802	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥 ∘_f − 𝑦)‘𝑎) = 0)
307	285, 306	suppss 8236	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑦) supp 0) ⊆ (𝑥 supp 0))
308	279, 280, 281, 283, 307	fsuppsssuppgd 9398	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦) finSupp 0)
309	257, 278, 308	elrabd 3650	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
310		fvexd 6920	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))) ∈ V)
311	242, 256, 309, 310	fvmptd 7021	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → ((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦)) = (𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))))
312	224, 311	oveq12d 7458	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (((𝐹‘𝑖)‘𝑦)(._r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦))) = ((𝑖‘(𝑦 ∘ 𝐷))(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷)))))
313	312	mpteq2dva 5201	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(._r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦)))) = (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))))))
314	313	oveq2d 7456	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σ_g (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(._r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦))))) = (𝑅 Σ_g (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷)))))))
315	199, 314	eqtr4d 2801	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))))) = (𝑅 Σ_g (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(._r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦))))))
316	315	mpteq2dva 5201	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(._r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦)))))))
317		oveq2 7448	. . . . . 6 ⊢ (𝑓 = (𝑖(._r‘𝑊)𝑗) → (𝐷𝐴𝑓) = (𝐷𝐴(𝑖(._r‘𝑊)𝑗)))
318	12	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
319		simprr 785	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) → 𝑓 = (𝑖(._r‘𝑊)𝑗))
320	2, 4, 115, 6, 20, 103, 123	mplmul 22345	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑖(._r‘𝑊)𝑗) = (𝑢 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣)))))))
321	320	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) → (𝑖(._r‘𝑊)𝑗) = (𝑢 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣)))))))
322	319, 321	eqtrd 2798	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) → 𝑓 = (𝑢 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣)))))))
323	322	adantr 486	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑓 = (𝑢 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣)))))))
324		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → 𝑢 = (𝑥 ∘ 𝑑))
325		simplrl 789	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑑 = 𝐷)
326	325	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → 𝑑 = 𝐷)
327	326	coeq2d 5845	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
328	324, 327	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → 𝑢 = (𝑥 ∘ 𝐷))
329	328	breq2d 5118	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑤 ∘_r ≤ 𝑢 ↔ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)))
330	329	rabbidv 3423	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} = {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)})
331	328	fvoveq1d 7462	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑗‘(𝑢 ∘_f − 𝑣)) = (𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))
332	331	oveq2d 7456	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣))) = ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))))
333	330, 332	mpteq12dv 5195	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣)))) = (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))
334	333	oveq2d 7456	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣))))) = (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))))))
335	7	ad4antr 745	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
336	26	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝐷 ∈ 𝑃)
337	325, 336	eqeltrd 2864	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑑 ∈ 𝑃)
338		simpr 490	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
339	28, 29, 335, 337, 338	mplvrpmlem 34242	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝑑) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
340		ovexd 7475	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))))) ∈ V)
341	323, 334, 339, 340	fvmptd 7021	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))))))
342	341	mpteq2dva 5201	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))))
343	9	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑊 ∈ Ring)
344	4, 6, 343, 103, 123	ringcld 20511	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑖(._r‘𝑊)𝑗) ∈ 𝑀)
345	77	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∈ V)
346	345	mptexd 7250	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))) ∈ V)
347	318, 342, 143, 344, 346	ovmpod 7593	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐷𝐴(𝑖(._r‘𝑊)𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))))
348	317, 347	sylan9eqr 2820	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗)) → (𝐷𝐴𝑓) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))))
349	10, 348, 344, 346	fvmptd2 7022	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(._r‘𝑊)𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))))
350	28, 29, 1, 12, 7	mplvrpmga 34244	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ (𝑆 GrpAct 𝑀))
351	29	gaf 19536	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑆 GrpAct 𝑀) → 𝐴:(𝑃 × 𝑀)⟶𝑀)
352	350, 351	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴:(𝑃 × 𝑀)⟶𝑀)
353	352	fovcld 7567	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ∈ 𝑃 ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
354	353	3expa 1136	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐷 ∈ 𝑃) ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
355	354	an32s 665	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑀) ∧ 𝐷 ∈ 𝑃) → (𝐷𝐴𝑓) ∈ 𝑀)
356	26, 355	mpidan 702	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
357	356, 10	fmptd 7135	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑀⟶𝑀)
358	357	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐹:𝑀⟶𝑀)
359	358, 103	ffvelcdmd 7106	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘𝑖) ∈ 𝑀)
360	358, 123	ffvelcdmd 7106	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘𝑗) ∈ 𝑀)
361	2, 4, 115, 6, 20, 359, 360	mplmul 22345	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → ((𝐹‘𝑖)(._r‘𝑊)(𝐹‘𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(._r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦)))))))
362	316, 349, 361	3eqtr4d 2808	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(._r‘𝑊)𝑗)) = ((𝐹‘𝑖)(._r‘𝑊)(𝐹‘𝑗)))
363	362	anasss 472	. 2 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑀)) → (𝐹‘(𝑖(._r‘𝑊)𝑗)) = ((𝐹‘𝑖)(._r‘𝑊)(𝐹‘𝑗)))
364		eqid 2763	. 2 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
365	28, 29, 1, 12, 7, 10, 2, 8, 26	mplvrpmmhm 34245	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (𝑊 MndHom 𝑊))
366	365	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐹 ∈ (𝑊 MndHom 𝑊))
367	4, 364, 364	mhmlin 19014	. . . 4 ⊢ ((𝐹 ∈ (𝑊 MndHom 𝑊) ∧ 𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(+_g‘𝑊)𝑗)) = ((𝐹‘𝑖)(+_g‘𝑊)(𝐹‘𝑗)))
368	366, 103, 123, 367	syl3anc 1399	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(+_g‘𝑊)𝑗)) = ((𝐹‘𝑖)(+_g‘𝑊)(𝐹‘𝑗)))
369	368	anasss 472	. 2 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑀)) → (𝐹‘(𝑖(+_g‘𝑊)𝑗)) = ((𝐹‘𝑖)(+_g‘𝑊)(𝐹‘𝑗)))
370	4, 5, 5, 6, 6, 9, 9, 90, 363, 4, 364, 364, 357, 369	isrhmd 20749	1 ⊢ (𝜑 → 𝐹 ∈ (𝑊 RingHom 𝑊))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ∀wral 3080 {crab 3416 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ifcif 4485 {csn 4588 class class class wbr 5106 ↦ cmpt 5189 I cid 5549 × cxp 5653 ^◡ccnv 5654 ↾ cres 5657 ∘ ccom 5659 Fn wfn 6550 ⟶wf 6551 ⟶1-1wf1 6552 ⟶1-1ontowf1o 6554 ‘cfv 6555 (class class class)co 7440 ∈ cmpo 7442 ∘_f cof 7712 ∘_r cofr 7713 supp csupp 8201 ↑_m cmap 8872 finSupp cfsupp 9378 0cc0 11224 ≤ cle 11368 − cmin 11565 ℕ₀cn0 12630 Basecbs 17413 +_gcplusg 17454 ._rcmulr 17455 0_gc0g 17636 Σ_g cgsu 17637 MndHom cmhm 19002 GrpAct cga 19530 SymGrpcsymg 19610 CMndccmn 20021 1_rcur 20434 Ringcrg 20486 RingHom crh 20726 SubRingcsubrg 20848 mPwSer cmps 22239 mPoly cmpl 22241

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-isom 6564 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-of 7714 df-ofr 7715 df-om 7899 df-1st 8022 df-2nd 8023 df-supp 8202 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-2o 8502 df-er 8742 df-map 8874 df-pm 8875 df-ixp 8951 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-fsupp 9379 df-sup 9458 df-oi 9528 df-card 10044 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-nn 12360 df-2 12429 df-3 12430 df-4 12431 df-5 12432 df-6 12433 df-7 12434 df-8 12435 df-9 12436 df-n0 12631 df-z 12718 df-dec 12839 df-uz 12990 df-fz 13664 df-fzo 13813 df-seq 14169 df-hash 14499 df-struct 17351 df-sets 17368 df-slot 17386 df-ndx 17398 df-base 17414 df-ress 17435 df-plusg 17467 df-mulr 17468 df-sca 17470 df-vsca 17471 df-ip 17472 df-tset 17473 df-ple 17474 df-ds 17476 df-hom 17478 df-cco 17479 df-0g 17638 df-gsum 17639 df-prds 17644 df-pws 17646 df-mre 17782 df-mrc 17783 df-acs 17785 df-mgm 18842 df-sgrp 18934 df-mnd 18950 df-mhm 19004 df-submnd 19005 df-efmnd 19091 df-grp 19173 df-minusg 19174 df-mulg 19304 df-subg 19359 df-ghm 19454 df-ga 19531 df-cntz 19558 df-symg 19611 df-cmn 20023 df-abl 20024 df-mgp 20388 df-rng 20402 df-ur 20435 df-ring 20488 df-rhm 20729 df-subrng 20825 df-subrg 20849 df-psr 22244 df-mpl 22246

This theorem is used by: splysubrg 34259

W3C validator