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	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
15	4	ringmgp	$⊢ P \in Ring \to N \in Mnd$
16	11 14 15	3syl	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to N \in Mnd$
17		simpr	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to F \in ℕ_{0}$
18		eqid	$⊢ {Base}_{P} = {Base}_{P}$
19	3 2 18	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
20	11 19	syl	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to X \in {Base}_{P}$
21	4 18	mgpbas	$⊢ {Base}_{P} = {Base}_{N}$
22	21 5	mulgnn0cl	$⊢ (N \in Mnd \land F \in ℕ_{0} \land X \in {Base}_{P}) \to F \underset{˙}{\times} X \in {Base}_{P}$
23	16 17 20 22	syl3anc	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to F \underset{˙}{\times} X \in {Base}_{P}$
24		eqid	$⊢ Scalar (P) = Scalar (P)$
25		eqid	$⊢ \cdot_{P} = \cdot_{P}$
26		eqid	$⊢ 1_{Scalar (P)} = 1_{Scalar (P)}$
27	18 24 25 26	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$
28	13 23 27	syl2anc	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to 1_{Scalar (P)} \cdot_{P} (F \underset{˙}{\times} X) = F \underset{˙}{\times} X$
29	9 28	eqtrd	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to 1_{R} \cdot_{P} (F \underset{˙}{\times} X) = F \underset{˙}{\times} X$
30	29	fveq2d	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to D (1_{R} \cdot_{P} (F \underset{˙}{\times} X)) = D (F \underset{˙}{\times} X)$
31		eqid	$⊢ {Base}_{R} = {Base}_{R}$
32		eqid	$⊢ 1_{R} = 1_{R}$
33	31 32	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
34	11 33	syl	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to 1_{R} \in {Base}_{R}$
35		eqid	$⊢ 0_{R} = 0_{R}$
36	32 35	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
37	36	adantr	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to 1_{R} \neq 0_{R}$
38	1 31 2 3 25 4 5 35	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$
39	11 34 37 17 38	syl121anc	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to D (1_{R} \cdot_{P} (F \underset{˙}{\times} X)) = F$
40	30 39	eqtr3d	$⊢ (R \in NzRing \land F \in ℕ_{0}) \to D (F \underset{˙}{\times} X) = F$

Metamath Proof Explorer

Theorem deg1pw

Proof