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 ⊢ 𝑃 = ( 𝐼 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 ⊢ ( 𝜑 → 𝐶 = ( 𝐴 ↾ 𝑇 ) )