ressply1mon1p

Description: The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025)

	Ref	Expression
Hypotheses	ressply.1	⊢ 𝑆 = ( Poly₁ ‘ 𝑅 )
	ressply.2	⊢ 𝐻 = ( 𝑅 ↾_s 𝑇 )
	ressply.3	⊢ 𝑈 = ( Poly₁ ‘ 𝐻 )
	ressply.4	⊢ 𝐵 = ( Base ‘ 𝑈 )
	ressply.5	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	ressply1mon1p.m	⊢ 𝑀 = ( Monic_1p ‘ 𝑅 )
	ressply1mon1p.n	⊢ 𝑁 = ( Monic_1p ‘ 𝐻 )
Assertion	ressply1mon1p	⊢ ( 𝜑 → 𝑁 = ( 𝐵 ∩ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		ressply.1	⊢ 𝑆 = ( Poly₁ ‘ 𝑅 )
2		ressply.2	⊢ 𝐻 = ( 𝑅 ↾_s 𝑇 )
3		ressply.3	⊢ 𝑈 = ( Poly₁ ‘ 𝐻 )
4		ressply.4	⊢ 𝐵 = ( Base ‘ 𝑈 )
5		ressply.5	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
6		ressply1mon1p.m	⊢ 𝑀 = ( Monic_1p ‘ 𝑅 )
7		ressply1mon1p.n	⊢ 𝑁 = ( Monic_1p ‘ 𝐻 )
8		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
9		eqid	⊢ ( 0_g ‘ 𝑆 ) = ( 0_g ‘ 𝑆 )
10		eqid	⊢ ( deg₁ ‘ 𝑅 ) = ( deg₁ ‘ 𝑅 )
11		eqid	⊢ ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝑅 )
12	1 8 9 10 6 11	ismon1p	⊢ ( 𝑝 ∈ 𝑀 ↔ ( 𝑝 ∈ ( Base ‘ 𝑆 ) ∧ 𝑝 ≠ ( 0_g ‘ 𝑆 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ) )
13	12	anbi2i	⊢ ( ( 𝑝 ∈ 𝐵 ∧ 𝑝 ∈ 𝑀 ) ↔ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ∈ ( Base ‘ 𝑆 ) ∧ 𝑝 ≠ ( 0_g ‘ 𝑆 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ) ) )
14		eqid	⊢ ( 𝑆 ↾_s 𝐵 ) = ( 𝑆 ↾_s 𝐵 )
15	1 2 3 4 5 14	ressply1bas	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑆 ↾_s 𝐵 ) ) )
16	14 8	ressbasss	⊢ ( Base ‘ ( 𝑆 ↾_s 𝐵 ) ) ⊆ ( Base ‘ 𝑆 )
17	15 16	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
18	17	sseld	⊢ ( 𝜑 → ( 𝑝 ∈ 𝐵 → 𝑝 ∈ ( Base ‘ 𝑆 ) ) )
19	18	pm4.71d	⊢ ( 𝜑 → ( 𝑝 ∈ 𝐵 ↔ ( 𝑝 ∈ 𝐵 ∧ 𝑝 ∈ ( Base ‘ 𝑆 ) ) ) )
20	19	anbi1d	⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ≠ ( 0_g ‘ 𝑆 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ) ) ↔ ( ( 𝑝 ∈ 𝐵 ∧ 𝑝 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑝 ≠ ( 0_g ‘ 𝑆 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ) ) ) )
21		13an22anass	⊢ ( ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ∈ ( Base ‘ 𝑆 ) ∧ 𝑝 ≠ ( 0_g ‘ 𝑆 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ) ) ↔ ( ( 𝑝 ∈ 𝐵 ∧ 𝑝 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑝 ≠ ( 0_g ‘ 𝑆 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ) ) )
22	20 21	bitr4di	⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ≠ ( 0_g ‘ 𝑆 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ) ) ↔ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ∈ ( Base ‘ 𝑆 ) ∧ 𝑝 ≠ ( 0_g ‘ 𝑆 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ) ) ) )
23	1 2 3 4 5 9	ressply10g	⊢ ( 𝜑 → ( 0_g ‘ 𝑆 ) = ( 0_g ‘ 𝑈 ) )
24	23	neeq2d	⊢ ( 𝜑 → ( 𝑝 ≠ ( 0_g ‘ 𝑆 ) ↔ 𝑝 ≠ ( 0_g ‘ 𝑈 ) ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 ≠ ( 0_g ‘ 𝑆 ) ↔ 𝑝 ≠ ( 0_g ‘ 𝑈 ) ) )
26		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
27	5	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
28	2 10 3 4 26 27	ressdeg1	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) = ( ( deg₁ ‘ 𝐻 ) ‘ 𝑝 ) )
29	28	fveq2d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝐻 ) ‘ 𝑝 ) ) )
30	2 11	subrg1	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝐻 ) )
31	5 30	syl	⊢ ( 𝜑 → ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝐻 ) )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝐻 ) )
33	29 32	eqeq12d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ↔ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝐻 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝐻 ) ) )
34	25 33	anbi12d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑝 ≠ ( 0_g ‘ 𝑆 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ) ↔ ( 𝑝 ≠ ( 0_g ‘ 𝑈 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝐻 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝐻 ) ) ) )
35	34	pm5.32da	⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ≠ ( 0_g ‘ 𝑆 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ) ) ↔ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ≠ ( 0_g ‘ 𝑈 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝐻 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝐻 ) ) ) ) )
36		3anass	⊢ ( ( 𝑝 ∈ 𝐵 ∧ 𝑝 ≠ ( 0_g ‘ 𝑈 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝐻 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝐻 ) ) ↔ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ≠ ( 0_g ‘ 𝑈 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝐻 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝐻 ) ) ) )
37	35 36	bitr4di	⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ≠ ( 0_g ‘ 𝑆 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ) ) ↔ ( 𝑝 ∈ 𝐵 ∧ 𝑝 ≠ ( 0_g ‘ 𝑈 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝐻 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝐻 ) ) ) )
38	22 37	bitr3d	⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ∈ ( Base ‘ 𝑆 ) ∧ 𝑝 ≠ ( 0_g ‘ 𝑆 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝑅 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝑅 ) ) ) ↔ ( 𝑝 ∈ 𝐵 ∧ 𝑝 ≠ ( 0_g ‘ 𝑈 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝐻 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝐻 ) ) ) )
39	13 38	bitr2id	⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝐵 ∧ 𝑝 ≠ ( 0_g ‘ 𝑈 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝐻 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝐻 ) ) ↔ ( 𝑝 ∈ 𝐵 ∧ 𝑝 ∈ 𝑀 ) ) )
40		eqid	⊢ ( 0_g ‘ 𝑈 ) = ( 0_g ‘ 𝑈 )
41		eqid	⊢ ( deg₁ ‘ 𝐻 ) = ( deg₁ ‘ 𝐻 )
42		eqid	⊢ ( 1_r ‘ 𝐻 ) = ( 1_r ‘ 𝐻 )
43	3 4 40 41 7 42	ismon1p	⊢ ( 𝑝 ∈ 𝑁 ↔ ( 𝑝 ∈ 𝐵 ∧ 𝑝 ≠ ( 0_g ‘ 𝑈 ) ∧ ( ( coe₁ ‘ 𝑝 ) ‘ ( ( deg₁ ‘ 𝐻 ) ‘ 𝑝 ) ) = ( 1_r ‘ 𝐻 ) ) )
44		elin	⊢ ( 𝑝 ∈ ( 𝐵 ∩ 𝑀 ) ↔ ( 𝑝 ∈ 𝐵 ∧ 𝑝 ∈ 𝑀 ) )
45	39 43 44	3bitr4g	⊢ ( 𝜑 → ( 𝑝 ∈ 𝑁 ↔ 𝑝 ∈ ( 𝐵 ∩ 𝑀 ) ) )
46	45	eqrdv	⊢ ( 𝜑 → 𝑁 = ( 𝐵 ∩ 𝑀 ) )

Metamath Proof Explorer

Theorem ressply1mon1p

Proof