Metamath Proof Explorer

Theorem mplmonmul

Description: The product of two 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 Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypotheses mplmon.s ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplmon.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
mplmon.z ⊢ 0 = ( 0g ‘ 𝑅 )
mplmon.o ⊢ 1 = ( 1r ‘ 𝑅 )
mplmon.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
mplmon.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mplmon.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mplmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
mplmonmul.t ⊢ · = ( .r ‘ 𝑃 )
mplmonmul.x ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
Assertion mplmonmul ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) )

Proof

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