ressply1mon1p

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

	Ref	Expression
Hypotheses	ressply.1	$⊢ S = {Poly}_{1} (R)$
	ressply.2	$⊢ H = R ↾_{𝑠} T$
	ressply.3	$⊢ U = {Poly}_{1} (H)$
	ressply.4	$⊢ B = {Base}_{U}$
	ressply.5	$⊢ φ \to T \in SubRing (R)$
	ressply1mon1p.m	$⊢ M = {Monic}_{1p} (R)$
	ressply1mon1p.n	$⊢ N = {Monic}_{1p} (H)$
Assertion	ressply1mon1p	$⊢ φ \to N = B \cap M$

Proof

Step	Hyp	Ref	Expression
1		ressply.1	$⊢ S = {Poly}_{1} (R)$
2		ressply.2	$⊢ H = R ↾_{𝑠} T$
3		ressply.3	$⊢ U = {Poly}_{1} (H)$
4		ressply.4	$⊢ B = {Base}_{U}$
5		ressply.5	$⊢ φ \to T \in SubRing (R)$
6		ressply1mon1p.m	$⊢ M = {Monic}_{1p} (R)$
7		ressply1mon1p.n	$⊢ N = {Monic}_{1p} (H)$
8		eqid	$⊢ {Base}_{S} = {Base}_{S}$
9		eqid	$⊢ 0_{S} = 0_{S}$
10		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
11		eqid	$⊢ 1_{R} = 1_{R}$
12	1 8 9 10 6 11	ismon1p	$⊢ p \in M \leftrightarrow (p \in {Base}_{S} \land p \neq 0_{S} \land {coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R})$
13	12	anbi2i	$⊢ (p \in B \land p \in M) \leftrightarrow (p \in B \land (p \in {Base}_{S} \land p \neq 0_{S} \land {coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R}))$
14		eqid	$⊢ S ↾_{𝑠} B = S ↾_{𝑠} B$
15	1 2 3 4 5 14	ressply1bas	$⊢ φ \to B = {Base}_{(S ↾_{𝑠} B)}$
16	14 8	ressbasss	$⊢ {Base}_{(S ↾_{𝑠} B)} \subseteq {Base}_{S}$
17	15 16	eqsstrdi	$⊢ φ \to B \subseteq {Base}_{S}$
18	17	sseld	$⊢ φ \to (p \in B \to p \in {Base}_{S})$
19	18	pm4.71d	$⊢ φ \to (p \in B \leftrightarrow (p \in B \land p \in {Base}_{S}))$
20	19	anbi1d	$⊢ φ \to ((p \in B \land (p \neq 0_{S} \land {coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R})) \leftrightarrow ((p \in B \land p \in {Base}_{S}) \land (p \neq 0_{S} \land {coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R})))$
21		13an22anass	$⊢ (p \in B \land (p \in {Base}_{S} \land p \neq 0_{S} \land {coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R})) \leftrightarrow ((p \in B \land p \in {Base}_{S}) \land (p \neq 0_{S} \land {coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R}))$
22	20 21	bitr4di	$⊢ φ \to ((p \in B \land (p \neq 0_{S} \land {coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R})) \leftrightarrow (p \in B \land (p \in {Base}_{S} \land p \neq 0_{S} \land {coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R})))$
23	1 2 3 4 5 9	ressply10g	$⊢ φ \to 0_{S} = 0_{U}$
24	23	neeq2d	$⊢ φ \to (p \neq 0_{S} \leftrightarrow p \neq 0_{U})$
25	24	adantr	$⊢ (φ \land p \in B) \to (p \neq 0_{S} \leftrightarrow p \neq 0_{U})$
26		simpr	$⊢ (φ \land p \in B) \to p \in B$
27	5	adantr	$⊢ (φ \land p \in B) \to T \in SubRing (R)$
28	2 10 3 4 26 27	ressdeg1	$⊢ (φ \land p \in B) \to \deg_{1} (R) (p) = \deg_{1} (H) (p)$
29	28	fveq2d	$⊢ (φ \land p \in B) \to {coe}_{1} (p) (\deg_{1} (R) (p)) = {coe}_{1} (p) (\deg_{1} (H) (p))$
30	2 11	subrg1	$⊢ T \in SubRing (R) \to 1_{R} = 1_{H}$
31	5 30	syl	$⊢ φ \to 1_{R} = 1_{H}$
32	31	adantr	$⊢ (φ \land p \in B) \to 1_{R} = 1_{H}$
33	29 32	eqeq12d	$⊢ (φ \land p \in B) \to ({coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R} \leftrightarrow {coe}_{1} (p) (\deg_{1} (H) (p)) = 1_{H})$
34	25 33	anbi12d	$⊢ (φ \land p \in B) \to ((p \neq 0_{S} \land {coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R}) \leftrightarrow (p \neq 0_{U} \land {coe}_{1} (p) (\deg_{1} (H) (p)) = 1_{H}))$
35	34	pm5.32da	$⊢ φ \to ((p \in B \land (p \neq 0_{S} \land {coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R})) \leftrightarrow (p \in B \land (p \neq 0_{U} \land {coe}_{1} (p) (\deg_{1} (H) (p)) = 1_{H})))$
36		3anass	$⊢ (p \in B \land p \neq 0_{U} \land {coe}_{1} (p) (\deg_{1} (H) (p)) = 1_{H}) \leftrightarrow (p \in B \land (p \neq 0_{U} \land {coe}_{1} (p) (\deg_{1} (H) (p)) = 1_{H}))$
37	35 36	bitr4di	$⊢ φ \to ((p \in B \land (p \neq 0_{S} \land {coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R})) \leftrightarrow (p \in B \land p \neq 0_{U} \land {coe}_{1} (p) (\deg_{1} (H) (p)) = 1_{H}))$
38	22 37	bitr3d	$⊢ φ \to ((p \in B \land (p \in {Base}_{S} \land p \neq 0_{S} \land {coe}_{1} (p) (\deg_{1} (R) (p)) = 1_{R})) \leftrightarrow (p \in B \land p \neq 0_{U} \land {coe}_{1} (p) (\deg_{1} (H) (p)) = 1_{H}))$
39	13 38	bitr2id	$⊢ φ \to ((p \in B \land p \neq 0_{U} \land {coe}_{1} (p) (\deg_{1} (H) (p)) = 1_{H}) \leftrightarrow (p \in B \land p \in M))$
40		eqid	$⊢ 0_{U} = 0_{U}$
41		eqid	$⊢ \deg_{1} (H) = \deg_{1} (H)$
42		eqid	$⊢ 1_{H} = 1_{H}$
43	3 4 40 41 7 42	ismon1p	$⊢ p \in N \leftrightarrow (p \in B \land p \neq 0_{U} \land {coe}_{1} (p) (\deg_{1} (H) (p)) = 1_{H})$
44		elin	$⊢ p \in (B \cap M) \leftrightarrow (p \in B \land p \in M)$
45	39 43 44	3bitr4g	$⊢ φ \to (p \in N \leftrightarrow p \in (B \cap M))$
46	45	eqrdv	$⊢ φ \to N = B \cap M$

Metamath Proof Explorer

Theorem ressply1mon1p

Proof