deg1pw

Description: Exact degree of a variable power over a nontrivial ring. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	deg1pw.d	$⊢ D = \deg_{1} (R)$
	deg1pw.p	$⊢ P = {Poly}_{1} (R)$
	deg1pw.x	$⊢ X = {var}_{1} (R)$
	deg1pw.n	$⊢ N = {mulGrp}_{P}$
	deg1pw.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
Assertion	deg1pw	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to D (F \underset{˙}{\times} X) = F$

Proof

Step	Hyp	Ref	Expression
1		deg1pw.d	$⊢ D = \deg_{1} (R)$
2		deg1pw.p	$⊢ P = {Poly}_{1} (R)$
3		deg1pw.x	$⊢ X = {var}_{1} (R)$
4		deg1pw.n	$⊢ N = {mulGrp}_{P}$
5		deg1pw.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
6	2	ply1sca	$⊢ R \in NzRing \to R = Scalar (P)$
7	6	adantr	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to R = Scalar (P)$
8	7	fveq2d	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to 1_{R} = 1_{Scalar (P)}$
9	8	oveq1d	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to 1_{R} \cdot_{P} (F \underset{˙}{\times} X) = 1_{Scalar (P)} \cdot_{P} (F \underset{˙}{\times} X)$
10		nzrring	$⊢ R \in NzRing \to R \in Ring$
11	10	adantr	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to R \in Ring$
12	2	ply1lmod	$⊢ R \in Ring \to P \in LMod$
13	11 12	syl	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to P \in LMod$
14		eqid	$⊢ {Base}_{P} = {Base}_{P}$
15	4 14	mgpbas	$⊢ {Base}_{P} = {Base}_{N}$
16	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
17	4	ringmgp	$⊢ P \in Ring \to N \in Mnd$
18	11 16 17	3syl	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to N \in Mnd$
19		simpr	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to F \in ℕ_{0}$
20	3 2 14	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
21	11 20	syl	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to X \in {Base}_{P}$
22	15 5 18 19 21	mulgnn0cld	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to F \underset{˙}{\times} X \in {Base}_{P}$
23		eqid	$⊢ Scalar (P) = Scalar (P)$
24		eqid	$⊢ \cdot_{P} = \cdot_{P}$
25		eqid	$⊢ 1_{Scalar (P)} = 1_{Scalar (P)}$
26	14 23 24 25	lmodvs1	$⊢ (P \in LMod \land F \underset{˙}{\times} X \in {Base}_{P}) \to 1_{Scalar (P)} \cdot_{P} (F \underset{˙}{\times} X) = F \underset{˙}{\times} X$
27	13 22 26	syl2anc	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to 1_{Scalar (P)} \cdot_{P} (F \underset{˙}{\times} X) = F \underset{˙}{\times} X$
28	9 27	eqtrd	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to 1_{R} \cdot_{P} (F \underset{˙}{\times} X) = F \underset{˙}{\times} X$
29	28	fveq2d	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to D (1_{R} \cdot_{P} (F \underset{˙}{\times} X)) = D (F \underset{˙}{\times} X)$
30		eqid	$⊢ {Base}_{R} = {Base}_{R}$
31		eqid	$⊢ 1_{R} = 1_{R}$
32	30 31	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
33	11 32	syl	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to 1_{R} \in {Base}_{R}$
34		eqid	$⊢ 0_{R} = 0_{R}$
35	31 34	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
36	35	adantr	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to 1_{R} \neq 0_{R}$
37	1 30 2 3 24 4 5 34	deg1tm	$⊢ (R \in Ring \land (1_{R} \in {Base}_{R} \land 1_{R} \neq 0_{R}) \land F \in ℕ_{0}) \to D (1_{R} \cdot_{P} (F \underset{˙}{\times} X)) = F$
38	11 33 36 19 37	syl121anc	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to D (1_{R} \cdot_{P} (F \underset{˙}{\times} X)) = F$
39	29 38	eqtr3d	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to D (F \underset{˙}{\times} X) = F$

Metamath Proof Explorer

Theorem deg1pw

Proof