Step |
Hyp |
Ref |
Expression |
1 |
|
psrcnrg.s |
⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) |
2 |
|
psrcnrg.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
3 |
|
psrcnrg.r |
⊢ ( 𝜑 → 𝑅 ∈ CRing ) |
4 |
|
eqidd |
⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) ) |
5 |
1 2 3
|
psrsca |
⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑆 ) ) |
6 |
|
eqidd |
⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) ) |
7 |
|
eqidd |
⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 ) ) |
8 |
|
eqidd |
⊢ ( 𝜑 → ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 ) ) |
9 |
|
crngring |
⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring ) |
10 |
3 9
|
syl |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
11 |
1 2 10
|
psrlmod |
⊢ ( 𝜑 → 𝑆 ∈ LMod ) |
12 |
1 2 10
|
psrring |
⊢ ( 𝜑 → 𝑆 ∈ Ring ) |
13 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝐼 ∈ 𝑉 ) |
14 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑅 ∈ Ring ) |
15 |
|
eqid |
⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } |
16 |
|
eqid |
⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 ) |
17 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
18 |
|
simpr2 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) ) |
19 |
|
simpr3 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑆 ) ) |
20 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑅 ∈ CRing ) |
21 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
22 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 ) |
23 |
|
simpr1 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) ) |
24 |
1 13 14 15 16 17 18 19 20 21 22 23
|
psrass23 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ( .r ‘ 𝑆 ) 𝑧 ) = ( 𝑥 ( ·𝑠 ‘ 𝑆 ) ( 𝑦 ( .r ‘ 𝑆 ) 𝑧 ) ) ∧ ( 𝑦 ( .r ‘ 𝑆 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑆 ) ( 𝑦 ( .r ‘ 𝑆 ) 𝑧 ) ) ) ) |
25 |
24
|
simpld |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ( .r ‘ 𝑆 ) 𝑧 ) = ( 𝑥 ( ·𝑠 ‘ 𝑆 ) ( 𝑦 ( .r ‘ 𝑆 ) 𝑧 ) ) ) |
26 |
24
|
simprd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑦 ( .r ‘ 𝑆 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑆 ) ( 𝑦 ( .r ‘ 𝑆 ) 𝑧 ) ) ) |
27 |
4 5 6 7 8 11 12 3 25 26
|
isassad |
⊢ ( 𝜑 → 𝑆 ∈ AssAlg ) |