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	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑇 ) → ( ( algSc ‘ 𝑈 ) ‘ 𝑋 ) ∈ 𝐵 )
58	44 57	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑇 ) → ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 )
59	39 58	impbida	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 ↔ 𝑋 ∈ 𝑇 ) )