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