Metamath Proof Explorer

Theorem psrmonmul

Description: The product of two power series monomials adds the exponent vectors together. For example, the product of ( x ^ 2 ) ( y ^ 2 ) with ( y ^ 1 ) ( z ^ 3 ) is ( x ^ 2 ) ( y ^ 3 ) ( z ^ 3 ) , where the exponent vectors <. 2 , 2 , 0 >. and <. 0 , 1 , 3 >. are added to give <. 2 , 3 , 3 >. . (Contributed by Thierry Arnoux, 16-Mar-2026)

Ref Expression
Hypotheses psrmon.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrmon.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psrmon.z ⊢ 0 = ( 0g ‘ 𝑅 )
psrmon.o ⊢ 1 = ( 1r ‘ 𝑅 )
psrmon.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
psrmon.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
psrmon.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
psrmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
psrmonmul.t ⊢ · = ( .r ‘ 𝑆 )
psrmonmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
Assertion psrmonmul ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 psrmon.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrmon.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psrmon.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 psrmon.o ⊢ 1 = ( 1r ‘ 𝑅 )
5 psrmon.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
6 psrmon.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
7 psrmon.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
8 psrmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
9 psrmonmul.t ⊢ · = ( .r ‘ 𝑆 )
10 psrmonmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
11 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
12 5 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
13 1 2 3 4 5 6 7 8 psrmon ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ 𝐵 )
14 1 2 3 4 5 6 7 10 psrmon ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ∈ 𝐵 )
15 1 2 11 9 12 13 14 psrmulfval ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) )
16 eqeq1 ⊢ ( 𝑦 = 𝑘 → ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) ↔ 𝑘 = ( 𝑋 ∘f + 𝑌 ) ) )
17 16 ifbid ⊢ ( 𝑦 = 𝑘 → if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) = if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
18 17 cbvmptv ⊢ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) = ( 𝑘 ∈ 𝐷 ↦ if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
19 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
20 19 snssd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → { 𝑋 } ⊆ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
21 20 resmptd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) = ( 𝑗 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) )
22 21 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑅 Σg ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) )
23 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring )
24 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
25 23 24 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Mnd )
26 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑋 ∈ 𝐷 )
27 iftrue ⊢ ( 𝑦 = 𝑋 → if ( 𝑦 = 𝑋 , 1 , 0 ) = 1 )
28 eqid ⊢ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) )
29 4 fvexi ⊢ 1 ∈ V
30 27 28 29 fvmpt ⊢ ( 𝑋 ∈ 𝐷 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) = 1 )
31 26 30 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) = 1 )
32 ssrab2 ⊢ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ⊆ 𝐷
33 eqid ⊢ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } = { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 }
34 12 33 psrbagconcl ⊢ ( ( 𝑘 ∈ 𝐷 ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑋 ) ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
35 34 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑋 ) ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
36 32 35 sselid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑋 ) ∈ 𝐷 )
37 eqeq1 ⊢ ( 𝑦 = ( 𝑘 ∘f − 𝑋 ) → ( 𝑦 = 𝑌 ↔ ( 𝑘 ∘f − 𝑋 ) = 𝑌 ) )
38 37 ifbid ⊢ ( 𝑦 = ( 𝑘 ∘f − 𝑋 ) → if ( 𝑦 = 𝑌 , 1 , 0 ) = if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) )
39 eqid ⊢ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) )
40 3 fvexi ⊢ 0 ∈ V
41 29 40 ifex ⊢ if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) ∈ V
42 38 39 41 fvmpt ⊢ ( ( 𝑘 ∘f − 𝑋 ) ∈ 𝐷 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) = if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) )
43 36 42 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) = if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) )
44 31 43 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) = ( 1 ( .r ‘ 𝑅 ) if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) ) )
45 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
46 45 4 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
47 45 3 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
48 46 47 ifcld ⊢ ( 𝑅 ∈ Ring → if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
49 23 48 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
50 45 11 4 23 49 ringlidmd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 1 ( .r ‘ 𝑅 ) if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) ) = if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) )
51 12 psrbagf ⊢ ( 𝑘 ∈ 𝐷 → 𝑘 : 𝐼 ⟶ ℕ0 )
52 51 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑘 : 𝐼 ⟶ ℕ0 )
53 52 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑘 ‘ 𝑧 ) ∈ ℕ0 )
54 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑋 ∈ 𝐷 )
55 12 psrbagf ⊢ ( 𝑋 ∈ 𝐷 → 𝑋 : 𝐼 ⟶ ℕ0 )
56 54 55 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑋 : 𝐼 ⟶ ℕ0 )
57 56 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑧 ) ∈ ℕ0 )
58 57 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑧 ) ∈ ℕ0 )
59 12 psrbagf ⊢ ( 𝑌 ∈ 𝐷 → 𝑌 : 𝐼 ⟶ ℕ0 )
60 10 59 syl ⊢ ( 𝜑 → 𝑌 : 𝐼 ⟶ ℕ0 )
61 60 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑌 : 𝐼 ⟶ ℕ0 )
62 61 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 )
63 62 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 )
64 nn0cn ⊢ ( ( 𝑘 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑘 ‘ 𝑧 ) ∈ ℂ )
65 nn0cn ⊢ ( ( 𝑋 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑋 ‘ 𝑧 ) ∈ ℂ )
66 nn0cn ⊢ ( ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑌 ‘ 𝑧 ) ∈ ℂ )
67 subadd ⊢ ( ( ( 𝑘 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝑋 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝑌 ‘ 𝑧 ) ∈ ℂ ) → ( ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) ↔ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) = ( 𝑘 ‘ 𝑧 ) ) )
68 64 65 66 67 syl3an ⊢ ( ( ( 𝑘 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑋 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 ) → ( ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) ↔ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) = ( 𝑘 ‘ 𝑧 ) ) )
69 53 58 63 68 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) ↔ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) = ( 𝑘 ‘ 𝑧 ) ) )
70 eqcom ⊢ ( ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) = ( 𝑘 ‘ 𝑧 ) ↔ ( 𝑘 ‘ 𝑧 ) = ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) )
71 69 70 bitrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) ↔ ( 𝑘 ‘ 𝑧 ) = ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) )
72 71 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ∀ 𝑧 ∈ 𝐼 ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑘 ‘ 𝑧 ) = ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) )
73 mpteqb ⊢ ( ∀ 𝑧 ∈ 𝐼 ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ∈ V → ( ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐼 ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) ) )
74 ovexd ⊢ ( 𝑧 ∈ 𝐼 → ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ∈ V )
75 73 74 mprg ⊢ ( ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐼 ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) )
76 mpteqb ⊢ ( ∀ 𝑧 ∈ 𝐼 ( 𝑘 ‘ 𝑧 ) ∈ V → ( ( 𝑧 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑧 ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑘 ‘ 𝑧 ) = ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) )
77 fvexd ⊢ ( 𝑧 ∈ 𝐼 → ( 𝑘 ‘ 𝑧 ) ∈ V )
78 76 77 mprg ⊢ ( ( 𝑧 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑧 ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑘 ‘ 𝑧 ) = ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) )
79 72 75 78 3bitr4g ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) ↔ ( 𝑧 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑧 ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) ) )
80 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝐼 ∈ 𝑊 )
81 52 feqmptd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑘 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑧 ) ) )
82 56 feqmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑋 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑧 ) ) )
83 82 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑋 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑧 ) ) )
84 80 53 58 81 83 offval2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑋 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) )
85 61 feqmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑌 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) )
86 85 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑌 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) )
87 84 86 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 ↔ ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) ) )
88 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝐼 ∈ 𝑊 )
89 88 57 62 82 85 offval2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑋 ∘f + 𝑌 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) )
90 89 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑋 ∘f + 𝑌 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) )
91 81 90 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) ↔ ( 𝑧 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑧 ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) ) )
92 79 87 91 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 ↔ 𝑘 = ( 𝑋 ∘f + 𝑌 ) ) )
93 92 ifbid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) = if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
94 44 50 93 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) = if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
95 93 49 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
96 94 95 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) ∈ ( Base ‘ 𝑅 ) )
97 fveq2 ⊢ ( 𝑗 = 𝑋 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) )
98 oveq2 ⊢ ( 𝑗 = 𝑋 → ( 𝑘 ∘f − 𝑗 ) = ( 𝑘 ∘f − 𝑋 ) )
99 98 fveq2d ⊢ ( 𝑗 = 𝑋 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) )
100 97 99 oveq12d ⊢ ( 𝑗 = 𝑋 → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) = ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) )
101 45 100 gsumsn ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑋 ∈ 𝐷 ∧ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 Σg ( 𝑗 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) = ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) )
102 25 26 96 101 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑅 Σg ( 𝑗 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) = ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) )
103 22 102 94 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑅 Σg ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) ) = if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
104 3 gsum0 ⊢ ( 𝑅 Σg ∅ ) = 0
105 disjsn ⊢ ( ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
106 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring )
107 1 45 12 2 13 psrelbas ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
108 107 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
109 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
110 32 109 sselid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑗 ∈ 𝐷 )
111 108 110 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
112 1 45 12 2 14 psrelbas ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
113 112 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
114 12 33 psrbagconcl ⊢ ( ( 𝑘 ∈ 𝐷 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑗 ) ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
115 114 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑗 ) ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
116 32 115 sselid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑗 ) ∈ 𝐷 )
117 113 116 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
118 45 11 106 111 117 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) )
119 118 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ⟶ ( Base ‘ 𝑅 ) )
120 ffn ⊢ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ⟶ ( Base ‘ 𝑅 ) → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) Fn { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
121 fnresdisj ⊢ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) Fn { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } → ( ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∩ { 𝑋 } ) = ∅ ↔ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) = ∅ ) )
122 119 120 121 3syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∩ { 𝑋 } ) = ∅ ↔ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) = ∅ ) )
123 122 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∩ { 𝑋 } ) = ∅ ) → ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) = ∅ )
124 105 123 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ ¬ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) = ∅ )
125 124 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ ¬ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑅 Σg ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) ) = ( 𝑅 Σg ∅ ) )
126 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) ↔ 𝑋 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) ) )
127 57 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑧 ) ∈ ℝ )
128 nn0addge1 ⊢ ( ( ( 𝑋 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 ) → ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) )
129 127 62 128 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) )
130 129 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ∀ 𝑧 ∈ 𝐼 ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) )
131 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ∈ V )
132 88 57 131 82 89 ofrfval2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑋 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) )
133 130 132 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑋 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) )
134 126 54 133 elrabd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) } )
135 breq2 ⊢ ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) → ( 𝑥 ∘r ≤ 𝑘 ↔ 𝑥 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) ) )
136 135 rabbidv ⊢ ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } = { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) } )
137 136 eleq2d ⊢ ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) → ( 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↔ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) } ) )
138 134 137 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) → 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) )
139 138 con3dimp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ ¬ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ¬ 𝑘 = ( 𝑋 ∘f + 𝑌 ) )
140 139 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ ¬ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) = 0 )
141 104 125 140 3eqtr4a ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ ¬ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑅 Σg ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) ) = if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
142 103 141 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) ) = if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
143 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ Ring )
144 143 ringcmnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ CMnd )
145 12 psrbaglefi ⊢ ( 𝑘 ∈ 𝐷 → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∈ Fin )
146 145 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∈ Fin )
147 ssdif ⊢ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ⊆ 𝐷 → ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) ⊆ ( 𝐷 ∖ { 𝑋 } ) )
148 32 147 ax-mp ⊢ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) ⊆ ( 𝐷 ∖ { 𝑋 } )
149 148 sseli ⊢ ( 𝑗 ∈ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) → 𝑗 ∈ ( 𝐷 ∖ { 𝑋 } ) )
150 107 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
151 eldifsni ⊢ ( 𝑦 ∈ ( 𝐷 ∖ { 𝑋 } ) → 𝑦 ≠ 𝑋 )
152 151 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐷 ∖ { 𝑋 } ) ) → 𝑦 ≠ 𝑋 )
153 152 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐷 ∖ { 𝑋 } ) ) → ¬ 𝑦 = 𝑋 )
154 153 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐷 ∖ { 𝑋 } ) ) → if ( 𝑦 = 𝑋 , 1 , 0 ) = 0 )
155 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
156 5 155 rabex2 ⊢ 𝐷 ∈ V
157 156 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝐷 ∈ V )
158 154 157 suppss2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) supp 0 ) ⊆ { 𝑋 } )
159 40 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 0 ∈ V )
160 150 158 157 159 suppssr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ ( 𝐷 ∖ { 𝑋 } ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) = 0 )
161 149 160 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) = 0 )
162 161 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) = ( 0 ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) )
163 eldifi ⊢ ( 𝑗 ∈ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) → 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
164 45 11 3 106 117 ringlzd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 0 ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) = 0 )
165 163 164 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) ) → ( 0 ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) = 0 )
166 162 165 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) = 0 )
167 156 rabex ⊢ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∈ V
168 167 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∈ V )
169 166 168 suppss2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) supp 0 ) ⊆ { 𝑋 } )
170 156 mptrabex ⊢ ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∈ V
171 funmpt ⊢ Fun ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) )
172 170 171 40 3pm3.2i ⊢ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∈ V ∧ Fun ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∧ 0 ∈ V )
173 172 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∈ V ∧ Fun ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∧ 0 ∈ V ) )
174 snfi ⊢ { 𝑋 } ∈ Fin
175 174 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → { 𝑋 } ∈ Fin )
176 suppssfifsupp ⊢ ( ( ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∈ V ∧ Fun ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∧ 0 ∈ V ) ∧ ( { 𝑋 } ∈ Fin ∧ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) supp 0 ) ⊆ { 𝑋 } ) ) → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) finSupp 0 )
177 173 175 169 176 syl12anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) finSupp 0 )
178 45 3 144 146 119 169 177 gsumres ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) )
179 142 178 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) )
180 179 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) )
181 18 180 eqtrid ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) )
182 15 181 eqtr4d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) )