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 { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
8 7 psrbaglefi ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } → { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ∈ Fin )
9 8 adantl ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ∈ Fin )
10 subrgsubg ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 ∈ ( SubGrp ‘ 𝑅 ) )
11 6 10 syl ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝑅 ) )
12 subgsubm ( 𝑇 ∈ ( SubGrp ‘ 𝑅 ) → 𝑇 ∈ ( SubMnd ‘ 𝑅 ) )
13 11 12 syl ( 𝜑𝑇 ∈ ( SubMnd ‘ 𝑅 ) )
14 13 ad2antrr ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → 𝑇 ∈ ( SubMnd ‘ 𝑅 ) )
15 6 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
16 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
17 simprl ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝑋𝐵 )
18 3 16 7 4 17 psrelbas ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝑋 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
19 18 adantr ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → 𝑋 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
20 elrabi ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } → 𝑥 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
21 ffvelrn ( ( 𝑋 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) ∧ 𝑥 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑋𝑥 ) ∈ ( Base ‘ 𝐻 ) )
22 19 20 21 syl2an ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → ( 𝑋𝑥 ) ∈ ( Base ‘ 𝐻 ) )
23 2 subrgbas ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 = ( Base ‘ 𝐻 ) )
24 15 23 syl ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → 𝑇 = ( Base ‘ 𝐻 ) )
25 22 24 eleqtrrd ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → ( 𝑋𝑥 ) ∈ 𝑇 )
26 simprr ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝑌𝐵 )
27 3 16 7 4 26 psrelbas ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝑌 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
28 27 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → 𝑌 : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
29 ssrab2 { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ⊆ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
30 simplr ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
31 simpr ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } )
32 eqid { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } = { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 }
33 7 32 psrbagconcl ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → ( 𝑘f𝑥 ) ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } )
34 30 31 33 syl2anc ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → ( 𝑘f𝑥 ) ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } )
35 29 34 sselid ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → ( 𝑘f𝑥 ) ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
36 28 35 ffvelrnd ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ∈ ( Base ‘ 𝐻 ) )
37 36 24 eleqtrrd ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ∈ 𝑇 )
38 eqid ( .r𝑅 ) = ( .r𝑅 )
39 38 subrgmcl ( ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑋𝑥 ) ∈ 𝑇 ∧ ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ∈ 𝑇 ) → ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ∈ 𝑇 )
40 15 25 37 39 syl3anc ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ∈ 𝑇 )
41 40 fmpttd ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) : { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ⟶ 𝑇 )
42 9 14 41 2 gsumsubm ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) = ( 𝐻 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) )
43 2 38 ressmulr ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( .r𝑅 ) = ( .r𝐻 ) )
44 6 43 syl ( 𝜑 → ( .r𝑅 ) = ( .r𝐻 ) )
45 44 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → ( .r𝑅 ) = ( .r𝐻 ) )
46 45 oveqd ( ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ) → ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) = ( ( 𝑋𝑥 ) ( .r𝐻 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) )
47 46 mpteq2dva ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝐻 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) )
48 47 oveq2d ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝐻 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) = ( 𝐻 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝐻 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) )
49 42 48 eqtrd ( ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) = ( 𝐻 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝐻 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) )
50 49 mpteq2dva ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
60 53 58 59 sylancr ( 𝜑 → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
61 60 adantr ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( ( Base ‘ 𝐻 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) ⊆ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) )
67 1 55 7 51 65 psrbas ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( Base ‘ 𝑆 ) = ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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𝑆 ) 𝑌 ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) )
72 eqid ( .r𝐻 ) = ( .r𝐻 )
73 eqid ( .r𝑈 ) = ( .r𝑈 )
74 3 4 72 73 7 17 26 psrmulfval ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 ( .r𝑈 ) 𝑌 ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 Σg ( 𝑥 ∈ { 𝑦 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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𝑃 ) 𝑌 ) )