This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mplvrpmrhm

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

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

Proof

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