deg1mhm

Description: Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015)

	Ref	Expression
Hypotheses	deg1mhm.d	$⊢ D = \deg_{1} (R)$
	deg1mhm.b	$⊢ B = {Base}_{P}$
	deg1mhm.p	$⊢ P = {Poly}_{1} (R)$
	deg1mhm.z	$⊢ \underset{˙}{0} = 0_{P}$
	deg1mhm.y	$⊢ Y = {mulGrp}_{P} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
	deg1mhm.n	$⊢ N = ℂ_{fld} ↾_{𝑠} ℕ_{0}$
Assertion	deg1mhm	$⊢ R \in Domn \to {D ↾}_{(B ∖ \{\underset{˙}{0}\})} \in (Y MndHom N)$

Proof

Step	Hyp	Ref	Expression
1		deg1mhm.d	$⊢ D = \deg_{1} (R)$
2		deg1mhm.b	$⊢ B = {Base}_{P}$
3		deg1mhm.p	$⊢ P = {Poly}_{1} (R)$
4		deg1mhm.z	$⊢ \underset{˙}{0} = 0_{P}$
5		deg1mhm.y	$⊢ Y = {mulGrp}_{P} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
6		deg1mhm.n	$⊢ N = ℂ_{fld} ↾_{𝑠} ℕ_{0}$
7	3	ply1domn	$⊢ R \in Domn \to P \in Domn$
8		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
9	2 4 8	isdomn3	$⊢ P \in Domn \leftrightarrow (P \in Ring \land B ∖ \{\underset{˙}{0}\} \in SubMnd ({mulGrp}_{P}))$
10	9	simprbi	$⊢ P \in Domn \to B ∖ \{\underset{˙}{0}\} \in SubMnd ({mulGrp}_{P})$
11	7 10	syl	$⊢ R \in Domn \to B ∖ \{\underset{˙}{0}\} \in SubMnd ({mulGrp}_{P})$
12	5	submmnd	$⊢ B ∖ \{\underset{˙}{0}\} \in SubMnd ({mulGrp}_{P}) \to Y \in Mnd$
13	11 12	syl	$⊢ R \in Domn \to Y \in Mnd$
14		nn0subm	$⊢ ℕ_{0} \in SubMnd (ℂ_{fld})$
15	6	submmnd	$⊢ ℕ_{0} \in SubMnd (ℂ_{fld}) \to N \in Mnd$
16	14 15	mp1i	$⊢ R \in Domn \to N \in Mnd$
17	13 16	jca	$⊢ R \in Domn \to (Y \in Mnd \land N \in Mnd)$
18	1 3 2	deg1xrf	$⊢ D : B ⟶ ℝ^{*}$
19		ffn	$⊢ D : B ⟶ ℝ^{*} \to D Fn B$
20	18 19	ax-mp	$⊢ D Fn B$
21		difss	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B$
22		fnssres	$⊢ (D Fn B \land B ∖ \{\underset{˙}{0}\} \subseteq B) \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) Fn (B ∖ \{\underset{˙}{0}\})$
23	20 21 22	mp2an	$⊢ ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) Fn (B ∖ \{\underset{˙}{0}\})$
24	23	a1i	$⊢ R \in Domn \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) Fn (B ∖ \{\underset{˙}{0}\})$
25		fvres	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) = D (x)$
26	25	adantl	$⊢ (R \in Domn \land x \in (B ∖ \{\underset{˙}{0}\})) \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) = D (x)$
27		domnring	$⊢ R \in Domn \to R \in Ring$
28	27	adantr	$⊢ (R \in Domn \land x \in (B ∖ \{\underset{˙}{0}\})) \to R \in Ring$
29		eldifi	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \to x \in B$
30	29	adantl	$⊢ (R \in Domn \land x \in (B ∖ \{\underset{˙}{0}\})) \to x \in B$
31		eldifsni	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \to x \neq \underset{˙}{0}$
32	31	adantl	$⊢ (R \in Domn \land x \in (B ∖ \{\underset{˙}{0}\})) \to x \neq \underset{˙}{0}$
33	1 3 4 2	deg1nn0cl	$⊢ (R \in Ring \land x \in B \land x \neq \underset{˙}{0}) \to D (x) \in ℕ_{0}$
34	28 30 32 33	syl3anc	$⊢ (R \in Domn \land x \in (B ∖ \{\underset{˙}{0}\})) \to D (x) \in ℕ_{0}$
35	26 34	eqeltrd	$⊢ (R \in Domn \land x \in (B ∖ \{\underset{˙}{0}\})) \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) \in ℕ_{0}$
36	35	ralrimiva	$⊢ R \in Domn \to \forall x \in (B ∖ \{\underset{˙}{0}\}) ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) \in ℕ_{0}$
37		ffnfv	$⊢ ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) : B ∖ \{\underset{˙}{0}\} ⟶ ℕ_{0} \leftrightarrow (({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) Fn (B ∖ \{\underset{˙}{0}\}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) \in ℕ_{0})$
38	24 36 37	sylanbrc	$⊢ R \in Domn \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) : B ∖ \{\underset{˙}{0}\} ⟶ ℕ_{0}$
39		eqid	$⊢ RLReg (R) = RLReg (R)$
40		eqid	$⊢ \cdot_{P} = \cdot_{P}$
41	27	adantr	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to R \in Ring$
42	29	ad2antrl	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to x \in B$
43	31	ad2antrl	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to x \neq \underset{˙}{0}$
44		simpl	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to R \in Domn$
45		eqid	$⊢ {coe}_{1} (x) = {coe}_{1} (x)$
46	1 3 4 2 39 45	deg1ldgdomn	$⊢ (R \in Domn \land x \in B \land x \neq \underset{˙}{0}) \to {coe}_{1} (x) (D (x)) \in RLReg (R)$
47	44 42 43 46	syl3anc	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to {coe}_{1} (x) (D (x)) \in RLReg (R)$
48		eldifi	$⊢ y \in (B ∖ \{\underset{˙}{0}\}) \to y \in B$
49	48	ad2antll	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to y \in B$
50		eldifsni	$⊢ y \in (B ∖ \{\underset{˙}{0}\}) \to y \neq \underset{˙}{0}$
51	50	ad2antll	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to y \neq \underset{˙}{0}$
52	1 3 39 2 40 4 41 42 43 47 49 51	deg1mul2	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to D (x \cdot_{P} y) = D (x) + D (y)$
53		domnring	$⊢ P \in Domn \to P \in Ring$
54	7 53	syl	$⊢ R \in Domn \to P \in Ring$
55	54	adantr	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to P \in Ring$
56	2 40	ringcl	$⊢ (P \in Ring \land x \in B \land y \in B) \to x \cdot_{P} y \in B$
57	55 42 49 56	syl3anc	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to x \cdot_{P} y \in B$
58	7	adantr	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to P \in Domn$
59	2 40 4	domnmuln0	$⊢ (P \in Domn \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to x \cdot_{P} y \neq \underset{˙}{0}$
60	58 42 43 49 51 59	syl122anc	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to x \cdot_{P} y \neq \underset{˙}{0}$
61		eldifsn	$⊢ x \cdot_{P} y \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (x \cdot_{P} y \in B \land x \cdot_{P} y \neq \underset{˙}{0})$
62	57 60 61	sylanbrc	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to x \cdot_{P} y \in (B ∖ \{\underset{˙}{0}\})$
63		fvres	$⊢ x \cdot_{P} y \in (B ∖ \{\underset{˙}{0}\}) \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x \cdot_{P} y) = D (x \cdot_{P} y)$
64	62 63	syl	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x \cdot_{P} y) = D (x \cdot_{P} y)$
65		fvres	$⊢ y \in (B ∖ \{\underset{˙}{0}\}) \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (y) = D (y)$
66	25 65	oveqan12d	$⊢ (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\})) \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) + ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (y) = D (x) + D (y)$
67	66	adantl	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) + ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (y) = D (x) + D (y)$
68	52 64 67	3eqtr4d	$⊢ (R \in Domn \land (x \in (B ∖ \{\underset{˙}{0}\}) \land y \in (B ∖ \{\underset{˙}{0}\}))) \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x \cdot_{P} y) = ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) + ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (y)$
69	68	ralrimivva	$⊢ R \in Domn \to \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x \cdot_{P} y) = ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) + ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (y)$
70		eqid	$⊢ 1_{P} = 1_{P}$
71	2 70	ringidcl	$⊢ P \in Ring \to 1_{P} \in B$
72	54 71	syl	$⊢ R \in Domn \to 1_{P} \in B$
73		domnnzr	$⊢ P \in Domn \to P \in NzRing$
74	70 4	nzrnz	$⊢ P \in NzRing \to 1_{P} \neq \underset{˙}{0}$
75	7 73 74	3syl	$⊢ R \in Domn \to 1_{P} \neq \underset{˙}{0}$
76		eldifsn	$⊢ 1_{P} \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (1_{P} \in B \land 1_{P} \neq \underset{˙}{0})$
77	72 75 76	sylanbrc	$⊢ R \in Domn \to 1_{P} \in (B ∖ \{\underset{˙}{0}\})$
78		fvres	$⊢ 1_{P} \in (B ∖ \{\underset{˙}{0}\}) \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (1_{P}) = D (1_{P})$
79	77 78	syl	$⊢ R \in Domn \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (1_{P}) = D (1_{P})$
80	8 70	ringidval	$⊢ 1_{P} = 0_{{mulGrp}_{P}}$
81	5 80	subm0	$⊢ B ∖ \{\underset{˙}{0}\} \in SubMnd ({mulGrp}_{P}) \to 1_{P} = 0_{Y}$
82	11 81	syl	$⊢ R \in Domn \to 1_{P} = 0_{Y}$
83	82	fveq2d	$⊢ R \in Domn \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (1_{P}) = ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (0_{Y})$
84		domnnzr	$⊢ R \in Domn \to R \in NzRing$
85		eqid	$⊢ {Monic}_{1p} (R) = {Monic}_{1p} (R)$
86	3 70 85 1	mon1pid	$⊢ R \in NzRing \to (1_{P} \in {Monic}_{1p} (R) \land D (1_{P}) = 0)$
87	86	simprd	$⊢ R \in NzRing \to D (1_{P}) = 0$
88	84 87	syl	$⊢ R \in Domn \to D (1_{P}) = 0$
89	79 83 88	3eqtr3d	$⊢ R \in Domn \to ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (0_{Y}) = 0$
90	38 69 89	3jca	$⊢ R \in Domn \to (({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) : B ∖ \{\underset{˙}{0}\} ⟶ ℕ_{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x \cdot_{P} y) = ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) + ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (y) \land ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (0_{Y}) = 0)$
91	8 2	mgpbas	$⊢ B = {Base}_{{mulGrp}_{P}}$
92	5 91	ressbas2	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B \to B ∖ \{\underset{˙}{0}\} = {Base}_{Y}$
93	21 92	ax-mp	$⊢ B ∖ \{\underset{˙}{0}\} = {Base}_{Y}$
94		nn0sscn	$⊢ ℕ_{0} \subseteq ℂ$
95		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
96	6 95	ressbas2	$⊢ ℕ_{0} \subseteq ℂ \to ℕ_{0} = {Base}_{N}$
97	94 96	ax-mp	$⊢ ℕ_{0} = {Base}_{N}$
98	2	fvexi	$⊢ B \in V$
99		difexg	$⊢ B \in V \to B ∖ \{\underset{˙}{0}\} \in V$
100	98 99	ax-mp	$⊢ B ∖ \{\underset{˙}{0}\} \in V$
101	8 40	mgpplusg	$⊢ \cdot_{P} = +_{{mulGrp}_{P}}$
102	5 101	ressplusg	$⊢ B ∖ \{\underset{˙}{0}\} \in V \to \cdot_{P} = +_{Y}$
103	100 102	ax-mp	$⊢ \cdot_{P} = +_{Y}$
104		nn0ex	$⊢ ℕ_{0} \in V$
105		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
106	6 105	ressplusg	$⊢ ℕ_{0} \in V \to + = +_{N}$
107	104 106	ax-mp	$⊢ + = +_{N}$
108		eqid	$⊢ 0_{Y} = 0_{Y}$
109		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
110	6 109	subm0	$⊢ ℕ_{0} \in SubMnd (ℂ_{fld}) \to 0 = 0_{N}$
111	14 110	ax-mp	$⊢ 0 = 0_{N}$
112	93 97 103 107 108 111	ismhm	$⊢ {D ↾}_{(B ∖ \{\underset{˙}{0}\})} \in (Y MndHom N) \leftrightarrow ((Y \in Mnd \land N \in Mnd) \land (({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) : B ∖ \{\underset{˙}{0}\} ⟶ ℕ_{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \forall y \in (B ∖ \{\underset{˙}{0}\}) ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x \cdot_{P} y) = ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (x) + ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (y) \land ({D ↾}_{(B ∖ \{\underset{˙}{0}\})}) (0_{Y}) = 0))$
113	17 90 112	sylanbrc	$⊢ R \in Domn \to {D ↾}_{(B ∖ \{\underset{˙}{0}\})} \in (Y MndHom N)$

Metamath Proof Explorer

Theorem deg1mhm

Proof