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