Metamath Proof Explorer

Theorem resspsrmul

Description: A restricted power series algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypotheses resspsr.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
resspsr.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
resspsr.u ⊢ 𝑈 = ( 𝐼 mPwSer 𝐻 )
resspsr.b ⊢ 𝐵 = ( Base ‘ 𝑈 )
resspsr.p ⊢ 𝑃 = ( 𝑆 ↾s 𝐵 )
resspsr.2 ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
Assertion resspsrmul ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( .r ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( .r ‘ 𝑃 ) 𝑌 ) )

Proof

Step Hyp Ref Expression
1 resspsr.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 resspsr.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
3 resspsr.u ⊢ 𝑈 = ( 𝐼 mPwSer 𝐻 )
4 resspsr.b ⊢ 𝐵 = ( Base ‘ 𝑈 )
5 resspsr.p ⊢ 𝑃 = ( 𝑆 ↾s 𝐵 )
6 resspsr.2 ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
7 eqid ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
8 7 psrbaglefi ⊢ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } → { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
9 8 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
10 subrgsubg ⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 ∈ ( SubGrp ‘ 𝑅 ) )
11 6 10 syl ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝑅 ) )
12 subgsubm ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝑅 ) → 𝑇 ∈ ( SubMnd ‘ 𝑅 ) )
13 11 12 syl ⊢ ( 𝜑 → 𝑇 ∈ ( SubMnd ‘ 𝑅 ) )
14 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑇 ∈ ( SubMnd ‘ 𝑅 ) )
15 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
16 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
18 3 16 7 4 17 psrelbas ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
19 18 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑋 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
20 elrabi ⊢ ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } → 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
21 ffvelrn ⊢ ( ( 𝑋 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) ∧ 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝐻 ) )
22 19 20 21 syl2an ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝐻 ) )
23 2 subrgbas ⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 = ( Base ‘ 𝐻 ) )
24 15 23 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑇 = ( Base ‘ 𝐻 ) )
25 22 24 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑋 ‘ 𝑥 ) ∈ 𝑇 )
26 simprr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
27 3 16 7 4 26 psrelbas ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
28 27 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑌 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
29 ssrab2 ⊢ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ⊆ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
30 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
31 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } )
32 eqid ⊢ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } = { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 }
33 7 32 psrbagconcl ⊢ ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } )
34 30 31 33 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } )
35 29 34 sseldi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
36 28 35 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝐻 ) )
37 36 24 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ 𝑇 )
38 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
39 38 subrgmcl ⊢ ( ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋 ‘ 𝑥 ) ∈ 𝑇 ∧ ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ 𝑇 ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ∈ 𝑇 )
40 15 25 37 39 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ∈ 𝑇 )
41 40 fmpttd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) : { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ⟶ 𝑇 )
42 9 14 41 2 gsumsubm ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝐻 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
43 2 38 ressmulr ⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐻 ) )
44 6 43 syl ⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐻 ) )
45 44 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐻 ) )
46 45 oveqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝐻 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
47 46 mpteq2dva ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝐻 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
48 47 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝐻 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝐻 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝐻 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
49 42 48 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝐻 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝐻 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
50 49 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝐻 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
51 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
52 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
53 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
54 6 23 syl ⊢ ( 𝜑 → 𝑇 = ( Base ‘ 𝐻 ) )
55 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
56 55 subrgss ⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 ⊆ ( Base ‘ 𝑅 ) )
57 6 56 syl ⊢ ( 𝜑 → 𝑇 ⊆ ( Base ‘ 𝑅 ) )
58 54 57 eqsstrrd ⊢ ( 𝜑 → ( Base ‘ 𝐻 ) ⊆ ( Base ‘ 𝑅 ) )
59 mapss ⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ ( Base ‘ 𝐻 ) ⊆ ( Base ‘ 𝑅 ) ) → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
60 53 58 59 sylancr ⊢ ( 𝜑 → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
61 60 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
62 reldmpsr ⊢ Rel dom mPwSer
63 62 3 4 elbasov ⊢ ( 𝑋 ∈ 𝐵 → ( 𝐼 ∈ V ∧ 𝐻 ∈ V ) )
64 63 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐼 ∈ V ∧ 𝐻 ∈ V ) )
65 64 simpld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐼 ∈ V )
66 3 16 7 4 65 psrbas ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐵 = ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
67 1 55 7 51 65 psrbas ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( Base ‘ 𝑆 ) = ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
68 61 66 67 3sstr4d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
69 68 17 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ ( Base ‘ 𝑆 ) )
70 68 26 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ ( Base ‘ 𝑆 ) )
71 1 51 38 52 7 69 70 psrmulfval ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
72 eqid ⊢ ( .r ‘ 𝐻 ) = ( .r ‘ 𝐻 )
73 eqid ⊢ ( .r ‘ 𝑈 ) = ( .r ‘ 𝑈 )
74 3 4 72 73 7 17 26 psrmulfval ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( .r ‘ 𝑈 ) 𝑌 ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝐻 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
75 50 71 74 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( .r ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) )
76 4 fvexi ⊢ 𝐵 ∈ V
77 5 52 ressmulr ⊢ ( 𝐵 ∈ V → ( .r ‘ 𝑆 ) = ( .r ‘ 𝑃 ) )
78 76 77 mp1i ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( .r ‘ 𝑆 ) = ( .r ‘ 𝑃 ) )
79 78 oveqd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) = ( 𝑋 ( .r ‘ 𝑃 ) 𝑌 ) )
80 75 79 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( .r ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( .r ‘ 𝑃 ) 𝑌 ) )