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	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	subrgascl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	subrgascl.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
	subrgascl.u	⊢ 𝑈 = ( 𝐼 mPoly 𝐻 )
	subrgascl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	subrgascl.r	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	subrgascl.c	⊢ 𝐶 = ( algSc ‘ 𝑈 )
Assertion	subrgascl	⊢ ( 𝜑 → 𝐶 = ( 𝐴 ↾ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		subrgascl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		subrgascl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
3		subrgascl.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
4		subrgascl.u	⊢ 𝑈 = ( 𝐼 mPoly 𝐻 )
5		subrgascl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6		subrgascl.r	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
7		subrgascl.c	⊢ 𝐶 = ( algSc ‘ 𝑈 )
8		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
9		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
10	7 8 9	asclfn	⊢ 𝐶 Fn ( Base ‘ ( Scalar ‘ 𝑈 ) )
11	3	subrgbas	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 = ( Base ‘ 𝐻 ) )
12	6 11	syl	⊢ ( 𝜑 → 𝑇 = ( Base ‘ 𝐻 ) )
13	3	ovexi	⊢ 𝐻 ∈ V
14	13	a1i	⊢ ( 𝜑 → 𝐻 ∈ V )
15	4 5 14	mplsca	⊢ ( 𝜑 → 𝐻 = ( Scalar ‘ 𝑈 ) )
16	15	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐻 ) = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
17	12 16	eqtrd	⊢ ( 𝜑 → 𝑇 = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
18	17	fneq2d	⊢ ( 𝜑 → ( 𝐶 Fn 𝑇 ↔ 𝐶 Fn ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) )
19	10 18	mpbiri	⊢ ( 𝜑 → 𝐶 Fn 𝑇 )
20		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
21		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
22	2 20 21	asclfn	⊢ 𝐴 Fn ( Base ‘ ( Scalar ‘ 𝑃 ) )
23		subrgrcl	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
24	6 23	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
25	1 5 24	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
26	25	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
27	26	fneq2d	⊢ ( 𝜑 → ( 𝐴 Fn ( Base ‘ 𝑅 ) ↔ 𝐴 Fn ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) )
28	22 27	mpbiri	⊢ ( 𝜑 → 𝐴 Fn ( Base ‘ 𝑅 ) )
29		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
30	29	subrgss	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 ⊆ ( Base ‘ 𝑅 ) )
31	6 30	syl	⊢ ( 𝜑 → 𝑇 ⊆ ( Base ‘ 𝑅 ) )
32		fnssres	⊢ ( ( 𝐴 Fn ( Base ‘ 𝑅 ) ∧ 𝑇 ⊆ ( Base ‘ 𝑅 ) ) → ( 𝐴 ↾ 𝑇 ) Fn 𝑇 )
33	28 31 32	syl2anc	⊢ ( 𝜑 → ( 𝐴 ↾ 𝑇 ) Fn 𝑇 )
34		fvres	⊢ ( 𝑥 ∈ 𝑇 → ( ( 𝐴 ↾ 𝑇 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
35	34	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ( 𝐴 ↾ 𝑇 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
36		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
37	3 36	subrg0	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝐻 ) )
38	6 37	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝐻 ) )
39	38	ifeq2d	⊢ ( 𝜑 → if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑥 , ( 0g ‘ 𝑅 ) ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑥 , ( 0g ‘ 𝐻 ) ) )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑥 , ( 0g ‘ 𝑅 ) ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑥 , ( 0g ‘ 𝐻 ) ) )
41	40	mpteq2dv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑥 , ( 0g ‘ 𝑅 ) ) ) = ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑥 , ( 0g ‘ 𝐻 ) ) ) )
42		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
43	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → 𝐼 ∈ 𝑊 )
44	24	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → 𝑅 ∈ Ring )
45	31	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
46	1 42 36 29 2 43 44 45	mplascl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐴 ‘ 𝑥 ) = ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑥 , ( 0g ‘ 𝑅 ) ) ) )
47		eqid	⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
48		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
49	3	subrgring	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐻 ∈ Ring )
50	6 49	syl	⊢ ( 𝜑 → 𝐻 ∈ Ring )
51	50	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → 𝐻 ∈ Ring )
52	12	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 ↔ 𝑥 ∈ ( Base ‘ 𝐻 ) ) )
53	52	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( Base ‘ 𝐻 ) )
54	4 42 47 48 7 43 51 53	mplascl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐶 ‘ 𝑥 ) = ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑥 , ( 0g ‘ 𝐻 ) ) ) )
55	41 46 54	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐴 ‘ 𝑥 ) = ( 𝐶 ‘ 𝑥 ) )
56	35 55	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐶 ‘ 𝑥 ) = ( ( 𝐴 ↾ 𝑇 ) ‘ 𝑥 ) )
57	19 33 56	eqfnfvd	⊢ ( 𝜑 → 𝐶 = ( 𝐴 ↾ 𝑇 ) )