Step |
Hyp |
Ref |
Expression |
1 |
|
subrgascl.p |
|- P = ( I mPoly R ) |
2 |
|
subrgascl.a |
|- A = ( algSc ` P ) |
3 |
|
subrgascl.h |
|- H = ( R |`s T ) |
4 |
|
subrgascl.u |
|- U = ( I mPoly H ) |
5 |
|
subrgascl.i |
|- ( ph -> I e. W ) |
6 |
|
subrgascl.r |
|- ( ph -> T e. ( SubRing ` R ) ) |
7 |
|
subrgasclcl.b |
|- B = ( Base ` U ) |
8 |
|
subrgasclcl.k |
|- K = ( Base ` R ) |
9 |
|
subrgasclcl.x |
|- ( ph -> X e. K ) |
10 |
|
iftrue |
|- ( x = ( I X. { 0 } ) -> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) = X ) |
11 |
10
|
eleq1d |
|- ( x = ( I X. { 0 } ) -> ( if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) e. ( Base ` H ) <-> X e. ( Base ` H ) ) ) |
12 |
|
eqid |
|- ( I mPwSer H ) = ( I mPwSer H ) |
13 |
|
eqid |
|- ( Base ` H ) = ( Base ` H ) |
14 |
|
eqid |
|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
15 |
|
eqid |
|- ( Base ` ( I mPwSer H ) ) = ( Base ` ( I mPwSer H ) ) |
16 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
17 |
|
subrgrcl |
|- ( T e. ( SubRing ` R ) -> R e. Ring ) |
18 |
6 17
|
syl |
|- ( ph -> R e. Ring ) |
19 |
1 14 16 8 2 5 18 9
|
mplascl |
|- ( ph -> ( A ` X ) = ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) ) |
20 |
19
|
adantr |
|- ( ( ph /\ ( A ` X ) e. B ) -> ( A ` X ) = ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) ) |
21 |
3
|
subrgring |
|- ( T e. ( SubRing ` R ) -> H e. Ring ) |
22 |
6 21
|
syl |
|- ( ph -> H e. Ring ) |
23 |
12 4 7 5 22
|
mplsubrg |
|- ( ph -> B e. ( SubRing ` ( I mPwSer H ) ) ) |
24 |
15
|
subrgss |
|- ( B e. ( SubRing ` ( I mPwSer H ) ) -> B C_ ( Base ` ( I mPwSer H ) ) ) |
25 |
23 24
|
syl |
|- ( ph -> B C_ ( Base ` ( I mPwSer H ) ) ) |
26 |
25
|
sselda |
|- ( ( ph /\ ( A ` X ) e. B ) -> ( A ` X ) e. ( Base ` ( I mPwSer H ) ) ) |
27 |
20 26
|
eqeltrrd |
|- ( ( ph /\ ( A ` X ) e. B ) -> ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) e. ( Base ` ( I mPwSer H ) ) ) |
28 |
12 13 14 15 27
|
psrelbas |
|- ( ( ph /\ ( A ` X ) e. B ) -> ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` H ) ) |
29 |
|
eqid |
|- ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) = ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) |
30 |
29
|
fmpt |
|- ( A. x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) e. ( Base ` H ) <-> ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` H ) ) |
31 |
28 30
|
sylibr |
|- ( ( ph /\ ( A ` X ) e. B ) -> A. x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } if ( x = ( I X. { 0 } ) , X , ( 0g ` R ) ) e. ( Base ` H ) ) |
32 |
5
|
adantr |
|- ( ( ph /\ ( A ` X ) e. B ) -> I e. W ) |
33 |
14
|
psrbag0 |
|- ( I e. W -> ( I X. { 0 } ) e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) |
34 |
32 33
|
syl |
|- ( ( ph /\ ( A ` X ) e. B ) -> ( I X. { 0 } ) e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) |
35 |
11 31 34
|
rspcdva |
|- ( ( ph /\ ( A ` X ) e. B ) -> X e. ( Base ` H ) ) |
36 |
3
|
subrgbas |
|- ( T e. ( SubRing ` R ) -> T = ( Base ` H ) ) |
37 |
6 36
|
syl |
|- ( ph -> T = ( Base ` H ) ) |
38 |
37
|
adantr |
|- ( ( ph /\ ( A ` X ) e. B ) -> T = ( Base ` H ) ) |
39 |
35 38
|
eleqtrrd |
|- ( ( ph /\ ( A ` X ) e. B ) -> X e. T ) |
40 |
|
eqid |
|- ( algSc ` U ) = ( algSc ` U ) |
41 |
1 2 3 4 5 6 40
|
subrgascl |
|- ( ph -> ( algSc ` U ) = ( A |` T ) ) |
42 |
41
|
fveq1d |
|- ( ph -> ( ( algSc ` U ) ` X ) = ( ( A |` T ) ` X ) ) |
43 |
|
fvres |
|- ( X e. T -> ( ( A |` T ) ` X ) = ( A ` X ) ) |
44 |
42 43
|
sylan9eq |
|- ( ( ph /\ X e. T ) -> ( ( algSc ` U ) ` X ) = ( A ` X ) ) |
45 |
|
eqid |
|- ( Scalar ` U ) = ( Scalar ` U ) |
46 |
4
|
mplring |
|- ( ( I e. W /\ H e. Ring ) -> U e. Ring ) |
47 |
4
|
mpllmod |
|- ( ( I e. W /\ H e. Ring ) -> U e. LMod ) |
48 |
|
eqid |
|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) ) |
49 |
40 45 46 47 48 7
|
asclf |
|- ( ( I e. W /\ H e. Ring ) -> ( algSc ` U ) : ( Base ` ( Scalar ` U ) ) --> B ) |
50 |
5 22 49
|
syl2anc |
|- ( ph -> ( algSc ` U ) : ( Base ` ( Scalar ` U ) ) --> B ) |
51 |
50
|
adantr |
|- ( ( ph /\ X e. T ) -> ( algSc ` U ) : ( Base ` ( Scalar ` U ) ) --> B ) |
52 |
4 5 22
|
mplsca |
|- ( ph -> H = ( Scalar ` U ) ) |
53 |
52
|
fveq2d |
|- ( ph -> ( Base ` H ) = ( Base ` ( Scalar ` U ) ) ) |
54 |
37 53
|
eqtrd |
|- ( ph -> T = ( Base ` ( Scalar ` U ) ) ) |
55 |
54
|
eleq2d |
|- ( ph -> ( X e. T <-> X e. ( Base ` ( Scalar ` U ) ) ) ) |
56 |
55
|
biimpa |
|- ( ( ph /\ X e. T ) -> X e. ( Base ` ( Scalar ` U ) ) ) |
57 |
51 56
|
ffvelrnd |
|- ( ( ph /\ X e. T ) -> ( ( algSc ` U ) ` X ) e. B ) |
58 |
44 57
|
eqeltrrd |
|- ( ( ph /\ X e. T ) -> ( A ` X ) e. B ) |
59 |
39 58
|
impbida |
|- ( ph -> ( ( A ` X ) e. B <-> X e. T ) ) |