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

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 ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 ) → ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) )
28 12 13 14 15 27 psrelbas ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 ) → ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
29 eqid ⊢ ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) = ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) )
30 29 fmpt ⊢ ( ∀ 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐻 ) ↔ ( 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝐻 ) )
31 28 30 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 ) → ∀ 𝑥 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } if ( 𝑥 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐻 ) )
32 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 ) → 𝐼 ∈ 𝑊 )
33 14 psrbag0 ⊢ ( 𝐼 ∈ 𝑊 → ( 𝐼 × { 0 } ) ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
34 32 33 syl ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 ) → ( 𝐼 × { 0 } ) ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑇 ) → ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ∈ 𝐵 )
58 44 57 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑇 ) → ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 )
59 39 58 impbida ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 ↔ 𝑋 ∈ 𝑇 ) )