Metamath Proof Explorer

Theorem mplsubrglem

Description: Lemma for mplsubrg . (Contributed by Mario Carneiro, 9-Jan-2015) (Revised by AV, 18-Jul-2019)

Ref Expression
Hypotheses mplsubg.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
mplsubg.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplsubg.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
mplsubg.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mpllss.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mplsubrglem.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
mplsubrglem.z ⊢ 0 = ( 0g ‘ 𝑅 )
mplsubrglem.p ⊢ 𝐴 = ( ∘f + “ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) )
mplsubrglem.t ⊢ · = ( .r ‘ 𝑅 )
mplsubrglem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
mplsubrglem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
Assertion mplsubrglem ( 𝜑 → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 mplsubg.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 mplsubg.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3 mplsubg.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
4 mplsubg.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5 mpllss.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 mplsubrglem.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
7 mplsubrglem.z ⊢ 0 = ( 0g ‘ 𝑅 )
8 mplsubrglem.p ⊢ 𝐴 = ( ∘f + “ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) )
9 mplsubrglem.t ⊢ · = ( .r ‘ 𝑅 )
10 mplsubrglem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
11 mplsubrglem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
12 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
13 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
14 2 1 3 12 mplbasss ⊢ 𝑈 ⊆ ( Base ‘ 𝑆 )
15 14 10 sseldi ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑆 ) )
16 14 11 sseldi ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑆 ) )
17 1 12 13 5 15 16 psrmulcl ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
18 ovexd ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ V )
19 1 12 psrelbasfun ⊢ ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ ( Base ‘ 𝑆 ) → Fun ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) )
20 17 19 syl ⊢ ( 𝜑 → Fun ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) )
21 7 fvexi ⊢ 0 ∈ V
22 21 a1i ⊢ ( 𝜑 → 0 ∈ V )
23 df-ima ⊢ ( ∘f + “ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) = ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) )
24 8 23 eqtri ⊢ 𝐴 = ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) )
25 2 1 12 7 3 mplelbas ⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ ( Base ‘ 𝑆 ) ∧ 𝑋 finSupp 0 ) )
26 25 simprbi ⊢ ( 𝑋 ∈ 𝑈 → 𝑋 finSupp 0 )
27 10 26 syl ⊢ ( 𝜑 → 𝑋 finSupp 0 )
28 2 1 12 7 3 mplelbas ⊢ ( 𝑌 ∈ 𝑈 ↔ ( 𝑌 ∈ ( Base ‘ 𝑆 ) ∧ 𝑌 finSupp 0 ) )
29 28 simprbi ⊢ ( 𝑌 ∈ 𝑈 → 𝑌 finSupp 0 )
30 11 29 syl ⊢ ( 𝜑 → 𝑌 finSupp 0 )
31 fsuppxpfi ⊢ ( ( 𝑋 finSupp 0 ∧ 𝑌 finSupp 0 ) → ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ∈ Fin )
32 27 30 31 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ∈ Fin )
33 ofmres ⊢ ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) = ( 𝑓 ∈ ( 𝑋 supp 0 ) , 𝑔 ∈ ( 𝑌 supp 0 ) ↦ ( 𝑓 ∘f + 𝑔 ) )
34 ovex ⊢ ( 𝑓 ∘f + 𝑔 ) ∈ V
35 33 34 fnmpoi ⊢ ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) Fn ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) )
36 dffn4 ⊢ ( ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) Fn ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ↔ ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) : ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) –onto→ ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) )
37 35 36 mpbi ⊢ ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) : ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) –onto→ ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) )
38 fofi ⊢ ( ( ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ∈ Fin ∧ ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) : ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) –onto→ ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ) → ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ∈ Fin )
39 32 37 38 sylancl ⊢ ( 𝜑 → ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ∈ Fin )
40 24 39 eqeltrid ⊢ ( 𝜑 → 𝐴 ∈ Fin )
41 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
42 1 41 6 12 17 psrelbas ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
43 15 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → 𝑋 ∈ ( Base ‘ 𝑆 ) )
44 16 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → 𝑌 ∈ ( Base ‘ 𝑆 ) )
45 eldifi ⊢ ( 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) → 𝑘 ∈ 𝐷 )
46 45 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → 𝑘 ∈ 𝐷 )
47 1 12 9 13 6 43 44 46 psrmulval ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ‘ 𝑘 ) = ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
48 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring )
49 2 41 3 6 11 mplelf ⊢ ( 𝜑 → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
50 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
51 ssrab2 ⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ⊆ 𝐷
52 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝐼 ∈ 𝑊 )
53 46 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑘 ∈ 𝐷 )
54 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
55 eqid ⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 }
56 6 55 psrbagconcl ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
57 52 53 54 56 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
58 51 57 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 )
59 50 58 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
60 41 9 7 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 0 · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 )
61 48 59 60 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 0 · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 )
62 oveq1 ⊢ ( ( 𝑋 ‘ 𝑥 ) = 0 → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( 0 · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
63 62 eqeq1d ⊢ ( ( 𝑋 ‘ 𝑥 ) = 0 → ( ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 ↔ ( 0 · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 ) )
64 61 63 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) = 0 → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 ) )
65 2 41 3 6 10 mplelf ⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
66 65 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
67 51 54 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∈ 𝐷 )
68 66 67 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
69 41 9 7 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑥 ) · 0 ) = 0 )
70 48 68 69 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) · 0 ) = 0 )
71 oveq2 ⊢ ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( ( 𝑋 ‘ 𝑥 ) · 0 ) )
72 71 eqeq1d ⊢ ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 → ( ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 ↔ ( ( 𝑋 ‘ 𝑥 ) · 0 ) = 0 ) )
73 70 72 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 ) )
74 6 psrbagf ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 : 𝐼 ⟶ ℕ0 )
75 52 67 74 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
76 75 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑛 ) ∈ ℕ0 )
77 6 psrbagf ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷 ) → 𝑘 : 𝐼 ⟶ ℕ0 )
78 52 53 77 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑘 : 𝐼 ⟶ ℕ0 )
79 78 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝑘 ‘ 𝑛 ) ∈ ℕ0 )
80 nn0cn ⊢ ( ( 𝑥 ‘ 𝑛 ) ∈ ℕ0 → ( 𝑥 ‘ 𝑛 ) ∈ ℂ )
81 nn0cn ⊢ ( ( 𝑘 ‘ 𝑛 ) ∈ ℕ0 → ( 𝑘 ‘ 𝑛 ) ∈ ℂ )
82 pncan3 ⊢ ( ( ( 𝑥 ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑘 ‘ 𝑛 ) ∈ ℂ ) → ( ( 𝑥 ‘ 𝑛 ) + ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ) = ( 𝑘 ‘ 𝑛 ) )
83 80 81 82 syl2an ⊢ ( ( ( 𝑥 ‘ 𝑛 ) ∈ ℕ0 ∧ ( 𝑘 ‘ 𝑛 ) ∈ ℕ0 ) → ( ( 𝑥 ‘ 𝑛 ) + ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ) = ( 𝑘 ‘ 𝑛 ) )
84 76 79 83 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑛 ) + ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ) = ( 𝑘 ‘ 𝑛 ) )
85 84 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑛 ) + ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑛 ) ) )
86 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ∈ V )
87 75 feqmptd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 = ( 𝑛 ∈ 𝐼 ↦ ( 𝑥 ‘ 𝑛 ) ) )
88 78 feqmptd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑘 = ( 𝑛 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑛 ) ) )
89 52 79 76 88 87 offval2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ) )
90 52 76 86 87 89 offval2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑥 ∘f + ( 𝑘 ∘f − 𝑥 ) ) = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑛 ) + ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ) ) )
91 85 90 88 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑥 ∘f + ( 𝑘 ∘f − 𝑥 ) ) = 𝑘 )
92 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) )
93 91 92 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑥 ∘f + ( 𝑘 ∘f − 𝑥 ) ) ∈ ( 𝐷 ∖ 𝐴 ) )
94 93 eldifbd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ¬ ( 𝑥 ∘f + ( 𝑘 ∘f − 𝑥 ) ) ∈ 𝐴 )
95 ovres ⊢ ( ( 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) → ( 𝑥 ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ( 𝑘 ∘f − 𝑥 ) ) = ( 𝑥 ∘f + ( 𝑘 ∘f − 𝑥 ) ) )
96 fnovrn ⊢ ( ( ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) Fn ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ∧ 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) → ( 𝑥 ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ( 𝑘 ∘f − 𝑥 ) ) ∈ ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) )
97 96 24 eleqtrrdi ⊢ ( ( ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) Fn ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ∧ 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) → ( 𝑥 ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ( 𝑘 ∘f − 𝑥 ) ) ∈ 𝐴 )
98 35 97 mp3an1 ⊢ ( ( 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) → ( 𝑥 ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ( 𝑘 ∘f − 𝑥 ) ) ∈ 𝐴 )
99 95 98 eqeltrrd ⊢ ( ( 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) → ( 𝑥 ∘f + ( 𝑘 ∘f − 𝑥 ) ) ∈ 𝐴 )
100 94 99 nsyl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ¬ ( 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) )
101 ianor ⊢ ( ¬ ( 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) ↔ ( ¬ 𝑥 ∈ ( 𝑋 supp 0 ) ∨ ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) )
102 100 101 sylib ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ¬ 𝑥 ∈ ( 𝑋 supp 0 ) ∨ ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) )
103 eldif ⊢ ( 𝑥 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ ( 𝑋 supp 0 ) ) )
104 103 baib ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ↔ ¬ 𝑥 ∈ ( 𝑋 supp 0 ) ) )
105 67 104 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑥 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ↔ ¬ 𝑥 ∈ ( 𝑋 supp 0 ) ) )
106 ssidd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑋 supp 0 ) ⊆ ( 𝑋 supp 0 ) )
107 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
108 6 107 rabex2 ⊢ 𝐷 ∈ V
109 108 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝐷 ∈ V )
110 21 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 0 ∈ V )
111 66 106 109 110 suppssr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑥 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( 𝑋 ‘ 𝑥 ) = 0 )
112 111 ex ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑥 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) → ( 𝑋 ‘ 𝑥 ) = 0 ) )
113 105 112 sylbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ¬ 𝑥 ∈ ( 𝑋 supp 0 ) → ( 𝑋 ‘ 𝑥 ) = 0 ) )
114 eldif ⊢ ( ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝐷 ∖ ( 𝑌 supp 0 ) ) ↔ ( ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 ∧ ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) )
115 114 baib ⊢ ( ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 → ( ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝐷 ∖ ( 𝑌 supp 0 ) ) ↔ ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) )
116 58 115 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝐷 ∖ ( 𝑌 supp 0 ) ) ↔ ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) )
117 ssidd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑌 supp 0 ) ⊆ ( 𝑌 supp 0 ) )
118 50 117 109 110 suppssr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝐷 ∖ ( 𝑌 supp 0 ) ) ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 )
119 118 ex ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝐷 ∖ ( 𝑌 supp 0 ) ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 ) )
120 116 119 sylbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 ) )
121 113 120 orim12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( ¬ 𝑥 ∈ ( 𝑋 supp 0 ) ∨ ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) → ( ( 𝑋 ‘ 𝑥 ) = 0 ∨ ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 ) ) )
122 102 121 mpd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) = 0 ∨ ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 ) )
123 64 73 122 mpjaod ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 )
124 123 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ 0 ) )
125 124 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ 0 ) ) )
126 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → 𝑅 ∈ Ring )
127 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
128 126 127 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → 𝑅 ∈ Mnd )
129 6 psrbaglefi ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
130 4 45 129 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
131 7 gsumz ⊢ ( ( 𝑅 ∈ Mnd ∧ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ 0 ) ) = 0 )
132 128 130 131 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ 0 ) ) = 0 )
133 47 125 132 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ‘ 𝑘 ) = 0 )
134 42 133 suppss ⊢ ( 𝜑 → ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) supp 0 ) ⊆ 𝐴 )
135 suppssfifsupp ⊢ ( ( ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ V ∧ Fun ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∧ 0 ∈ V ) ∧ ( 𝐴 ∈ Fin ∧ ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) supp 0 ) ⊆ 𝐴 ) ) → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) finSupp 0 )
136 18 20 22 40 134 135 syl32anc ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) finSupp 0 )
137 2 1 12 7 3 mplelbas ⊢ ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ 𝑈 ↔ ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) finSupp 0 ) )
138 17 136 137 sylanbrc ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ 𝑈 )