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

Metamath Proof Explorer

Theorem mplvrpmmhm

Description: The action of permuting variables in a multivariate polynomial is a monoid homomorphism. (Contributed by Thierry Arnoux, 11-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 mplvrpmmhm ( 𝜑 → 𝐹 ∈ ( 𝑊 MndHom 𝑊 ) )

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 ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
13 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
14 7 5 8 mplringd ⊢ ( 𝜑 → 𝑊 ∈ Ring )
15 14 ringgrpd ⊢ ( 𝜑 → 𝑊 ∈ Grp )
16 15 grpmndd ⊢ ( 𝜑 → 𝑊 ∈ Mnd )
17 1 2 3 4 5 mplvrpmga ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 GrpAct 𝑀 ) )
18 2 gaf ⊢ ( 𝐴 ∈ ( 𝑆 GrpAct 𝑀 ) → 𝐴 : ( 𝑃 × 𝑀 ) ⟶ 𝑀 )
19 17 18 syl ⊢ ( 𝜑 → 𝐴 : ( 𝑃 × 𝑀 ) ⟶ 𝑀 )
20 19 fovcld ⊢ ( ( 𝜑 ∧ 𝐷 ∈ 𝑃 ∧ 𝑓 ∈ 𝑀 ) → ( 𝐷 𝐴 𝑓 ) ∈ 𝑀 )
21 20 3expa ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝐷 𝐴 𝑓 ) ∈ 𝑀 )
22 21 an32s ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑀 ) ∧ 𝐷 ∈ 𝑃 ) → ( 𝐷 𝐴 𝑓 ) ∈ 𝑀 )
23 9 22 mpidan ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑀 ) → ( 𝐷 𝐴 𝑓 ) ∈ 𝑀 )
24 23 6 fmptd ⊢ ( 𝜑 → 𝐹 : 𝑀 ⟶ 𝑀 )
25 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
26 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
27 26 psrbasfsupp ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
28 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → 𝑖 ∈ 𝑀 )
29 7 25 11 27 28 mplelf ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → 𝑖 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
30 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑖 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
31 30 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑖 Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
32 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → 𝑗 ∈ 𝑀 )
33 7 25 11 27 32 mplelf ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → 𝑗 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
34 33 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑗 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
35 34 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑗 Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
36 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
37 36 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V
38 37 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V )
39 breq1 ⊢ ( ℎ = ( 𝑥 ∘ 𝐷 ) → ( ℎ finSupp 0 ↔ ( 𝑥 ∘ 𝐷 ) finSupp 0 ) )
40 nn0ex ⊢ ℕ0 ∈ V
41 40 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ℕ0 ∈ V )
42 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐼 ∈ 𝑉 )
43 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐼 ∈ 𝑉 )
44 40 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ℕ0 ∈ V )
45 breq1 ⊢ ( ℎ = 𝑥 → ( ℎ finSupp 0 ↔ 𝑥 finSupp 0 ) )
46 45 elrab ⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↔ ( 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∧ 𝑥 finSupp 0 ) )
47 46 biimpi ⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } → ( 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∧ 𝑥 finSupp 0 ) )
48 47 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∧ 𝑥 finSupp 0 ) )
49 48 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) )
50 43 44 49 elmaprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
51 50 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
52 1 2 symgbasf1o ⊢ ( 𝐷 ∈ 𝑃 → 𝐷 : 𝐼 –1-1-onto→ 𝐼 )
53 9 52 syl ⊢ ( 𝜑 → 𝐷 : 𝐼 –1-1-onto→ 𝐼 )
54 f1of ⊢ ( 𝐷 : 𝐼 –1-1-onto→ 𝐼 → 𝐷 : 𝐼 ⟶ 𝐼 )
55 53 54 syl ⊢ ( 𝜑 → 𝐷 : 𝐼 ⟶ 𝐼 )
56 55 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐷 : 𝐼 ⟶ 𝐼 )
57 51 56 fcod ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝐷 ) : 𝐼 ⟶ ℕ0 )
58 41 42 57 elmapdd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝐷 ) ∈ ( ℕ0 ↑m 𝐼 ) )
59 48 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 finSupp 0 )
60 53 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐷 : 𝐼 –1-1-onto→ 𝐼 )
61 f1of1 ⊢ ( 𝐷 : 𝐼 –1-1-onto→ 𝐼 → 𝐷 : 𝐼 –1-1→ 𝐼 )
62 60 61 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐷 : 𝐼 –1-1→ 𝐼 )
63 0nn0 ⊢ 0 ∈ ℕ0
64 63 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 0 ∈ ℕ0 )
65 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
66 59 62 64 65 fsuppco ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝐷 ) finSupp 0 )
67 66 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝐷 ) finSupp 0 )
68 39 58 67 elrabd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝐷 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
69 fnfvof ⊢ ( ( ( 𝑖 Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∧ 𝑗 Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V ∧ ( 𝑥 ∘ 𝐷 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) ) → ( ( 𝑖 ∘f ( +g ‘ 𝑅 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) = ( ( 𝑖 ‘ ( 𝑥 ∘ 𝐷 ) ) ( +g ‘ 𝑅 ) ( 𝑗 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
70 31 35 38 68 69 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( 𝑖 ∘f ( +g ‘ 𝑅 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) = ( ( 𝑖 ‘ ( 𝑥 ∘ 𝐷 ) ) ( +g ‘ 𝑅 ) ( 𝑗 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
71 oveq2 ⊢ ( 𝑓 = 𝑖 → ( 𝐷 𝐴 𝑓 ) = ( 𝐷 𝐴 𝑖 ) )
72 4 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) )
73 simpr ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑓 = 𝑖 ) → 𝑓 = 𝑖 )
74 coeq2 ⊢ ( 𝑑 = 𝐷 → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝐷 ) )
75 74 adantr ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑓 = 𝑖 ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝐷 ) )
76 73 75 fveq12d ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑓 = 𝑖 ) → ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) = ( 𝑖 ‘ ( 𝑥 ∘ 𝐷 ) ) )
77 76 mpteq2dv ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑓 = 𝑖 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑖 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
78 77 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ ( 𝑑 = 𝐷 ∧ 𝑓 = 𝑖 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑖 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
79 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → 𝐷 ∈ 𝑃 )
80 37 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V )
81 80 mptexd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑖 ‘ ( 𝑥 ∘ 𝐷 ) ) ) ∈ V )
82 72 78 79 28 81 ovmpod ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐷 𝐴 𝑖 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑖 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
83 71 82 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑓 = 𝑖 ) → ( 𝐷 𝐴 𝑓 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑖 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
84 6 83 28 81 fvmptd2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐹 ‘ 𝑖 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑖 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
85 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑖 ‘ ( 𝑥 ∘ 𝐷 ) ) ∈ V )
86 84 85 fvmpt2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) = ( 𝑖 ‘ ( 𝑥 ∘ 𝐷 ) ) )
87 oveq2 ⊢ ( 𝑓 = 𝑗 → ( 𝐷 𝐴 𝑓 ) = ( 𝐷 𝐴 𝑗 ) )
88 simpr ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑓 = 𝑗 ) → 𝑓 = 𝑗 )
89 74 adantr ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑓 = 𝑗 ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝐷 ) )
90 88 89 fveq12d ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑓 = 𝑗 ) → ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) = ( 𝑗 ‘ ( 𝑥 ∘ 𝐷 ) ) )
91 90 mpteq2dv ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑓 = 𝑗 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑗 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
92 91 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ ( 𝑑 = 𝐷 ∧ 𝑓 = 𝑗 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑗 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
93 80 mptexd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑗 ‘ ( 𝑥 ∘ 𝐷 ) ) ) ∈ V )
94 72 92 79 32 93 ovmpod ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐷 𝐴 𝑗 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑗 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
95 87 94 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑓 = 𝑗 ) → ( 𝐷 𝐴 𝑓 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑗 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
96 6 95 32 93 fvmptd2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑗 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
97 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑗 ‘ ( 𝑥 ∘ 𝐷 ) ) ∈ V )
98 96 97 fvmpt2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) = ( 𝑗 ‘ ( 𝑥 ∘ 𝐷 ) ) )
99 86 98 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) = ( ( 𝑖 ‘ ( 𝑥 ∘ 𝐷 ) ) ( +g ‘ 𝑅 ) ( 𝑗 ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
100 70 99 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( 𝑖 ∘f ( +g ‘ 𝑅 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) = ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
101 100 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝑖 ∘f ( +g ‘ 𝑅 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) )
102 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → 𝐹 : 𝑀 ⟶ 𝑀 )
103 102 28 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐹 ‘ 𝑖 ) ∈ 𝑀 )
104 7 25 11 27 103 mplelf ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐹 ‘ 𝑖 ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
105 104 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐹 ‘ 𝑖 ) Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
106 102 32 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑀 )
107 7 25 11 27 106 mplelf ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐹 ‘ 𝑗 ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
108 107 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐹 ‘ 𝑗 ) Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
109 80 105 108 offvalfv ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( ( 𝐹 ‘ 𝑖 ) ∘f ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑗 ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( ( 𝐹 ‘ 𝑖 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) )
110 101 109 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝑖 ∘f ( +g ‘ 𝑅 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) = ( ( 𝐹 ‘ 𝑖 ) ∘f ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑗 ) ) )
111 oveq2 ⊢ ( 𝑓 = ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) → ( 𝐷 𝐴 𝑓 ) = ( 𝐷 𝐴 ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ) )
112 simpr ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑓 = ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ) → 𝑓 = ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) )
113 74 adantr ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑓 = ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝐷 ) )
114 112 113 fveq12d ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑓 = ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ) → ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) = ( ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) )
115 114 mpteq2dv ⊢ ( ( 𝑑 = 𝐷 ∧ 𝑓 = ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
116 115 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ ( 𝑑 = 𝐷 ∧ 𝑓 = ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
117 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → 𝑊 ∈ Grp )
118 11 12 117 28 32 grpcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ∈ 𝑀 )
119 80 mptexd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) ∈ V )
120 72 116 79 118 119 ovmpod ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐷 𝐴 ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
121 111 120 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑓 = ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ) → ( 𝐷 𝐴 𝑓 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
122 6 121 118 119 fvmptd2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐹 ‘ ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
123 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
124 7 11 123 12 28 32 mpladd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) = ( 𝑖 ∘f ( +g ‘ 𝑅 ) 𝑗 ) )
125 124 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) = ( ( 𝑖 ∘f ( +g ‘ 𝑅 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) )
126 125 mpteq2dv ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝑖 ∘f ( +g ‘ 𝑅 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
127 122 126 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐹 ‘ ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 𝑖 ∘f ( +g ‘ 𝑅 ) 𝑗 ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
128 7 11 123 12 103 106 mpladd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( ( 𝐹 ‘ 𝑖 ) ( +g ‘ 𝑊 ) ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝐹 ‘ 𝑖 ) ∘f ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑗 ) ) )
129 110 127 128 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) ∧ 𝑗 ∈ 𝑀 ) → ( 𝐹 ‘ ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ) = ( ( 𝐹 ‘ 𝑖 ) ( +g ‘ 𝑊 ) ( 𝐹 ‘ 𝑗 ) ) )
130 129 anasss ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑖 ( +g ‘ 𝑊 ) 𝑗 ) ) = ( ( 𝐹 ‘ 𝑖 ) ( +g ‘ 𝑊 ) ( 𝐹 ‘ 𝑗 ) ) )
131 simpr ⊢ ( ( 𝜑 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) → 𝑓 = ( 0g ‘ 𝑊 ) )
132 131 oveq2d ⊢ ( ( 𝜑 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) → ( 𝐷 𝐴 𝑓 ) = ( 𝐷 𝐴 ( 0g ‘ 𝑊 ) ) )
133 4 a1i ⊢ ( 𝜑 → 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) )
134 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑑 = 𝐷 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑓 = ( 0g ‘ 𝑊 ) )
135 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
136 8 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
137 7 27 135 13 5 136 mpl0 ⊢ ( 𝜑 → ( 0g ‘ 𝑊 ) = ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) )
138 137 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑑 = 𝐷 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 0g ‘ 𝑊 ) = ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) )
139 134 138 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑑 = 𝐷 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑓 = ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) )
140 74 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐷 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝐷 ) )
141 140 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑑 = 𝐷 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝐷 ) )
142 139 141 fveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑑 = 𝐷 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) = ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝑥 ∘ 𝐷 ) ) )
143 142 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐷 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) )
144 55 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐷 : 𝐼 ⟶ 𝐼 )
145 50 144 fcod ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝐷 ) : 𝐼 ⟶ ℕ0 )
146 44 43 145 elmapdd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝐷 ) ∈ ( ℕ0 ↑m 𝐼 ) )
147 39 146 66 elrabd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝐷 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
148 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
149 148 fvconst2 ⊢ ( ( 𝑥 ∘ 𝐷 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } → ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝑥 ∘ 𝐷 ) ) = ( 0g ‘ 𝑅 ) )
150 147 149 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝑥 ∘ 𝐷 ) ) = ( 0g ‘ 𝑅 ) )
151 150 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 0g ‘ 𝑅 ) ) )
152 fconstmpt ⊢ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 0g ‘ 𝑅 ) )
153 137 152 eqtrdi ⊢ ( 𝜑 → ( 0g ‘ 𝑊 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 0g ‘ 𝑅 ) ) )
154 151 153 eqtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) = ( 0g ‘ 𝑊 ) )
155 154 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐷 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝑥 ∘ 𝐷 ) ) ) = ( 0g ‘ 𝑊 ) )
156 143 155 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑑 = 𝐷 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 0g ‘ 𝑊 ) )
157 11 13 grpidcl ⊢ ( 𝑊 ∈ Grp → ( 0g ‘ 𝑊 ) ∈ 𝑀 )
158 15 157 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑊 ) ∈ 𝑀 )
159 133 156 9 158 158 ovmpod ⊢ ( 𝜑 → ( 𝐷 𝐴 ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
160 159 adantr ⊢ ( ( 𝜑 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) → ( 𝐷 𝐴 ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
161 132 160 eqtrd ⊢ ( ( 𝜑 ∧ 𝑓 = ( 0g ‘ 𝑊 ) ) → ( 𝐷 𝐴 𝑓 ) = ( 0g ‘ 𝑊 ) )
162 6 161 158 158 fvmptd2 ⊢ ( 𝜑 → ( 𝐹 ‘ ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
163 11 11 12 12 13 13 16 16 24 130 162 ismhmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑊 MndHom 𝑊 ) )