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 |
|
subrgascl.c |
|- C = ( algSc ` U ) |
8 |
|
eqid |
|- ( Scalar ` U ) = ( Scalar ` U ) |
9 |
|
eqid |
|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) ) |
10 |
7 8 9
|
asclfn |
|- C Fn ( Base ` ( Scalar ` U ) ) |
11 |
3
|
subrgbas |
|- ( T e. ( SubRing ` R ) -> T = ( Base ` H ) ) |
12 |
6 11
|
syl |
|- ( ph -> T = ( Base ` H ) ) |
13 |
3
|
ovexi |
|- H e. _V |
14 |
13
|
a1i |
|- ( ph -> H e. _V ) |
15 |
4 5 14
|
mplsca |
|- ( ph -> H = ( Scalar ` U ) ) |
16 |
15
|
fveq2d |
|- ( ph -> ( Base ` H ) = ( Base ` ( Scalar ` U ) ) ) |
17 |
12 16
|
eqtrd |
|- ( ph -> T = ( Base ` ( Scalar ` U ) ) ) |
18 |
17
|
fneq2d |
|- ( ph -> ( C Fn T <-> C Fn ( Base ` ( Scalar ` U ) ) ) ) |
19 |
10 18
|
mpbiri |
|- ( ph -> C Fn T ) |
20 |
|
eqid |
|- ( Scalar ` P ) = ( Scalar ` P ) |
21 |
|
eqid |
|- ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) ) |
22 |
2 20 21
|
asclfn |
|- A Fn ( Base ` ( Scalar ` P ) ) |
23 |
|
subrgrcl |
|- ( T e. ( SubRing ` R ) -> R e. Ring ) |
24 |
6 23
|
syl |
|- ( ph -> R e. Ring ) |
25 |
1 5 24
|
mplsca |
|- ( ph -> R = ( Scalar ` P ) ) |
26 |
25
|
fveq2d |
|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) ) |
27 |
26
|
fneq2d |
|- ( ph -> ( A Fn ( Base ` R ) <-> A Fn ( Base ` ( Scalar ` P ) ) ) ) |
28 |
22 27
|
mpbiri |
|- ( ph -> A Fn ( Base ` R ) ) |
29 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
30 |
29
|
subrgss |
|- ( T e. ( SubRing ` R ) -> T C_ ( Base ` R ) ) |
31 |
6 30
|
syl |
|- ( ph -> T C_ ( Base ` R ) ) |
32 |
|
fnssres |
|- ( ( A Fn ( Base ` R ) /\ T C_ ( Base ` R ) ) -> ( A |` T ) Fn T ) |
33 |
28 31 32
|
syl2anc |
|- ( ph -> ( A |` T ) Fn T ) |
34 |
|
fvres |
|- ( x e. T -> ( ( A |` T ) ` x ) = ( A ` x ) ) |
35 |
34
|
adantl |
|- ( ( ph /\ x e. T ) -> ( ( A |` T ) ` x ) = ( A ` x ) ) |
36 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
37 |
3 36
|
subrg0 |
|- ( T e. ( SubRing ` R ) -> ( 0g ` R ) = ( 0g ` H ) ) |
38 |
6 37
|
syl |
|- ( ph -> ( 0g ` R ) = ( 0g ` H ) ) |
39 |
38
|
ifeq2d |
|- ( ph -> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) = if ( y = ( I X. { 0 } ) , x , ( 0g ` H ) ) ) |
40 |
39
|
adantr |
|- ( ( ph /\ x e. T ) -> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) = if ( y = ( I X. { 0 } ) , x , ( 0g ` H ) ) ) |
41 |
40
|
mpteq2dv |
|- ( ( ph /\ x e. T ) -> ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) ) = ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` H ) ) ) ) |
42 |
|
eqid |
|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
43 |
5
|
adantr |
|- ( ( ph /\ x e. T ) -> I e. W ) |
44 |
24
|
adantr |
|- ( ( ph /\ x e. T ) -> R e. Ring ) |
45 |
31
|
sselda |
|- ( ( ph /\ x e. T ) -> x e. ( Base ` R ) ) |
46 |
1 42 36 29 2 43 44 45
|
mplascl |
|- ( ( ph /\ x e. T ) -> ( A ` x ) = ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) ) ) |
47 |
|
eqid |
|- ( 0g ` H ) = ( 0g ` H ) |
48 |
|
eqid |
|- ( Base ` H ) = ( Base ` H ) |
49 |
3
|
subrgring |
|- ( T e. ( SubRing ` R ) -> H e. Ring ) |
50 |
6 49
|
syl |
|- ( ph -> H e. Ring ) |
51 |
50
|
adantr |
|- ( ( ph /\ x e. T ) -> H e. Ring ) |
52 |
12
|
eleq2d |
|- ( ph -> ( x e. T <-> x e. ( Base ` H ) ) ) |
53 |
52
|
biimpa |
|- ( ( ph /\ x e. T ) -> x e. ( Base ` H ) ) |
54 |
4 42 47 48 7 43 51 53
|
mplascl |
|- ( ( ph /\ x e. T ) -> ( C ` x ) = ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` H ) ) ) ) |
55 |
41 46 54
|
3eqtr4d |
|- ( ( ph /\ x e. T ) -> ( A ` x ) = ( C ` x ) ) |
56 |
35 55
|
eqtr2d |
|- ( ( ph /\ x e. T ) -> ( C ` x ) = ( ( A |` T ) ` x ) ) |
57 |
19 33 56
|
eqfnfvd |
|- ( ph -> C = ( A |` T ) ) |