Metamath Proof Explorer


Theorem subrgascl

Description: The scalar injection function in a subring algebra is the same up to a restriction to the subring. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses subrgascl.p
|- P = ( I mPoly R )
subrgascl.a
|- A = ( algSc ` P )
subrgascl.h
|- H = ( R |`s T )
subrgascl.u
|- U = ( I mPoly H )
subrgascl.i
|- ( ph -> I e. W )
subrgascl.r
|- ( ph -> T e. ( SubRing ` R ) )
subrgascl.c
|- C = ( algSc ` U )
Assertion subrgascl
|- ( ph -> C = ( A |` T ) )

Proof

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 ) )