dchrpt

Description: For any element other than 1, there is a Dirichlet character that is not one at the given element. (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	dchrpt.g	$⊢ G = DChr (N)$
	dchrpt.z	$⊢ Z = ℤ / N ℤ$
	dchrpt.d	$⊢ D = {Base}_{G}$
	dchrpt.b	$⊢ B = {Base}_{Z}$
	dchrpt.1	$⊢ \underset{˙}{1} = 1_{Z}$
	dchrpt.n	$⊢ φ \to N \in ℕ$
	dchrpt.n1	$⊢ φ \to A \neq \underset{˙}{1}$
	dchrpt.a	$⊢ φ \to A \in B$
Assertion	dchrpt	$⊢ φ \to \exists x \in D x (A) \neq 1$

Proof

Step	Hyp	Ref	Expression
1		dchrpt.g	$⊢ G = DChr (N)$
2		dchrpt.z	$⊢ Z = ℤ / N ℤ$
3		dchrpt.d	$⊢ D = {Base}_{G}$
4		dchrpt.b	$⊢ B = {Base}_{Z}$
5		dchrpt.1	$⊢ \underset{˙}{1} = 1_{Z}$
6		dchrpt.n	$⊢ φ \to N \in ℕ$
7		dchrpt.n1	$⊢ φ \to A \neq \underset{˙}{1}$
8		dchrpt.a	$⊢ φ \to A \in B$
9	6	ad3antrrr	$⊢ (((φ \land A \in Unit (Z)) \land w \in Word Unit (Z)) \land (({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) dom DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) \land ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) = Unit (Z))) \to N \in ℕ$
10	7	ad3antrrr	$⊢ (((φ \land A \in Unit (Z)) \land w \in Word Unit (Z)) \land (({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) dom DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) \land ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) = Unit (Z))) \to A \neq \underset{˙}{1}$
11		eqid	$⊢ Unit (Z) = Unit (Z)$
12		eqid	$⊢ {mulGrp}_{Z} ↾_{𝑠} Unit (Z) = {mulGrp}_{Z} ↾_{𝑠} Unit (Z)$
13		eqid	$⊢ \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} = \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))}$
14		oveq1	$⊢ n = b \to n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k) = b \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k)$
15	14	cbvmptv	$⊢ (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k)) = (b \in ℤ ⟼ b \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))$
16		fveq2	$⊢ k = a \to w (k) = w (a)$
17	16	oveq2d	$⊢ k = a \to b \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k) = b \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (a)$
18	17	mpteq2dv	$⊢ k = a \to (b \in ℤ ⟼ b \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k)) = (b \in ℤ ⟼ b \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (a))$
19	15 18	eqtrid	$⊢ k = a \to (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k)) = (b \in ℤ ⟼ b \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (a))$
20	19	rneqd	$⊢ k = a \to ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k)) = ran (b \in ℤ ⟼ b \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (a))$
21	20	cbvmptv	$⊢ (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) = (a \in dom w ⟼ ran (b \in ℤ ⟼ b \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (a)))$
22		simpllr	$⊢ (((φ \land A \in Unit (Z)) \land w \in Word Unit (Z)) \land (({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) dom DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) \land ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) = Unit (Z))) \to A \in Unit (Z)$
23		simplr	$⊢ (((φ \land A \in Unit (Z)) \land w \in Word Unit (Z)) \land (({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) dom DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) \land ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) = Unit (Z))) \to w \in Word Unit (Z)$
24		simprl	$⊢ (((φ \land A \in Unit (Z)) \land w \in Word Unit (Z)) \land (({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) dom DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) \land ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) = Unit (Z))) \to ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) dom DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k)))$
25		simprr	$⊢ (((φ \land A \in Unit (Z)) \land w \in Word Unit (Z)) \land (({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) dom DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) \land ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) = Unit (Z))) \to ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) = Unit (Z)$
26	1 2 3 4 5 9 10 11 12 13 21 22 23 24 25	dchrptlem3	$⊢ (((φ \land A \in Unit (Z)) \land w \in Word Unit (Z)) \land (({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) dom DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) \land ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) = Unit (Z))) \to \exists x \in D x (A) \neq 1$
27	26	3adantr1	$⊢ (((φ \land A \in Unit (Z)) \land w \in Word Unit (Z)) \land ((k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) : dom w ⟶ \{u \in SubGrp ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) \| ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) ↾_{𝑠} u \in (CycGrp \cap ran pGrp)\} \land ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) dom DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) \land ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) = Unit (Z))) \to \exists x \in D x (A) \neq 1$
28	11 12	unitgrpbas	$⊢ Unit (Z) = {Base}_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))}$
29		eqid	$⊢ \{u \in SubGrp ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) \| ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) ↾_{𝑠} u \in (CycGrp \cap ran pGrp)\} = \{u \in SubGrp ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) \| ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) ↾_{𝑠} u \in (CycGrp \cap ran pGrp)\}$
30	6	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
31	2	zncrng	$⊢ N \in ℕ_{0} \to Z \in CRing$
32	11 12	unitabl	$⊢ Z \in CRing \to {mulGrp}_{Z} ↾_{𝑠} Unit (Z) \in Abel$
33	30 31 32	3syl	$⊢ φ \to {mulGrp}_{Z} ↾_{𝑠} Unit (Z) \in Abel$
34	33	adantr	$⊢ (φ \land A \in Unit (Z)) \to {mulGrp}_{Z} ↾_{𝑠} Unit (Z) \in Abel$
35	2 4	znfi	$⊢ N \in ℕ \to B \in Fin$
36	6 35	syl	$⊢ φ \to B \in Fin$
37	4 11	unitss	$⊢ Unit (Z) \subseteq B$
38		ssfi	$⊢ (B \in Fin \land Unit (Z) \subseteq B) \to Unit (Z) \in Fin$
39	36 37 38	sylancl	$⊢ φ \to Unit (Z) \in Fin$
40	39	adantr	$⊢ (φ \land A \in Unit (Z)) \to Unit (Z) \in Fin$
41		eqid	$⊢ (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) = (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k)))$
42	28 29 34 40 13 41	ablfac2	$⊢ (φ \land A \in Unit (Z)) \to \exists w \in Word Unit (Z) ((k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) : dom w ⟶ \{u \in SubGrp ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) \| ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) ↾_{𝑠} u \in (CycGrp \cap ran pGrp)\} \land ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) dom DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) \land ({mulGrp}_{Z} ↾_{𝑠} Unit (Z)) DProd (k \in dom w ⟼ ran (n \in ℤ ⟼ n \cdot_{({mulGrp}_{Z} ↾_{𝑠} Unit (Z))} w (k))) = Unit (Z))$
43	27 42	r19.29a	$⊢ (φ \land A \in Unit (Z)) \to \exists x \in D x (A) \neq 1$
44	1	dchrabl	$⊢ N \in ℕ \to G \in Abel$
45		ablgrp	$⊢ G \in Abel \to G \in Grp$
46		eqid	$⊢ 0_{G} = 0_{G}$
47	3 46	grpidcl	$⊢ G \in Grp \to 0_{G} \in D$
48	6 44 45 47	4syl	$⊢ φ \to 0_{G} \in D$
49		0ne1	$⊢ 0 \neq 1$
50	1 2 3 4 11 48 8	dchrn0	$⊢ φ \to (0_{G} (A) \neq 0 \leftrightarrow A \in Unit (Z))$
51	50	necon1bbid	$⊢ φ \to (\neg A \in Unit (Z) \leftrightarrow 0_{G} (A) = 0)$
52	51	biimpa	$⊢ (φ \land \neg A \in Unit (Z)) \to 0_{G} (A) = 0$
53	52	neeq1d	$⊢ (φ \land \neg A \in Unit (Z)) \to (0_{G} (A) \neq 1 \leftrightarrow 0 \neq 1)$
54	49 53	mpbiri	$⊢ (φ \land \neg A \in Unit (Z)) \to 0_{G} (A) \neq 1$
55		fveq1	$⊢ x = 0_{G} \to x (A) = 0_{G} (A)$
56	55	neeq1d	$⊢ x = 0_{G} \to (x (A) \neq 1 \leftrightarrow 0_{G} (A) \neq 1)$
57	56	rspcev	$⊢ (0_{G} \in D \land 0_{G} (A) \neq 1) \to \exists x \in D x (A) \neq 1$
58	48 54 57	syl2an2r	$⊢ (φ \land \neg A \in Unit (Z)) \to \exists x \in D x (A) \neq 1$
59	43 58	pm2.61dan	$⊢ φ \to \exists x \in D x (A) \neq 1$

Metamath Proof Explorer

Theorem dchrpt

Proof