This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rhmpsrlem2

Description: Lemma for rhmpsr et al. (Contributed by SN, 8-Feb-2025)

Ref Expression
Hypotheses rhmpsrlem1.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
rhmpsrlem1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
rhmpsrlem1.x ⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
rhmpsrlem1.y ⊢ ( 𝜑 → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
Assertion rhmpsrlem2 ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 rhmpsrlem1.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 rhmpsrlem1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
3 rhmpsrlem1.x ⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
4 rhmpsrlem1.y ⊢ ( 𝜑 → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7 2 ringcmnd ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ CMnd )
9 1 psrbaglefi ⊢ ( 𝑘 ∈ 𝐷 → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
11 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
12 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring )
13 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
14 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∘r ≤ 𝑘 ↔ 𝑥 ∘r ≤ 𝑘 ) )
15 14 elrab ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∘r ≤ 𝑘 ) )
16 15 biimpi ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } → ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∘r ≤ 𝑘 ) )
17 16 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∘r ≤ 𝑘 ) )
18 17 simpld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∈ 𝐷 )
19 13 18 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
20 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
21 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑘 ∈ 𝐷 )
22 1 psrbagf ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 : 𝐼 ⟶ ℕ0 )
23 18 22 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
24 17 simprd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∘r ≤ 𝑘 )
25 1 psrbagcon ⊢ ( ( 𝑘 ∈ 𝐷 ∧ 𝑥 : 𝐼 ⟶ ℕ0 ∧ 𝑥 ∘r ≤ 𝑘 ) → ( ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 ∧ ( 𝑘 ∘f − 𝑥 ) ∘r ≤ 𝑘 ) )
26 21 23 24 25 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 ∧ ( 𝑘 ∘f − 𝑥 ) ∘r ≤ 𝑘 ) )
27 26 simpld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 )
28 20 27 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
29 5 11 12 19 28 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
30 29 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) : { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ⟶ ( Base ‘ 𝑅 ) )
31 1 2 3 4 rhmpsrlem1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) finSupp ( 0g ‘ 𝑅 ) )
32 5 6 8 10 30 31 gsumcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )