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

Metamath Proof Explorer

Theorem mplmulmvr

Description: Multiply a polynomial F with a variable X (i.e. with a monic monomial). (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses mplmulmvr.1 ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplmulmvr.2 ⊢ 𝑋 = ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 )
mplmulmvr.3 ⊢ 𝑀 = ( Base ‘ 𝑃 )
mplmulmvr.4 ⊢ · = ( .r ‘ 𝑃 )
mplmulmvr.5 ⊢ 0 = ( 0g ‘ 𝑅 )
mplmulmvr.6 ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
mplmulmvr.7 ⊢ 𝐴 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } )
mplmulmvr.8 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mplmulmvr.9 ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
mplmulmvr.10 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mplmulmvr.11 ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
Assertion mplmulmvr ( 𝜑 → ( 𝑋 · 𝐹 ) = ( 𝑏 ∈ 𝐷 ↦ if ( ( 𝑏 ‘ 𝑌 ) = 0 , 0 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mplmulmvr.1 ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplmulmvr.2 ⊢ 𝑋 = ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 )
3 mplmulmvr.3 ⊢ 𝑀 = ( Base ‘ 𝑃 )
4 mplmulmvr.4 ⊢ · = ( .r ‘ 𝑃 )
5 mplmulmvr.5 ⊢ 0 = ( 0g ‘ 𝑅 )
6 mplmulmvr.6 ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
7 mplmulmvr.7 ⊢ 𝐴 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } )
8 mplmulmvr.8 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
9 mplmulmvr.9 ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
10 mplmulmvr.10 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
11 mplmulmvr.11 ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
12 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13 6 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
14 eqid ⊢ ( 𝐼 mVar 𝑅 ) = ( 𝐼 mVar 𝑅 )
15 1 14 3 8 10 9 mvrcl ⊢ ( 𝜑 → ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ∈ 𝑀 )
16 2 15 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ 𝑀 )
17 1 3 12 4 13 16 11 mplmul ⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) = ( 𝑏 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) ) ) )
18 eqeq2 ⊢ ( 0 = if ( ( 𝑏 ‘ 𝑌 ) = 0 , 0 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) ) → ( ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) ) = 0 ↔ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) ) = if ( ( 𝑏 ‘ 𝑌 ) = 0 , 0 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) ) ) )
19 eqeq2 ⊢ ( ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) = if ( ( 𝑏 ‘ 𝑌 ) = 0 , 0 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) ) → ( ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) ) = ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) ↔ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) ) = if ( ( 𝑏 ‘ 𝑌 ) = 0 , 0 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) ) ) )
20 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝜑 )
21 ssrab2 ⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ⊆ 𝐷
22 21 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ⊆ 𝐷 )
23 22 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑥 ∈ 𝐷 )
24 2 fveq1i ⊢ ( 𝑋 ‘ 𝑥 ) = ( ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ‘ 𝑥 )
25 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
26 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
27 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑅 ∈ Ring )
28 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑌 ∈ 𝐼 )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
30 14 13 5 25 26 27 28 29 7 mvrvalind ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ‘ 𝑥 ) = if ( 𝑥 = 𝐴 , ( 1r ‘ 𝑅 ) , 0 ) )
31 24 30 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑥 ) = if ( 𝑥 = 𝐴 , ( 1r ‘ 𝑅 ) , 0 ) )
32 20 23 31 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( 𝑋 ‘ 𝑥 ) = if ( 𝑥 = 𝐴 , ( 1r ‘ 𝑅 ) , 0 ) )
33 32 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = ( if ( 𝑥 = 𝐴 , ( 1r ‘ 𝑅 ) , 0 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) )
34 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐴 )
35 34 fveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ( 𝑥 ‘ 𝑌 ) = ( 𝐴 ‘ 𝑌 ) )
36 0ne1 ⊢ 0 ≠ 1
37 36 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → 0 ≠ 1 )
38 20 8 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝐼 ∈ 𝑉 )
39 nn0ex ⊢ ℕ0 ∈ V
40 39 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ℕ0 ∈ V )
41 6 ssrab3 ⊢ 𝐷 ⊆ ( ℕ0 ↑m 𝐼 )
42 22 41 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ⊆ ( ℕ0 ↑m 𝐼 ) )
43 42 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) )
44 38 40 43 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
45 44 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → 𝑥 : 𝐼 ⟶ ℕ0 )
46 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → 𝑌 ∈ 𝐼 )
47 45 46 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ( 𝑥 ‘ 𝑌 ) ∈ ℕ0 )
48 44 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑥 Fn 𝐼 )
49 8 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
50 39 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ℕ0 ∈ V )
51 41 a1i ⊢ ( 𝜑 → 𝐷 ⊆ ( ℕ0 ↑m 𝐼 ) )
52 51 sselda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ ( ℕ0 ↑m 𝐼 ) )
53 49 50 52 elmaprd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 : 𝐼 ⟶ ℕ0 )
54 53 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑏 : 𝐼 ⟶ ℕ0 )
55 54 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑏 Fn 𝐼 )
56 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∘r ≤ 𝑏 ↔ 𝑥 ∘r ≤ 𝑏 ) )
57 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } )
58 56 57 elrabrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑥 ∘r ≤ 𝑏 )
59 20 9 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑌 ∈ 𝐼 )
60 48 55 38 58 59 fnfvor ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( 𝑥 ‘ 𝑌 ) ≤ ( 𝑏 ‘ 𝑌 ) )
61 60 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ( 𝑥 ‘ 𝑌 ) ≤ ( 𝑏 ‘ 𝑌 ) )
62 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ( 𝑏 ‘ 𝑌 ) = 0 )
63 61 62 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ( 𝑥 ‘ 𝑌 ) ≤ 0 )
64 nn0le0eq0 ⊢ ( ( 𝑥 ‘ 𝑌 ) ∈ ℕ0 → ( ( 𝑥 ‘ 𝑌 ) ≤ 0 ↔ ( 𝑥 ‘ 𝑌 ) = 0 ) )
65 64 biimpa ⊢ ( ( ( 𝑥 ‘ 𝑌 ) ∈ ℕ0 ∧ ( 𝑥 ‘ 𝑌 ) ≤ 0 ) → ( 𝑥 ‘ 𝑌 ) = 0 )
66 47 63 65 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ( 𝑥 ‘ 𝑌 ) = 0 )
67 7 fveq1i ⊢ ( 𝐴 ‘ 𝑌 ) = ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 )
68 9 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝐼 )
69 snidg ⊢ ( 𝑌 ∈ 𝐼 → 𝑌 ∈ { 𝑌 } )
70 9 69 syl ⊢ ( 𝜑 → 𝑌 ∈ { 𝑌 } )
71 ind1 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ { 𝑌 } ⊆ 𝐼 ∧ 𝑌 ∈ { 𝑌 } ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) = 1 )
72 8 68 70 71 syl3anc ⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) ‘ 𝑌 ) = 1 )
73 67 72 eqtrid ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑌 ) = 1 )
74 73 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ( 𝐴 ‘ 𝑌 ) = 1 )
75 37 66 74 3netr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ( 𝑥 ‘ 𝑌 ) ≠ ( 𝐴 ‘ 𝑌 ) )
76 75 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ¬ ( 𝑥 ‘ 𝑌 ) = ( 𝐴 ‘ 𝑌 ) )
77 35 76 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ¬ 𝑥 = 𝐴 )
78 77 iffalsed ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → if ( 𝑥 = 𝐴 , ( 1r ‘ 𝑅 ) , 0 ) = 0 )
79 78 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( if ( 𝑥 = 𝐴 , ( 1r ‘ 𝑅 ) , 0 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = ( 0 ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) )
80 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
81 20 10 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑅 ∈ Ring )
82 1 80 3 13 11 mplelf ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
83 20 82 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
84 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑏 ∈ 𝐷 )
85 13 psrbagcon ⊢ ( ( 𝑏 ∈ 𝐷 ∧ 𝑥 : 𝐼 ⟶ ℕ0 ∧ 𝑥 ∘r ≤ 𝑏 ) → ( ( 𝑏 ∘f − 𝑥 ) ∈ 𝐷 ∧ ( 𝑏 ∘f − 𝑥 ) ∘r ≤ 𝑏 ) )
86 85 simpld ⊢ ( ( 𝑏 ∈ 𝐷 ∧ 𝑥 : 𝐼 ⟶ ℕ0 ∧ 𝑥 ∘r ≤ 𝑏 ) → ( 𝑏 ∘f − 𝑥 ) ∈ 𝐷 )
87 84 44 58 86 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( 𝑏 ∘f − 𝑥 ) ∈ 𝐷 )
88 83 87 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
89 80 12 5 81 88 ringlzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( 0 ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = 0 )
90 33 79 89 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = 0 )
91 90 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ 0 ) )
92 91 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ 0 ) ) )
93 10 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
94 93 grpmndd ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
95 94 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) → 𝑅 ∈ Mnd )
96 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
97 6 96 rab2ex ⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ∈ V
98 97 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ∈ V )
99 5 gsumz ⊢ ( ( 𝑅 ∈ Mnd ∧ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ∈ V ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ 0 ) ) = 0 )
100 95 98 99 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ 0 ) ) = 0 )
101 92 100 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ( 𝑏 ‘ 𝑌 ) = 0 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) ) = 0 )
102 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝜑 )
103 21 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ⊆ 𝐷 )
104 103 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑥 ∈ 𝐷 )
105 102 104 31 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( 𝑋 ‘ 𝑥 ) = if ( 𝑥 = 𝐴 , ( 1r ‘ 𝑅 ) , 0 ) )
106 105 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = ( if ( 𝑥 = 𝐴 , ( 1r ‘ 𝑅 ) , 0 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) )
107 ovif ⊢ ( if ( 𝑥 = 𝐴 , ( 1r ‘ 𝑅 ) , 0 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) , ( 0 ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) )
108 107 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( if ( 𝑥 = 𝐴 , ( 1r ‘ 𝑅 ) , 0 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) , ( 0 ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) )
109 102 10 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑅 ∈ Ring )
110 102 82 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
111 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑏 ∈ 𝐷 )
112 102 8 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝐼 ∈ 𝑉 )
113 39 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ℕ0 ∈ V )
114 41 104 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) )
115 112 113 114 elmaprd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
116 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } )
117 56 116 elrabrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → 𝑥 ∘r ≤ 𝑏 )
118 111 115 117 86 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( 𝑏 ∘f − 𝑥 ) ∈ 𝐷 )
119 110 118 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
120 80 12 25 109 119 ringlidmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) )
121 120 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) )
122 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑏 ∘f − 𝑥 ) = ( 𝑏 ∘f − 𝐴 ) )
123 122 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ( 𝑏 ∘f − 𝑥 ) = ( 𝑏 ∘f − 𝐴 ) )
124 123 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) = ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) )
125 121 124 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ 𝑥 = 𝐴 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) )
126 80 12 5 109 119 ringlzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( 0 ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = 0 )
127 126 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) ∧ ¬ 𝑥 = 𝐴 ) → ( 0 ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = 0 )
128 125 127 ifeq12da ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → if ( 𝑥 = 𝐴 , ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) , ( 0 ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) = if ( 𝑥 = 𝐴 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) , 0 ) )
129 106 108 128 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) = if ( 𝑥 = 𝐴 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) , 0 ) )
130 129 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ if ( 𝑥 = 𝐴 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) , 0 ) ) )
131 130 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ if ( 𝑥 = 𝐴 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) , 0 ) ) ) )
132 94 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → 𝑅 ∈ Mnd )
133 97 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ∈ V )
134 breq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∘r ≤ 𝑏 ↔ 𝐴 ∘r ≤ 𝑏 ) )
135 breq1 ⊢ ( ℎ = 𝐴 → ( ℎ finSupp 0 ↔ 𝐴 finSupp 0 ) )
136 39 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
137 indf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ { 𝑌 } ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) : 𝐼 ⟶ { 0 , 1 } )
138 8 68 137 syl2anc ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) : 𝐼 ⟶ { 0 , 1 } )
139 7 feq1i ⊢ ( 𝐴 : 𝐼 ⟶ { 0 , 1 } ↔ ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) : 𝐼 ⟶ { 0 , 1 } )
140 138 139 sylibr ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ { 0 , 1 } )
141 0nn0 ⊢ 0 ∈ ℕ0
142 141 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
143 1nn0 ⊢ 1 ∈ ℕ0
144 143 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
145 142 144 prssd ⊢ ( 𝜑 → { 0 , 1 } ⊆ ℕ0 )
146 140 145 fssd ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ ℕ0 )
147 136 8 146 elmapdd ⊢ ( 𝜑 → 𝐴 ∈ ( ℕ0 ↑m 𝐼 ) )
148 146 ffund ⊢ ( 𝜑 → Fun 𝐴 )
149 7 oveq1i ⊢ ( 𝐴 supp 0 ) = ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) supp 0 )
150 indsupp ⊢ ( ( 𝐼 ∈ 𝑉 ∧ { 𝑌 } ⊆ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) supp 0 ) = { 𝑌 } )
151 8 68 150 syl2anc ⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) supp 0 ) = { 𝑌 } )
152 149 151 eqtrid ⊢ ( 𝜑 → ( 𝐴 supp 0 ) = { 𝑌 } )
153 snfi ⊢ { 𝑌 } ∈ Fin
154 152 153 eqeltrdi ⊢ ( 𝜑 → ( 𝐴 supp 0 ) ∈ Fin )
155 147 142 148 154 isfsuppd ⊢ ( 𝜑 → 𝐴 finSupp 0 )
156 135 147 155 elrabd ⊢ ( 𝜑 → 𝐴 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
157 156 6 eleqtrrdi ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
158 157 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → 𝐴 ∈ 𝐷 )
159 breq1 ⊢ ( 1 = if ( 𝑢 ∈ { 𝑌 } , 1 , 0 ) → ( 1 ≤ ( 𝑏 ‘ 𝑢 ) ↔ if ( 𝑢 ∈ { 𝑌 } , 1 , 0 ) ≤ ( 𝑏 ‘ 𝑢 ) ) )
160 breq1 ⊢ ( 0 = if ( 𝑢 ∈ { 𝑌 } , 1 , 0 ) → ( 0 ≤ ( 𝑏 ‘ 𝑢 ) ↔ if ( 𝑢 ∈ { 𝑌 } , 1 , 0 ) ≤ ( 𝑏 ‘ 𝑢 ) ) )
161 53 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → 𝑏 : 𝐼 ⟶ ℕ0 )
162 161 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) → ( 𝑏 ‘ 𝑢 ) ∈ ℕ0 )
163 162 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) ∧ 𝑢 ∈ { 𝑌 } ) → ( 𝑏 ‘ 𝑢 ) ∈ ℕ0 )
164 elsni ⊢ ( 𝑢 ∈ { 𝑌 } → 𝑢 = 𝑌 )
165 164 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) ∧ 𝑢 ∈ { 𝑌 } ) → 𝑢 = 𝑌 )
166 165 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) ∧ 𝑢 ∈ { 𝑌 } ) → ( 𝑏 ‘ 𝑢 ) = ( 𝑏 ‘ 𝑌 ) )
167 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) ∧ 𝑢 ∈ { 𝑌 } ) → ¬ ( 𝑏 ‘ 𝑌 ) = 0 )
168 167 neqned ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) ∧ 𝑢 ∈ { 𝑌 } ) → ( 𝑏 ‘ 𝑌 ) ≠ 0 )
169 166 168 eqnetrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) ∧ 𝑢 ∈ { 𝑌 } ) → ( 𝑏 ‘ 𝑢 ) ≠ 0 )
170 elnnne0 ⊢ ( ( 𝑏 ‘ 𝑢 ) ∈ ℕ ↔ ( ( 𝑏 ‘ 𝑢 ) ∈ ℕ0 ∧ ( 𝑏 ‘ 𝑢 ) ≠ 0 ) )
171 163 169 170 sylanbrc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) ∧ 𝑢 ∈ { 𝑌 } ) → ( 𝑏 ‘ 𝑢 ) ∈ ℕ )
172 171 nnge1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) ∧ 𝑢 ∈ { 𝑌 } ) → 1 ≤ ( 𝑏 ‘ 𝑢 ) )
173 162 nn0ge0d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) → 0 ≤ ( 𝑏 ‘ 𝑢 ) )
174 173 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) ∧ ¬ 𝑢 ∈ { 𝑌 } ) → 0 ≤ ( 𝑏 ‘ 𝑢 ) )
175 159 160 172 174 ifbothda ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) → if ( 𝑢 ∈ { 𝑌 } , 1 , 0 ) ≤ ( 𝑏 ‘ 𝑢 ) )
176 175 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → ∀ 𝑢 ∈ 𝐼 if ( 𝑢 ∈ { 𝑌 } , 1 , 0 ) ≤ ( 𝑏 ‘ 𝑢 ) )
177 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → 𝐼 ∈ 𝑉 )
178 143 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) → 1 ∈ ℕ0 )
179 141 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) → 0 ∈ ℕ0 )
180 178 179 ifexd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) → if ( 𝑢 ∈ { 𝑌 } , 1 , 0 ) ∈ V )
181 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) ∧ 𝑢 ∈ 𝐼 ) → ( 𝑏 ‘ 𝑢 ) ∈ V )
182 indval ⊢ ( ( 𝐼 ∈ 𝑉 ∧ { 𝑌 } ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) = ( 𝑢 ∈ 𝐼 ↦ if ( 𝑢 ∈ { 𝑌 } , 1 , 0 ) ) )
183 8 68 182 syl2anc ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑌 } ) = ( 𝑢 ∈ 𝐼 ↦ if ( 𝑢 ∈ { 𝑌 } , 1 , 0 ) ) )
184 7 183 eqtrid ⊢ ( 𝜑 → 𝐴 = ( 𝑢 ∈ 𝐼 ↦ if ( 𝑢 ∈ { 𝑌 } , 1 , 0 ) ) )
185 184 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → 𝐴 = ( 𝑢 ∈ 𝐼 ↦ if ( 𝑢 ∈ { 𝑌 } , 1 , 0 ) ) )
186 53 feqmptd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 = ( 𝑢 ∈ 𝐼 ↦ ( 𝑏 ‘ 𝑢 ) ) )
187 186 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → 𝑏 = ( 𝑢 ∈ 𝐼 ↦ ( 𝑏 ‘ 𝑢 ) ) )
188 177 180 181 185 187 ofrfval2 ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → ( 𝐴 ∘r ≤ 𝑏 ↔ ∀ 𝑢 ∈ 𝐼 if ( 𝑢 ∈ { 𝑌 } , 1 , 0 ) ≤ ( 𝑏 ‘ 𝑢 ) ) )
189 176 188 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → 𝐴 ∘r ≤ 𝑏 )
190 134 158 189 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → 𝐴 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } )
191 eqid ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ if ( 𝑥 = 𝐴 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) , 0 ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ if ( 𝑥 = 𝐴 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) , 0 ) )
192 82 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
193 simplr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → 𝑏 ∈ 𝐷 )
194 146 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → 𝐴 : 𝐼 ⟶ ℕ0 )
195 13 psrbagcon ⊢ ( ( 𝑏 ∈ 𝐷 ∧ 𝐴 : 𝐼 ⟶ ℕ0 ∧ 𝐴 ∘r ≤ 𝑏 ) → ( ( 𝑏 ∘f − 𝐴 ) ∈ 𝐷 ∧ ( 𝑏 ∘f − 𝐴 ) ∘r ≤ 𝑏 ) )
196 195 simpld ⊢ ( ( 𝑏 ∈ 𝐷 ∧ 𝐴 : 𝐼 ⟶ ℕ0 ∧ 𝐴 ∘r ≤ 𝑏 ) → ( 𝑏 ∘f − 𝐴 ) ∈ 𝐷 )
197 193 194 189 196 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → ( 𝑏 ∘f − 𝐴 ) ∈ 𝐷 )
198 192 197 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) ∈ ( Base ‘ 𝑅 ) )
199 5 132 133 190 191 198 gsummptif1n0 ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ if ( 𝑥 = 𝐴 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) , 0 ) ) ) = ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) )
200 131 199 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) ∧ ¬ ( 𝑏 ‘ 𝑌 ) = 0 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) ) = ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) )
201 18 19 101 200 ifbothda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) ) = if ( ( 𝑏 ‘ 𝑌 ) = 0 , 0 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) ) )
202 201 mpteq2dva ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑏 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏 ∘f − 𝑥 ) ) ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ if ( ( 𝑏 ‘ 𝑌 ) = 0 , 0 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) ) ) )
203 17 202 eqtrd ⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) = ( 𝑏 ∈ 𝐷 ↦ if ( ( 𝑏 ‘ 𝑌 ) = 0 , 0 , ( 𝐹 ‘ ( 𝑏 ∘f − 𝐴 ) ) ) ) )