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 33558

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 6825	. . 3 ⊢ (Base‘𝑊) = (Base‘(𝐼 mPoly 𝑅))
4	1, 3	eqtr4i 2755	. 2 ⊢ 𝑀 = (Base‘𝑊)
5		eqid 2729	. 2 ⊢ (1_r‘𝑊) = (1_r‘𝑊)
6		eqid 2729	. 2 ⊢ (._r‘𝑊) = (._r‘𝑊)
7		mplvrpmga.5	. . 3 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
8		mplvrpmmhm.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ Ring)
9	2, 7, 8	mplringd 21930	. 2 ⊢ (𝜑 → 𝑊 ∈ Ring)
10		mplvrpmmhm.f	. . 3 ⊢ 𝐹 = (𝑓 ∈ 𝑀 ↦ (𝐷𝐴𝑓))
11		oveq2 7357	. . . 4 ⊢ (𝑓 = (1_r‘𝑊) → (𝐷𝐴𝑓) = (𝐷𝐴(1_r‘𝑊)))
12		mplvrpmga.4	. . . . . . 7 ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))
13	12	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
14		simpr 484	. . . . . . . . . 10 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊)) → 𝑓 = (1_r‘𝑊))
15		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊)) → 𝑑 = 𝐷)
16	15	coeq2d 5805	. . . . . . . . . 10 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊)) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
17	14, 16	fveq12d 6829	. . . . . . . . 9 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊)) → (𝑓‘(𝑥 ∘ 𝑑)) = ((1_r‘𝑊)‘(𝑥 ∘ 𝐷)))
18	17	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = ((1_r‘𝑊)‘(𝑥 ∘ 𝐷)))
19		eqid 2729	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}
20	19	psrbasfsupp 33553	. . . . . . . . . . . 12 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}
21		eqid 2729	. . . . . . . . . . . 12 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
22		eqid 2729	. . . . . . . . . . . 12 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
23	2, 20, 21, 22, 5, 7, 8	mpl1 21919	. . . . . . . . . . 11 ⊢ (𝜑 → (1_r‘𝑊) = (𝑦 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑦 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅))))
24	23	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (1_r‘𝑊) = (𝑦 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑦 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅))))
25		eqeq1 2733	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥 ∘ 𝐷) → (𝑦 = (𝐼 × {0}) ↔ (𝑥 ∘ 𝐷) = (𝐼 × {0})))
26		mplvrpmmhm.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
27	26	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝐷 ∈ 𝑃)
28		mplvrpmga.1	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (SymGrp‘𝐼)
29		mplvrpmga.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑃 = (Base‘𝑆)
30	28, 29	symgbasf1o 19254	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ 𝑃 → 𝐷:𝐼–1-1-onto→𝐼)
31		f1ococnv2 6791	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷:𝐼–1-1-onto→𝐼 → (𝐷 ∘ ^◡𝐷) = ( I ↾ 𝐼))
32	27, 30, 31	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝐷 ∘ ^◡𝐷) = ( I ↾ 𝐼))
33	32	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝐷 ∘ ^◡𝐷) = ( I ↾ 𝐼))
34	33	coeq2d 5805	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ (𝐷 ∘ ^◡𝐷)) = (𝑥 ∘ ( I ↾ 𝐼)))
35		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = (𝐼 × {0}))
36	35	coeq1d 5804	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝑥 ∘ 𝐷) ∘ ^◡𝐷) = ((𝐼 × {0}) ∘ ^◡𝐷))
37		coass 6214	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∘ 𝐷) ∘ ^◡𝐷) = (𝑥 ∘ (𝐷 ∘ ^◡𝐷))
38	37	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝑥 ∘ 𝐷) ∘ ^◡𝐷) = (𝑥 ∘ (𝐷 ∘ ^◡𝐷)))
39	26, 30	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷:𝐼–1-1-onto→𝐼)
40		f1ocnv 6776	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷:𝐼–1-1-onto→𝐼 → ^◡𝐷:𝐼–1-1-onto→𝐼)
41		f1of 6764	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐷:𝐼–1-1-onto→𝐼 → ^◡𝐷:𝐼⟶𝐼)
42	39, 40, 41	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ^◡𝐷:𝐼⟶𝐼)
43		0nn0 12399	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℕ₀
44	43	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℕ₀)
45	42, 44	constcof 32573	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐼 × {0}) ∘ ^◡𝐷) = (𝐼 × {0}))
46	45	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → ((𝐼 × {0}) ∘ ^◡𝐷) = (𝐼 × {0}))
47	36, 38, 46	3eqtr3d 2772	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ (𝐷 ∘ ^◡𝐷)) = (𝐼 × {0}))
48	7	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
49		nn0ex 12390	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ₀ ∈ V
50	49	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → ℕ₀ ∈ V)
51		ssrab2 4031	. . . . . . . . . . . . . . . . . 18 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ₀ ↑_m 𝐼)
52		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
53	51, 52	sselid 3933	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ (ℕ₀ ↑_m 𝐼))
54	48, 50, 53	elmaprd 32630	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑥:𝐼⟶ℕ₀)
55		fcoi1 6698	. . . . . . . . . . . . . . . 16 ⊢ (𝑥:𝐼⟶ℕ₀ → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
56	54, 55	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
57	56	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
58	34, 47, 57	3eqtr3rd 2773	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ (𝑥 ∘ 𝐷) = (𝐼 × {0})) → 𝑥 = (𝐼 × {0}))
59		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → 𝑥 = (𝐼 × {0}))
60	59	coeq1d 5804	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = ((𝐼 × {0}) ∘ 𝐷))
61		f1of 6764	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷:𝐼–1-1-onto→𝐼 → 𝐷:𝐼⟶𝐼)
62	26, 30, 61	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷:𝐼⟶𝐼)
63	62, 44	constcof 32573	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐼 × {0}) ∘ 𝐷) = (𝐼 × {0}))
64	63	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → ((𝐼 × {0}) ∘ 𝐷) = (𝐼 × {0}))
65	60, 64	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 = (𝐼 × {0})) → (𝑥 ∘ 𝐷) = (𝐼 × {0}))
66	58, 65	impbida 800	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → ((𝑥 ∘ 𝐷) = (𝐼 × {0}) ↔ 𝑥 = (𝐼 × {0})))
67	25, 66	sylan9bbr 510	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 = (𝑥 ∘ 𝐷)) → (𝑦 = (𝐼 × {0}) ↔ 𝑥 = (𝐼 × {0})))
68	67	ifbid 4500	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 = (𝑥 ∘ 𝐷)) → if(𝑦 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅)) = if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅)))
69	28, 29, 48, 27, 52	mplvrpmlem 33554	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝐷) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
70		fvexd 6837	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (1_r‘𝑅) ∈ V)
71		fvexd 6837	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (0_g‘𝑅) ∈ V)
72	70, 71	ifcld 4523	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅)) ∈ V)
73	24, 68, 69, 72	fvmptd 6937	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → ((1_r‘𝑊)‘(𝑥 ∘ 𝐷)) = if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅)))
74	73	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → ((1_r‘𝑊)‘(𝑥 ∘ 𝐷)) = if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅)))
75	18, 74	eqtrd 2764	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅)))
76	75	mpteq2dva 5185	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 = 𝐷 ∧ 𝑓 = (1_r‘𝑊))) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅))))
77	4, 5, 9	ringidcld 20151	. . . . . 6 ⊢ (𝜑 → (1_r‘𝑊) ∈ 𝑀)
78		ovex 7382	. . . . . . . . 9 ⊢ (ℕ₀ ↑_m 𝐼) ∈ V
79	78	rabex 5278	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∈ V
80	79	a1i 11	. . . . . . 7 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∈ V)
81	80	mptexd 7160	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅))) ∈ V)
82	13, 76, 26, 77, 81	ovmpod 7501	. . . . 5 ⊢ (𝜑 → (𝐷𝐴(1_r‘𝑊)) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅))))
83		eqid 2729	. . . . . 6 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
84		eqid 2729	. . . . . 6 ⊢ (1_r‘(𝐼 mPwSer 𝑅)) = (1_r‘(𝐼 mPwSer 𝑅))
85	83, 7, 8, 20, 21, 22, 84	psr1 21878	. . . . 5 ⊢ (𝜑 → (1_r‘(𝐼 mPwSer 𝑅)) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ if(𝑥 = (𝐼 × {0}), (1_r‘𝑅), (0_g‘𝑅))))
86	83, 2, 4, 7, 8	mplsubrg 21912	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (SubRing‘(𝐼 mPwSer 𝑅)))
87	2, 83, 4	mplval2 21903	. . . . . . 7 ⊢ 𝑊 = ((𝐼 mPwSer 𝑅) ↾_s 𝑀)
88	87, 84	subrg1 20467	. . . . . 6 ⊢ (𝑀 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → (1_r‘(𝐼 mPwSer 𝑅)) = (1_r‘𝑊))
89	86, 88	syl 17	. . . . 5 ⊢ (𝜑 → (1_r‘(𝐼 mPwSer 𝑅)) = (1_r‘𝑊))
90	82, 85, 89	3eqtr2d 2770	. . . 4 ⊢ (𝜑 → (𝐷𝐴(1_r‘𝑊)) = (1_r‘𝑊))
91	11, 90	sylan9eqr 2786	. . 3 ⊢ ((𝜑 ∧ 𝑓 = (1_r‘𝑊)) → (𝐷𝐴𝑓) = (1_r‘𝑊))
92	10, 91, 77, 77	fvmptd2 6938	. 2 ⊢ (𝜑 → (𝐹‘(1_r‘𝑊)) = (1_r‘𝑊))
93		nfcv 2891	. . . . . . 7 ⊢ Ⅎ𝑣((𝑖‘(𝑦 ∘ 𝐷))(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))))
94		eqid 2729	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘𝑅)
95		fveq2 6822	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → (𝑖‘𝑣) = (𝑖‘(𝑦 ∘ 𝐷)))
96		oveq2 7357	. . . . . . . . 9 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → ((𝑥 ∘ 𝐷) ∘_f − 𝑣) = ((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷)))
97	96	fveq2d 6826	. . . . . . . 8 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → (𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)) = (𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))))
98	95, 97	oveq12d 7367	. . . . . . 7 ⊢ (𝑣 = (𝑦 ∘ 𝐷) → ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))) = ((𝑖‘(𝑦 ∘ 𝐷))(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷)))))
99	8	ringcmnd 20169	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ CMnd)
100	99	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑅 ∈ CMnd)
101	79	rabex 5278	. . . . . . . 8 ⊢ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ∈ V
102	101	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ∈ V)
103		eqid 2729	. . . . . . . . . . . 12 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
104	2, 83, 4, 103	mplbasss 21904	. . . . . . . . . . . . . 14 ⊢ 𝑀 ⊆ (Base‘(𝐼 mPwSer 𝑅))
105		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑖 ∈ 𝑀)
106	104, 105	sselid 3933	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑖 ∈ (Base‘(𝐼 mPwSer 𝑅)))
107	106	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 ∈ (Base‘(𝐼 mPwSer 𝑅)))
108	83, 94, 20, 103, 107	psrelbas 21841	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑖:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
109	108	feqmptd 6891	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 = (𝑣 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘𝑣)))
110	105	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 ∈ 𝑀)
111	2, 4, 21, 110	mplelsfi 21902	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑖 finSupp (0_g‘𝑅))
112	109, 111	eqbrtrrd 5116	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘𝑣)) finSupp (0_g‘𝑅))
113		ssrab2 4031	. . . . . . . . . 10 ⊢ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ⊆ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}
114	113	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ⊆ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
115		fvexd 6837	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (0_g‘𝑅) ∈ V)
116	112, 114, 115	fmptssfisupp 9284	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ (𝑖‘𝑣)) finSupp (0_g‘𝑅))
117		eqid 2729	. . . . . . . . 9 ⊢ (._r‘𝑅) = (._r‘𝑅)
118	8	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑛 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring)
119		simpr 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑛 ∈ (Base‘𝑅)) → 𝑛 ∈ (Base‘𝑅))
120	94, 117, 21, 118, 119	ringlzd 20180	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑛 ∈ (Base‘𝑅)) → ((0_g‘𝑅)(._r‘𝑅)𝑛) = (0_g‘𝑅))
121	108	adantr 480	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑖:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
122		elrabi 3643	. . . . . . . . . 10 ⊢ (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} → 𝑣 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
123	122	adantl 481	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
124	121, 123	ffvelcdmd 7019	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑖‘𝑣) ∈ (Base‘𝑅))
125		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑗 ∈ 𝑀)
126	104, 125	sselid 3933	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑗 ∈ (Base‘(𝐼 mPwSer 𝑅)))
127	126	ad2antrr 726	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑗 ∈ (Base‘(𝐼 mPwSer 𝑅)))
128	83, 94, 20, 103, 127	psrelbas 21841	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑗:{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
129	69	ad5ant14 757	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ 𝐷) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
130	7	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝐼 ∈ 𝑉)
131	49	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ℕ₀ ∈ V)
132	51, 123	sselid 3933	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∈ (ℕ₀ ↑_m 𝐼))
133	130, 131, 132	elmaprd 32630	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣:𝐼⟶ℕ₀)
134		breq1 5095	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑤 ∘_r ≤ (𝑥 ∘ 𝐷) ↔ 𝑣 ∘_r ≤ (𝑥 ∘ 𝐷)))
135		simpr 484	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)})
136	134, 135	elrabrd 32447	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 ∘_r ≤ (𝑥 ∘ 𝐷))
137	20	psrbagcon 21832	. . . . . . . . . . 11 ⊢ (((𝑥 ∘ 𝐷) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∧ 𝑣:𝐼⟶ℕ₀ ∧ 𝑣 ∘_r ≤ (𝑥 ∘ 𝐷)) → (((𝑥 ∘ 𝐷) ∘_f − 𝑣) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∧ ((𝑥 ∘ 𝐷) ∘_f − 𝑣) ∘_r ≤ (𝑥 ∘ 𝐷)))
138	129, 133, 136, 137	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (((𝑥 ∘ 𝐷) ∘_f − 𝑣) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∧ ((𝑥 ∘ 𝐷) ∘_f − 𝑣) ∘_r ≤ (𝑥 ∘ 𝐷)))
139	138	simpld 494	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ((𝑥 ∘ 𝐷) ∘_f − 𝑣) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
140	128, 139	ffvelcdmd 7019	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)) ∈ (Base‘𝑅))
141	116, 120, 124, 140, 115	fsuppssov1 9274	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))) finSupp (0_g‘𝑅))
142		ssidd 3959	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (Base‘𝑅) ⊆ (Base‘𝑅))
143	8	ad4antr 732	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑅 ∈ Ring)
144	94, 117, 143, 124, 140	ringcld 20145	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))) ∈ (Base‘𝑅))
145		breq1 5095	. . . . . . . 8 ⊢ (𝑤 = (𝑦 ∘ 𝐷) → (𝑤 ∘_r ≤ (𝑥 ∘ 𝐷) ↔ (𝑦 ∘ 𝐷) ∘_r ≤ (𝑥 ∘ 𝐷)))
146	7	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝐼 ∈ 𝑉)
147	26	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐷 ∈ 𝑃)
148	147	ad2antrr 726	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝐷 ∈ 𝑃)
149		ssrab2 4031	. . . . . . . . . . 11 ⊢ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ⊆ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}
150		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥})
151	149, 150	sselid 3933	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
152	151	adantlr 715	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
153	28, 29, 146, 148, 152	mplvrpmlem 33554	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
154	49	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → ℕ₀ ∈ V)
155	51	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ₀ ↑_m 𝐼))
156	149, 155	sstrid 3947	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ⊆ (ℕ₀ ↑_m 𝐼))
157	156	sselda 3935	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 ∈ (ℕ₀ ↑_m 𝐼))
158	146, 154, 157	elmaprd 32630	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦:𝐼⟶ℕ₀)
159	158	ffnd 6653	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 Fn 𝐼)
160	54	ad4ant14 752	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑥:𝐼⟶ℕ₀)
161	160	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑥:𝐼⟶ℕ₀)
162	161	ffnd 6653	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑥 Fn 𝐼)
163	62	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝐷:𝐼⟶𝐼)
164		breq1 5095	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → (𝑧 ∘_r ≤ 𝑥 ↔ 𝑦 ∘_r ≤ 𝑥))
165		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥})
166	164, 165	elrabrd 32447	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦 ∘_r ≤ 𝑥)
167	159, 162, 163, 146, 146, 166	ofrco 32562	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∘_r ≤ (𝑥 ∘ 𝐷))
168	145, 153, 167	elrabd 3650	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑦 ∘ 𝐷) ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)})
169		breq1 5095	. . . . . . . . 9 ⊢ (𝑧 = (𝑣 ∘ ^◡𝐷) → (𝑧 ∘_r ≤ 𝑥 ↔ (𝑣 ∘ ^◡𝐷) ∘_r ≤ 𝑥))
170		breq1 5095	. . . . . . . . . 10 ⊢ (ℎ = (𝑣 ∘ ^◡𝐷) → (ℎ finSupp 0 ↔ (𝑣 ∘ ^◡𝐷) finSupp 0))
171	42	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ^◡𝐷:𝐼⟶𝐼)
172	133, 171	fcod 6677	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷):𝐼⟶ℕ₀)
173	131, 130, 172	elmapdd 8768	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷) ∈ (ℕ₀ ↑_m 𝐼))
174		breq1 5095	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑣 → (ℎ finSupp 0 ↔ 𝑣 finSupp 0))
175	174, 123	elrabrd 32447	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 finSupp 0)
176	39	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝐷:𝐼–1-1-onto→𝐼)
177		f1of1 6763	. . . . . . . . . . . 12 ⊢ (^◡𝐷:𝐼–1-1-onto→𝐼 → ^◡𝐷:𝐼–1-1→𝐼)
178	176, 40, 177	3syl 18	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ^◡𝐷:𝐼–1-1→𝐼)
179	43	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 0 ∈ ℕ₀)
180	175, 178, 179, 123	fsuppco 9292	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷) finSupp 0)
181	170, 173, 180	elrabd 3650	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
182	133	ffnd 6653	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑣 Fn 𝐼)
183	160	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑥:𝐼⟶ℕ₀)
184	183	ffnd 6653	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝑥 Fn 𝐼)
185	62	ad4antr 732	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → 𝐷:𝐼⟶𝐼)
186		fnfco 6689	. . . . . . . . . . . 12 ⊢ ((𝑥 Fn 𝐼 ∧ 𝐷:𝐼⟶𝐼) → (𝑥 ∘ 𝐷) Fn 𝐼)
187	184, 185, 186	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ 𝐷) Fn 𝐼)
188	182, 187, 171, 130, 130, 136	ofrco 32562	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷) ∘_r ≤ ((𝑥 ∘ 𝐷) ∘ ^◡𝐷))
189	176, 31	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝐷 ∘ ^◡𝐷) = ( I ↾ 𝐼))
190	189	coeq2d 5805	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ (𝐷 ∘ ^◡𝐷)) = (𝑥 ∘ ( I ↾ 𝐼)))
191	183, 55	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
192	190, 191	eqtrd 2764	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑥 ∘ (𝐷 ∘ ^◡𝐷)) = 𝑥)
193	37, 192	eqtrid 2776	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ((𝑥 ∘ 𝐷) ∘ ^◡𝐷) = 𝑥)
194	188, 193	breqtrd 5118	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷) ∘_r ≤ 𝑥)
195	169, 181, 194	elrabd 3650	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → (𝑣 ∘ ^◡𝐷) ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥})
196	133	adantr 480	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑣:𝐼⟶ℕ₀)
197	158	adantlr 715	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑦:𝐼⟶ℕ₀)
198	39	ad5antr 734	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝐷:𝐼–1-1-onto→𝐼)
199	196, 197, 198	cocnvf1o 32681	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑣 = (𝑦 ∘ 𝐷) ↔ 𝑦 = (𝑣 ∘ ^◡𝐷)))
200	195, 199	reu6dv 32421	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)}) → ∃!𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}𝑣 = (𝑦 ∘ 𝐷))
201	93, 94, 21, 98, 100, 102, 141, 142, 144, 168, 200	gsummptfsf1o 33016	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))))) = (𝑅 Σ_g (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷)))))))
202		coeq1 5800	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑦 → (𝑡 ∘ 𝐷) = (𝑦 ∘ 𝐷))
203	202	fveq2d 6826	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → (𝑖‘(𝑡 ∘ 𝐷)) = (𝑖‘(𝑦 ∘ 𝐷)))
204		oveq2 7357	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑖 → (𝐷𝐴𝑓) = (𝐷𝐴𝑖))
205	105	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑖 ∈ 𝑀)
206		ovexd 7384	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝐷𝐴𝑖) ∈ V)
207	10, 204, 205, 206	fvmptd3 6953	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝐹‘𝑖) = (𝐷𝐴𝑖))
208	12	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
209		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → 𝑓 = 𝑖)
210		coeq2 5801	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝐷 → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
211	210	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
212	209, 211	fveq12d 6829	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑖‘(𝑥 ∘ 𝐷)))
213	212	mpteq2dv 5186	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑥 ∘ 𝐷))))
214		coeq1 5800	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (𝑥 ∘ 𝐷) = (𝑡 ∘ 𝐷))
215	214	fveq2d 6826	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑡 → (𝑖‘(𝑥 ∘ 𝐷)) = (𝑖‘(𝑡 ∘ 𝐷)))
216	215	cbvmptv 5196	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑥 ∘ 𝐷))) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷)))
217	213, 216	eqtrdi 2780	. . . . . . . . . . . . . 14 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑖) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
218	217	adantl 481	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ (𝑑 = 𝐷 ∧ 𝑓 = 𝑖)) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
219	147	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝐷 ∈ 𝑃)
220	79	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∈ V)
221	220	mptexd 7160	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))) ∈ V)
222	208, 218, 219, 205, 221	ovmpod 7501	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝐷𝐴𝑖) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
223	207, 222	eqtrd 2764	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝐹‘𝑖) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑖‘(𝑡 ∘ 𝐷))))
224		fvexd 6837	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑖‘(𝑦 ∘ 𝐷)) ∈ V)
225	203, 223, 151, 224	fvmptd4 6954	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → ((𝐹‘𝑖)‘𝑦) = (𝑖‘(𝑦 ∘ 𝐷)))
226	225	adantlr 715	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → ((𝐹‘𝑖)‘𝑦) = (𝑖‘(𝑦 ∘ 𝐷)))
227		oveq2 7357	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑗 → (𝐷𝐴𝑓) = (𝐷𝐴𝑗))
228		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → 𝑓 = 𝑗)
229	210	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
230	228, 229	fveq12d 6829	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑗‘(𝑥 ∘ 𝐷)))
231	230	mpteq2dv 5186	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑥 ∘ 𝐷))))
232	214	fveq2d 6826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑡 → (𝑗‘(𝑥 ∘ 𝐷)) = (𝑗‘(𝑡 ∘ 𝐷)))
233	232	cbvmptv 5196	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑥 ∘ 𝐷))) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷)))
234	231, 233	eqtrdi 2780	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 = 𝐷 ∧ 𝑓 = 𝑗) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
235	234	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ (𝑑 = 𝐷 ∧ 𝑓 = 𝑗)) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
236		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑗 ∈ 𝑀)
237	220	mptexd 7160	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))) ∈ V)
238	208, 235, 219, 236, 237	ovmpod 7501	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝐷𝐴𝑗) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
239	227, 238	sylan9eqr 2786	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑓 = 𝑗) → (𝐷𝐴𝑓) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
240	239	adantllr 719	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑓 = 𝑗) → (𝐷𝐴𝑓) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
241	125	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑗 ∈ 𝑀)
242	79	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∈ V)
243	242	mptexd 7160	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))) ∈ V)
244	10, 240, 241, 243	fvmptd2 6938	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝐹‘𝑗) = (𝑡 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑗‘(𝑡 ∘ 𝐷))))
245		coeq1 5800	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑥 ∘_f − 𝑦) → (𝑡 ∘ 𝐷) = ((𝑥 ∘_f − 𝑦) ∘ 𝐷))
246	245	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑥 ∘_f − 𝑦) → (𝑗‘(𝑡 ∘ 𝐷)) = (𝑗‘((𝑥 ∘_f − 𝑦) ∘ 𝐷)))
247	246	adantl 481	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → (𝑗‘(𝑡 ∘ 𝐷)) = (𝑗‘((𝑥 ∘_f − 𝑦) ∘ 𝐷)))
248	160	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝑥:𝐼⟶ℕ₀)
249	248	ffnd 6653	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝑥 Fn 𝐼)
250	7	ad5antr 734	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝐼 ∈ 𝑉)
251	49	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → ℕ₀ ∈ V)
252	157	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝑦 ∈ (ℕ₀ ↑_m 𝐼))
253	250, 251, 252	elmaprd 32630	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝑦:𝐼⟶ℕ₀)
254	253	ffnd 6653	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝑦 Fn 𝐼)
255	62	ad5antr 734	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → 𝐷:𝐼⟶𝐼)
256		inidm 4178	. . . . . . . . . . . . 13 ⊢ (𝐼 ∩ 𝐼) = 𝐼
257	249, 254, 255, 250, 250, 250, 256	ofco 7638	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → ((𝑥 ∘_f − 𝑦) ∘ 𝐷) = ((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷)))
258	257	fveq2d 6826	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → (𝑗‘((𝑥 ∘_f − 𝑦) ∘ 𝐷)) = (𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))))
259	247, 258	eqtrd 2764	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑡 = (𝑥 ∘_f − 𝑦)) → (𝑗‘(𝑡 ∘ 𝐷)) = (𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))))
260		breq1 5095	. . . . . . . . . . 11 ⊢ (ℎ = (𝑥 ∘_f − 𝑦) → (ℎ finSupp 0 ↔ (𝑥 ∘_f − 𝑦) finSupp 0))
261	162, 159, 146, 146, 256	offn 7626	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦) Fn 𝐼)
262	162	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑥 Fn 𝐼)
263	159	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑦 Fn 𝐼)
264	146	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝐼 ∈ 𝑉)
265		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑎 ∈ 𝐼)
266		fnfvof 7630	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 Fn 𝐼 ∧ 𝑦 Fn 𝐼) ∧ (𝐼 ∈ 𝑉 ∧ 𝑎 ∈ 𝐼)) → ((𝑥 ∘_f − 𝑦)‘𝑎) = ((𝑥‘𝑎) − (𝑦‘𝑎)))
267	262, 263, 264, 265, 266	syl22anc 838	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → ((𝑥 ∘_f − 𝑦)‘𝑎) = ((𝑥‘𝑎) − (𝑦‘𝑎)))
268	158	ffvelcdmda 7018	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑦‘𝑎) ∈ ℕ₀)
269	161	ffvelcdmda 7018	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑥‘𝑎) ∈ ℕ₀)
270		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥})
271	164, 270	elrabrd 32447	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → 𝑦 ∘_r ≤ 𝑥)
272	263, 262, 264, 271, 265	fnfvor 32561	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → (𝑦‘𝑎) ≤ (𝑥‘𝑎))
273		nn0sub 12434	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦‘𝑎) ∈ ℕ₀ ∧ (𝑥‘𝑎) ∈ ℕ₀) → ((𝑦‘𝑎) ≤ (𝑥‘𝑎) ↔ ((𝑥‘𝑎) − (𝑦‘𝑎)) ∈ ℕ₀))
274	273	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦‘𝑎) ∈ ℕ₀ ∧ (𝑥‘𝑎) ∈ ℕ₀) ∧ (𝑦‘𝑎) ≤ (𝑥‘𝑎)) → ((𝑥‘𝑎) − (𝑦‘𝑎)) ∈ ℕ₀)
275	268, 269, 272, 274	syl21anc 837	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → ((𝑥‘𝑎) − (𝑦‘𝑎)) ∈ ℕ₀)
276	267, 275	eqeltrd 2828	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ 𝐼) → ((𝑥 ∘_f − 𝑦)‘𝑎) ∈ ℕ₀)
277	276	ralrimiva 3121	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → ∀𝑎 ∈ 𝐼 ((𝑥 ∘_f − 𝑦)‘𝑎) ∈ ℕ₀)
278		ffnfv 7053	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∘_f − 𝑦):𝐼⟶ℕ₀ ↔ ((𝑥 ∘_f − 𝑦) Fn 𝐼 ∧ ∀𝑎 ∈ 𝐼 ((𝑥 ∘_f − 𝑦)‘𝑎) ∈ ℕ₀))
279	261, 277, 278	sylanbrc 583	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦):𝐼⟶ℕ₀)
280	154, 146, 279	elmapdd 8768	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦) ∈ (ℕ₀ ↑_m 𝐼))
281		ovexd 7384	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦) ∈ V)
282	43	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 0 ∈ ℕ₀)
283	162, 159, 146, 146	offun 7627	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → Fun (𝑥 ∘_f − 𝑦))
284	20	psrbagfsupp 21826	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} → 𝑥 finSupp 0)
285	284	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → 𝑥 finSupp 0)
286		dffn2 6654	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∘_f − 𝑦) Fn 𝐼 ↔ (𝑥 ∘_f − 𝑦):𝐼⟶V)
287	261, 286	sylib 218	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦):𝐼⟶V)
288	162	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑥 Fn 𝐼)
289	159	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦 Fn 𝐼)
290	146	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝐼 ∈ 𝑉)
291		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0)))
292	291	eldifad 3915	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑎 ∈ 𝐼)
293	288, 289, 290, 292, 266	syl22anc 838	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥 ∘_f − 𝑦)‘𝑎) = ((𝑥‘𝑎) − (𝑦‘𝑎)))
294	43	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 0 ∈ ℕ₀)
295	288, 290, 294, 291	fvdifsupp 8104	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑥‘𝑎) = 0)
296	158	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦:𝐼⟶ℕ₀)
297	296, 292	ffvelcdmd 7019	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ∈ ℕ₀)
298		simplr 768	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥})
299	164, 298	elrabrd 32447	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → 𝑦 ∘_r ≤ 𝑥)
300	289, 288, 290, 299, 292	fnfvor 32561	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ≤ (𝑥‘𝑎))
301	300, 295	breqtrd 5118	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) ≤ 0)
302		nn0le0eq0 12412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦‘𝑎) ∈ ℕ₀ → ((𝑦‘𝑎) ≤ 0 ↔ (𝑦‘𝑎) = 0))
303	302	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦‘𝑎) ∈ ℕ₀ ∧ (𝑦‘𝑎) ≤ 0) → (𝑦‘𝑎) = 0)
304	297, 301, 303	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (𝑦‘𝑎) = 0)
305	295, 304	oveq12d 7367	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥‘𝑎) − (𝑦‘𝑎)) = (0 − 0))
306		0m0e0 12243	. . . . . . . . . . . . . . 15 ⊢ (0 − 0) = 0
307	306	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → (0 − 0) = 0)
308	293, 305, 307	3eqtrd 2768	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) ∧ 𝑎 ∈ (𝐼 ∖ (𝑥 supp 0))) → ((𝑥 ∘_f − 𝑦)‘𝑎) = 0)
309	287, 308	suppss 8127	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → ((𝑥 ∘_f − 𝑦) supp 0) ⊆ (𝑥 supp 0))
310	281, 282, 283, 285, 309	fsuppsssuppgd 9272	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦) finSupp 0)
311	260, 280, 310	elrabd 3650	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑥 ∘_f − 𝑦) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
312		fvexd 6837	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))) ∈ V)
313	244, 259, 311, 312	fvmptd 6937	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → ((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦)) = (𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))))
314	226, 313	oveq12d 7367	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥}) → (((𝐹‘𝑖)‘𝑦)(._r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦))) = ((𝑖‘(𝑦 ∘ 𝐷))(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷)))))
315	314	mpteq2dva 5185	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(._r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦)))) = (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷))))))
316	315	oveq2d 7365	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σ_g (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(._r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦))))) = (𝑅 Σ_g (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ ((𝑖‘(𝑦 ∘ 𝐷))(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − (𝑦 ∘ 𝐷)))))))
317	201, 316	eqtr4d 2767	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))))) = (𝑅 Σ_g (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(._r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦))))))
318	317	mpteq2dva 5185	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(._r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦)))))))
319		oveq2 7357	. . . . . 6 ⊢ (𝑓 = (𝑖(._r‘𝑊)𝑗) → (𝐷𝐴𝑓) = (𝐷𝐴(𝑖(._r‘𝑊)𝑗)))
320	12	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
321		simprr 772	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) → 𝑓 = (𝑖(._r‘𝑊)𝑗))
322	2, 4, 117, 6, 20, 105, 125	mplmul 21918	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑖(._r‘𝑊)𝑗) = (𝑢 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣)))))))
323	322	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) → (𝑖(._r‘𝑊)𝑗) = (𝑢 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣)))))))
324	321, 323	eqtrd 2764	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) → 𝑓 = (𝑢 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣)))))))
325	324	adantr 480	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑓 = (𝑢 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣)))))))
326		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → 𝑢 = (𝑥 ∘ 𝑑))
327		simplrl 776	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑑 = 𝐷)
328	327	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → 𝑑 = 𝐷)
329	328	coeq2d 5805	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝐷))
330	326, 329	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → 𝑢 = (𝑥 ∘ 𝐷))
331	330	breq2d 5104	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑤 ∘_r ≤ 𝑢 ↔ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)))
332	331	rabbidv 3402	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} = {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)})
333	330	fvoveq1d 7371	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑗‘(𝑢 ∘_f − 𝑣)) = (𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))
334	333	oveq2d 7365	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣))) = ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))))
335	332, 334	mpteq12dv 5179	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣)))) = (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))
336	335	oveq2d 7365	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑢 = (𝑥 ∘ 𝑑)) → (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ 𝑢} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘(𝑢 ∘_f − 𝑣))))) = (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))))))
337	7	ad4antr 732	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
338	26	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝐷 ∈ 𝑃)
339	327, 338	eqeltrd 2828	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑑 ∈ 𝑃)
340		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
341	28, 29, 337, 339, 340	mplvrpmlem 33554	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝑑) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
342		ovexd 7384	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))))) ∈ V)
343	325, 336, 341, 342	fvmptd 6937	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣))))))
344	343	mpteq2dva 5185	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ (𝑑 = 𝐷 ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗))) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))))
345	9	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝑊 ∈ Ring)
346	4, 6, 345, 105, 125	ringcld 20145	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑖(._r‘𝑊)𝑗) ∈ 𝑀)
347	79	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∈ V)
348	347	mptexd 7160	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))) ∈ V)
349	320, 344, 147, 346, 348	ovmpod 7501	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐷𝐴(𝑖(._r‘𝑊)𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))))
350	319, 349	sylan9eqr 2786	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) ∧ 𝑓 = (𝑖(._r‘𝑊)𝑗)) → (𝐷𝐴𝑓) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))))
351	10, 350, 346, 348	fvmptd2 6938	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(._r‘𝑊)𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑣 ∈ {𝑤 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑤 ∘_r ≤ (𝑥 ∘ 𝐷)} ↦ ((𝑖‘𝑣)(._r‘𝑅)(𝑗‘((𝑥 ∘ 𝐷) ∘_f − 𝑣)))))))
352	28, 29, 1, 12, 7	mplvrpmga 33556	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ (𝑆 GrpAct 𝑀))
353	29	gaf 19174	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑆 GrpAct 𝑀) → 𝐴:(𝑃 × 𝑀)⟶𝑀)
354	352, 353	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴:(𝑃 × 𝑀)⟶𝑀)
355	354	fovcld 7476	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ∈ 𝑃 ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
356	355	3expa 1118	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐷 ∈ 𝑃) ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
357	356	an32s 652	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝑀) ∧ 𝐷 ∈ 𝑃) → (𝐷𝐴𝑓) ∈ 𝑀)
358	26, 357	mpidan 689	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑀) → (𝐷𝐴𝑓) ∈ 𝑀)
359	358, 10	fmptd 7048	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝑀⟶𝑀)
360	359	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐹:𝑀⟶𝑀)
361	360, 105	ffvelcdmd 7019	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘𝑖) ∈ 𝑀)
362	360, 125	ffvelcdmd 7019	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘𝑗) ∈ 𝑀)
363	2, 4, 117, 6, 20, 361, 362	mplmul 21918	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → ((𝐹‘𝑖)(._r‘𝑊)(𝐹‘𝑗)) = (𝑥 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑅 Σ_g (𝑦 ∈ {𝑧 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∣ 𝑧 ∘_r ≤ 𝑥} ↦ (((𝐹‘𝑖)‘𝑦)(._r‘𝑅)((𝐹‘𝑗)‘(𝑥 ∘_f − 𝑦)))))))
364	318, 351, 363	3eqtr4d 2774	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(._r‘𝑊)𝑗)) = ((𝐹‘𝑖)(._r‘𝑊)(𝐹‘𝑗)))
365	364	anasss 466	. 2 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑀)) → (𝐹‘(𝑖(._r‘𝑊)𝑗)) = ((𝐹‘𝑖)(._r‘𝑊)(𝐹‘𝑗)))
366		eqid 2729	. 2 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
367	28, 29, 1, 12, 7, 10, 2, 8, 26	mplvrpmmhm 33557	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (𝑊 MndHom 𝑊))
368	367	ad2antrr 726	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑀) ∧ 𝑗 ∈ 𝑀) → 𝐹 ∈ (𝑊 MndHom 𝑊))
369	4, 366, 366	mhmlin 18667	. . . 4 ⊢ ((𝐹 ∈ (𝑊 MndHom 𝑊) ∧ 𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑀) → (𝐹‘(𝑖(+_g‘𝑊)𝑗)) = ((𝐹‘𝑖)(+_g‘𝑊)(𝐹‘𝑗)))
370	368, 105, 125, 369	syl3anc 1373	. . 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 20373	1 ⊢ (𝜑 → 𝐹 ∈ (𝑊 RingHom 𝑊))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3044 {crab 3394 Vcvv 3436 ∖ cdif 3900 ⊆ wss 3903 ifcif 4476 {csn 4577 class class class wbr 5092 ↦ cmpt 5173 I cid 5513 × cxp 5617 ^◡ccnv 5618 ↾ cres 5621 ∘ ccom 5623 Fn wfn 6477 ⟶wf 6478 –1-1→wf1 6479 –1-1-onto→wf1o 6481 ‘cfv 6482 (class class class)co 7349 ∈ cmpo 7351 ∘_f cof 7611 ∘_r cofr 7612 supp csupp 8093 ↑_m cmap 8753 finSupp cfsupp 9251 0cc0 11009 ≤ cle 11150 − cmin 11347 ℕ₀cn0 12384 Basecbs 17120 +_gcplusg 17161 ._rcmulr 17162 0_gc0g 17343 Σ_g cgsu 17344 MndHom cmhm 18655 GrpAct cga 19168 SymGrpcsymg 19248 CMndccmn 19659 1_rcur 20066 Ringcrg 20118 RingHom crh 20354 SubRingcsubrg 20454 mPwSer cmps 21811 mPoly cmpl 21813

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-of 7613 df-ofr 7614 df-om 7800 df-1st 7924 df-2nd 7925 df-supp 8094 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-er 8625 df-map 8755 df-pm 8756 df-ixp 8825 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-fsupp 9252 df-sup 9332 df-oi 9402 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-z 12472 df-dec 12592 df-uz 12736 df-fz 13411 df-fzo 13558 df-seq 13909 df-hash 14238 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-hom 17185 df-cco 17186 df-0g 17345 df-gsum 17346 df-prds 17351 df-pws 17353 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18514 df-sgrp 18593 df-mnd 18609 df-mhm 18657 df-submnd 18658 df-efmnd 18743 df-grp 18815 df-minusg 18816 df-mulg 18947 df-subg 19002 df-ghm 19092 df-ga 19169 df-cntz 19196 df-symg 19249 df-cmn 19661 df-abl 19662 df-mgp 20026 df-rng 20038 df-ur 20067 df-ring 20120 df-rhm 20357 df-subrng 20431 df-subrg 20455 df-psr 21816 df-mpl 21818

This theorem is referenced by: splysubrg 33562

W3C validator