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 |
⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 ) |
8 |
|
eqid |
⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 ) |
9 |
|
eqid |
⊢ ( .r ‘ 𝐻 ) = ( .r ‘ 𝐻 ) |
10 |
|
eqid |
⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } |
11 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝑇 ) |
12 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑇 ∈ ( SubRing ‘ 𝑅 ) ) |
13 |
2
|
subrgbas |
⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 = ( Base ‘ 𝐻 ) ) |
14 |
12 13
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑇 = ( Base ‘ 𝐻 ) ) |
15 |
11 14
|
eleqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ ( Base ‘ 𝐻 ) ) |
16 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 ) |
17 |
3 7 8 4 9 10 15 16
|
psrvsca |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑌 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝐻 ) 𝑌 ) ) |
18 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 ) |
19 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
20 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
21 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
22 |
19
|
subrgss |
⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 ⊆ ( Base ‘ 𝑅 ) ) |
23 |
12 22
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑇 ⊆ ( Base ‘ 𝑅 ) ) |
24 |
23 11
|
sseldd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ ( Base ‘ 𝑅 ) ) |
25 |
1 2 3 4 5 6
|
resspsrbas |
⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑃 ) ) |
26 |
5 20
|
ressbasss |
⊢ ( Base ‘ 𝑃 ) ⊆ ( Base ‘ 𝑆 ) |
27 |
25 26
|
eqsstrdi |
⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝑆 ) ) |
28 |
27
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) ) |
29 |
28 16
|
sseldd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ ( Base ‘ 𝑆 ) ) |
30 |
1 18 19 20 21 10 24 29
|
psrvsca |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑆 ) 𝑌 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝑌 ) ) |
31 |
2 21
|
ressmulr |
⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐻 ) ) |
32 |
|
ofeq |
⊢ ( ( .r ‘ 𝑅 ) = ( .r ‘ 𝐻 ) → ∘f ( .r ‘ 𝑅 ) = ∘f ( .r ‘ 𝐻 ) ) |
33 |
12 31 32
|
3syl |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ∘f ( .r ‘ 𝑅 ) = ∘f ( .r ‘ 𝐻 ) ) |
34 |
33
|
oveqd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝑌 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝐻 ) 𝑌 ) ) |
35 |
30 34
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑆 ) 𝑌 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑋 } ) ∘f ( .r ‘ 𝐻 ) 𝑌 ) ) |
36 |
4
|
fvexi |
⊢ 𝐵 ∈ V |
37 |
5 18
|
ressvsca |
⊢ ( 𝐵 ∈ V → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑃 ) ) |
38 |
36 37
|
mp1i |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑃 ) ) |
39 |
38
|
oveqd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑆 ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) 𝑌 ) ) |
40 |
17 35 39
|
3eqtr2d |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) 𝑌 ) ) |