This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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