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