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