Step |
Hyp |
Ref |
Expression |
1 |
|
psrcnrg.s |
|- S = ( I mPwSer R ) |
2 |
|
psrcnrg.i |
|- ( ph -> I e. V ) |
3 |
|
psrcnrg.r |
|- ( ph -> R e. CRing ) |
4 |
|
eqidd |
|- ( ph -> ( Base ` S ) = ( Base ` S ) ) |
5 |
1 2 3
|
psrsca |
|- ( ph -> R = ( Scalar ` S ) ) |
6 |
|
eqidd |
|- ( ph -> ( Base ` R ) = ( Base ` R ) ) |
7 |
|
eqidd |
|- ( ph -> ( .s ` S ) = ( .s ` S ) ) |
8 |
|
eqidd |
|- ( ph -> ( .r ` S ) = ( .r ` S ) ) |
9 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
10 |
3 9
|
syl |
|- ( ph -> R e. Ring ) |
11 |
1 2 10
|
psrlmod |
|- ( ph -> S e. LMod ) |
12 |
1 2 10
|
psrring |
|- ( ph -> S e. Ring ) |
13 |
2
|
adantr |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> I e. V ) |
14 |
10
|
adantr |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> R e. Ring ) |
15 |
|
eqid |
|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
16 |
|
eqid |
|- ( .r ` S ) = ( .r ` S ) |
17 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
18 |
|
simpr2 |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> y e. ( Base ` S ) ) |
19 |
|
simpr3 |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> z e. ( Base ` S ) ) |
20 |
3
|
adantr |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> R e. CRing ) |
21 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
22 |
|
eqid |
|- ( .s ` S ) = ( .s ` S ) |
23 |
|
simpr1 |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> x e. ( Base ` R ) ) |
24 |
1 13 14 15 16 17 18 19 20 21 22 23
|
psrass23 |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( ( x ( .s ` S ) y ) ( .r ` S ) z ) = ( x ( .s ` S ) ( y ( .r ` S ) z ) ) /\ ( y ( .r ` S ) ( x ( .s ` S ) z ) ) = ( x ( .s ` S ) ( y ( .r ` S ) z ) ) ) ) |
25 |
24
|
simpld |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( .s ` S ) y ) ( .r ` S ) z ) = ( x ( .s ` S ) ( y ( .r ` S ) z ) ) ) |
26 |
24
|
simprd |
|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( y ( .r ` S ) ( x ( .s ` S ) z ) ) = ( x ( .s ` S ) ( y ( .r ` S ) z ) ) ) |
27 |
4 5 6 7 8 11 12 3 25 26
|
isassad |
|- ( ph -> S e. AssAlg ) |