Metamath Proof Explorer


Theorem subrgasclcl

Description: The scalars in a polynomial algebra are in the subring algebra iff the scalar value is in 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 ‘ 𝑅 ) )
subrgasclcl.b 𝐵 = ( Base ‘ 𝑈 )
subrgasclcl.k 𝐾 = ( Base ‘ 𝑅 )
subrgasclcl.x ( 𝜑𝑋𝐾 )
Assertion subrgasclcl ( 𝜑 → ( ( 𝐴𝑋 ) ∈ 𝐵𝑋𝑇 ) )

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 subrgasclcl.b 𝐵 = ( Base ‘ 𝑈 )
8 subrgasclcl.k 𝐾 = ( Base ‘ 𝑅 )
9 subrgasclcl.x ( 𝜑𝑋𝐾 )
10 iftrue ( 𝑥 = ( 𝐼 × { 0 } ) → if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g𝑅 ) ) = 𝑋 )
11 10 eleq1d ( 𝑥 = ( 𝐼 × { 0 } ) → ( if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g𝑅 ) ) ∈ ( Base ‘ 𝐻 ) ↔ 𝑋 ∈ ( Base ‘ 𝐻 ) ) )
12 eqid ( 𝐼 mPwSer 𝐻 ) = ( 𝐼 mPwSer 𝐻 )
13 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
14 eqid { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
15 eqid ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝐻 ) )
16 eqid ( 0g𝑅 ) = ( 0g𝑅 )
17 subrgrcl ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
18 6 17 syl ( 𝜑𝑅 ∈ Ring )
19 1 14 16 8 2 5 18 9 mplascl ( 𝜑 → ( 𝐴𝑋 ) = ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g𝑅 ) ) ) )
20 19 adantr ( ( 𝜑 ∧ ( 𝐴𝑋 ) ∈ 𝐵 ) → ( 𝐴𝑋 ) = ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g𝑅 ) ) ) )
21 3 subrgring ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐻 ∈ Ring )
22 6 21 syl ( 𝜑𝐻 ∈ Ring )
23 12 4 7 5 22 mplsubrg ( 𝜑𝐵 ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝐻 ) ) )
24 15 subrgss ( 𝐵 ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝐻 ) ) → 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) )
25 23 24 syl ( 𝜑𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) )
26 25 sselda ( ( 𝜑 ∧ ( 𝐴𝑋 ) ∈ 𝐵 ) → ( 𝐴𝑋 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) )
27 20 26 eqeltrrd ( ( 𝜑 ∧ ( 𝐴𝑋 ) ∈ 𝐵 ) → ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g𝑅 ) ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) )
28 12 13 14 15 27 psrelbas ( ( 𝜑 ∧ ( 𝐴𝑋 ) ∈ 𝐵 ) → ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g𝑅 ) ) ) : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
29 eqid ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g𝑅 ) ) ) = ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g𝑅 ) ) )
30 29 fmpt ( ∀ 𝑥 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g𝑅 ) ) ∈ ( Base ‘ 𝐻 ) ↔ ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g𝑅 ) ) ) : { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
31 28 30 sylibr ( ( 𝜑 ∧ ( 𝐴𝑋 ) ∈ 𝐵 ) → ∀ 𝑥 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g𝑅 ) ) ∈ ( Base ‘ 𝐻 ) )
32 5 adantr ( ( 𝜑 ∧ ( 𝐴𝑋 ) ∈ 𝐵 ) → 𝐼𝑊 )
33 14 psrbag0 ( 𝐼𝑊 → ( 𝐼 × { 0 } ) ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
34 32 33 syl ( ( 𝜑 ∧ ( 𝐴𝑋 ) ∈ 𝐵 ) → ( 𝐼 × { 0 } ) ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } )
35 11 31 34 rspcdva ( ( 𝜑 ∧ ( 𝐴𝑋 ) ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝐻 ) )
36 3 subrgbas ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 = ( Base ‘ 𝐻 ) )
37 6 36 syl ( 𝜑𝑇 = ( Base ‘ 𝐻 ) )
38 37 adantr ( ( 𝜑 ∧ ( 𝐴𝑋 ) ∈ 𝐵 ) → 𝑇 = ( Base ‘ 𝐻 ) )
39 35 38 eleqtrrd ( ( 𝜑 ∧ ( 𝐴𝑋 ) ∈ 𝐵 ) → 𝑋𝑇 )
40 eqid ( algSc ‘ 𝑈 ) = ( algSc ‘ 𝑈 )
41 1 2 3 4 5 6 40 subrgascl ( 𝜑 → ( algSc ‘ 𝑈 ) = ( 𝐴𝑇 ) )
42 41 fveq1d ( 𝜑 → ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) = ( ( 𝐴𝑇 ) ‘ 𝑋 ) )
43 fvres ( 𝑋𝑇 → ( ( 𝐴𝑇 ) ‘ 𝑋 ) = ( 𝐴𝑋 ) )
44 42 43 sylan9eq ( ( 𝜑𝑋𝑇 ) → ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) = ( 𝐴𝑋 ) )
45 eqid ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
46 4 mplring ( ( 𝐼𝑊𝐻 ∈ Ring ) → 𝑈 ∈ Ring )
47 4 mpllmod ( ( 𝐼𝑊𝐻 ∈ Ring ) → 𝑈 ∈ LMod )
48 eqid ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
49 40 45 46 47 48 7 asclf ( ( 𝐼𝑊𝐻 ∈ Ring ) → ( algSc ‘ 𝑈 ) : ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟶ 𝐵 )
50 5 22 49 syl2anc ( 𝜑 → ( algSc ‘ 𝑈 ) : ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟶ 𝐵 )
51 50 adantr ( ( 𝜑𝑋𝑇 ) → ( algSc ‘ 𝑈 ) : ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟶ 𝐵 )
52 4 5 22 mplsca ( 𝜑𝐻 = ( Scalar ‘ 𝑈 ) )
53 52 fveq2d ( 𝜑 → ( Base ‘ 𝐻 ) = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
54 37 53 eqtrd ( 𝜑𝑇 = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
55 54 eleq2d ( 𝜑 → ( 𝑋𝑇𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) )
56 55 biimpa ( ( 𝜑𝑋𝑇 ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
57 51 56 ffvelrnd ( ( 𝜑𝑋𝑇 ) → ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ∈ 𝐵 )
58 44 57 eqeltrrd ( ( 𝜑𝑋𝑇 ) → ( 𝐴𝑋 ) ∈ 𝐵 )
59 39 58 impbida ( 𝜑 → ( ( 𝐴𝑋 ) ∈ 𝐵𝑋𝑇 ) )