Theorem dchrptlem3

Description: Lemma for dchrpt . (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	dchrpt.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrpt.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchrpt.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	dchrpt.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
	dchrpt.1	⊢ 1 = ( 1r ‘ 𝑍 )
	dchrpt.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	dchrpt.n1	⊢ ( 𝜑 → 𝐴 ≠ 1 )
	dchrpt.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
	dchrpt.h	⊢ 𝐻 = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 )
	dchrpt.m	⊢ · = ( .g ‘ 𝐻 )
	dchrpt.s	⊢ 𝑆 = ( 𝑘 ∈ dom 𝑊 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) )
	dchrpt.au	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	dchrpt.w	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑈 )
	dchrpt.2	⊢ ( 𝜑 → 𝐻 dom DProd 𝑆 )
	dchrpt.3	⊢ ( 𝜑 → ( 𝐻 DProd 𝑆 ) = 𝑈 )
Assertion	dchrptlem3	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )

Proof

Step	Hyp	Ref	Expression
1		dchrpt.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchrpt.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		dchrpt.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
4		dchrpt.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
5		dchrpt.1	⊢ 1 = ( 1r ‘ 𝑍 )
6		dchrpt.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7		dchrpt.n1	⊢ ( 𝜑 → 𝐴 ≠ 1 )
8		dchrpt.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
9		dchrpt.h	⊢ 𝐻 = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 )
10		dchrpt.m	⊢ · = ( .g ‘ 𝐻 )
11		dchrpt.s	⊢ 𝑆 = ( 𝑘 ∈ dom 𝑊 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) )
12		dchrpt.au	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
13		dchrpt.w	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑈 )
14		dchrpt.2	⊢ ( 𝜑 → 𝐻 dom DProd 𝑆 )
15		dchrpt.3	⊢ ( 𝜑 → ( 𝐻 DProd 𝑆 ) = 𝑈 )
16	6	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
17	2	zncrng	⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
18	16 17	syl	⊢ ( 𝜑 → 𝑍 ∈ CRing )
19		crngring	⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
20	18 19	syl	⊢ ( 𝜑 → 𝑍 ∈ Ring )
21	8 9	unitgrp	⊢ ( 𝑍 ∈ Ring → 𝐻 ∈ Grp )
22	20 21	syl	⊢ ( 𝜑 → 𝐻 ∈ Grp )
23	22	grpmndd	⊢ ( 𝜑 → 𝐻 ∈ Mnd )
24	13	dmexd	⊢ ( 𝜑 → dom 𝑊 ∈ V )
25		eqid	⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
26	25	gsumz	⊢ ( ( 𝐻 ∈ Mnd ∧ dom 𝑊 ∈ V ) → ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ ( 0g ‘ 𝐻 ) ) ) = ( 0g ‘ 𝐻 ) )
27	23 24 26	syl2anc	⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ ( 0g ‘ 𝐻 ) ) ) = ( 0g ‘ 𝐻 ) )
28	8 9 5	unitgrpid	⊢ ( 𝑍 ∈ Ring → 1 = ( 0g ‘ 𝐻 ) )
29	20 28	syl	⊢ ( 𝜑 → 1 = ( 0g ‘ 𝐻 ) )
30	29	mpteq2dv	⊢ ( 𝜑 → ( 𝑎 ∈ dom 𝑊 ↦ 1 ) = ( 𝑎 ∈ dom 𝑊 ↦ ( 0g ‘ 𝐻 ) ) )
31	30	oveq2d	⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ 1 ) ) = ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ ( 0g ‘ 𝐻 ) ) ) )
32	27 31 29	3eqtr4d	⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ 1 ) ) = 1 )
33	7 32	neeqtrrd	⊢ ( 𝜑 → 𝐴 ≠ ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ 1 ) ) )
34		zex	⊢ ℤ ∈ V
35	34	mptex	⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) ∈ V
36	35	rnex	⊢ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) ∈ V
37	36 11	dmmpti	⊢ dom 𝑆 = dom 𝑊
38	37	a1i	⊢ ( 𝜑 → dom 𝑆 = dom 𝑊 )
39		eqid	⊢ ( 𝐻 dProj 𝑆 ) = ( 𝐻 dProj 𝑆 )
40	12 15	eleqtrrd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐻 DProd 𝑆 ) )
41		eqid	⊢ { ℎ ∈ X 𝑖 ∈ dom 𝑊 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐻 ) } = { ℎ ∈ X 𝑖 ∈ dom 𝑊 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐻 ) }
42	29	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → 1 = ( 0g ‘ 𝐻 ) )
43	14 38	dprdf2	⊢ ( 𝜑 → 𝑆 : dom 𝑊 ⟶ ( SubGrp ‘ 𝐻 ) )
44	43	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → ( 𝑆 ‘ 𝑎 ) ∈ ( SubGrp ‘ 𝐻 ) )
45	25	subg0cl	⊢ ( ( 𝑆 ‘ 𝑎 ) ∈ ( SubGrp ‘ 𝐻 ) → ( 0g ‘ 𝐻 ) ∈ ( 𝑆 ‘ 𝑎 ) )
46	44 45	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → ( 0g ‘ 𝐻 ) ∈ ( 𝑆 ‘ 𝑎 ) )
47	42 46	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → 1 ∈ ( 𝑆 ‘ 𝑎 ) )
48	5	fvexi	⊢ 1 ∈ V
49	48	a1i	⊢ ( 𝜑 → 1 ∈ V )
50	24 49	fczfsuppd	⊢ ( 𝜑 → ( dom 𝑊 × { 1 } ) finSupp 1 )
51		fconstmpt	⊢ ( dom 𝑊 × { 1 } ) = ( 𝑎 ∈ dom 𝑊 ↦ 1 )
52	51	eqcomi	⊢ ( 𝑎 ∈ dom 𝑊 ↦ 1 ) = ( dom 𝑊 × { 1 } )
53	52	a1i	⊢ ( 𝜑 → ( 𝑎 ∈ dom 𝑊 ↦ 1 ) = ( dom 𝑊 × { 1 } ) )
54	29	eqcomd	⊢ ( 𝜑 → ( 0g ‘ 𝐻 ) = 1 )
55	50 53 54	3brtr4d	⊢ ( 𝜑 → ( 𝑎 ∈ dom 𝑊 ↦ 1 ) finSupp ( 0g ‘ 𝐻 ) )
56	41 14 38 47 55	dprdwd	⊢ ( 𝜑 → ( 𝑎 ∈ dom 𝑊 ↦ 1 ) ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑊 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐻 ) } )
57	14 38 39 40 25 41 56	dpjeq	⊢ ( 𝜑 → ( 𝐴 = ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ 1 ) ) ↔ ∀ 𝑎 ∈ dom 𝑊 ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 ) )
58	57	necon3abid	⊢ ( 𝜑 → ( 𝐴 ≠ ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ 1 ) ) ↔ ¬ ∀ 𝑎 ∈ dom 𝑊 ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 ) )
59	33 58	mpbid	⊢ ( 𝜑 → ¬ ∀ 𝑎 ∈ dom 𝑊 ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 )
60		rexnal	⊢ ( ∃ 𝑎 ∈ dom 𝑊 ¬ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 ↔ ¬ ∀ 𝑎 ∈ dom 𝑊 ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 )
61	59 60	sylibr	⊢ ( 𝜑 → ∃ 𝑎 ∈ dom 𝑊 ¬ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 )
62		df-ne	⊢ ( ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ↔ ¬ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 )
63	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → 𝑁 ∈ ℕ )
64	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → 𝐴 ≠ 1 )
65	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → 𝐴 ∈ 𝑈 )
66	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → 𝑊 ∈ Word 𝑈 )
67	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → 𝐻 dom DProd 𝑆 )
68	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → ( 𝐻 DProd 𝑆 ) = 𝑈 )
69		eqid	⊢ ( od ‘ 𝐻 ) = ( od ‘ 𝐻 )
70		eqid	⊢ ( - 1 ↑𝑐 ( 2 / ( ( od ‘ 𝐻 ) ‘ ( 𝑊 ‘ 𝑎 ) ) ) ) = ( - 1 ↑𝑐 ( 2 / ( ( od ‘ 𝐻 ) ‘ ( 𝑊 ‘ 𝑎 ) ) ) )
71		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → 𝑎 ∈ dom 𝑊 )
72		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 )
73		eqid	⊢ ( 𝑢 ∈ 𝑈 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝑢 ) = ( 𝑚 · ( 𝑊 ‘ 𝑎 ) ) ∧ ℎ = ( ( - 1 ↑𝑐 ( 2 / ( ( od ‘ 𝐻 ) ‘ ( 𝑊 ‘ 𝑎 ) ) ) ) ↑ 𝑚 ) ) ) ) = ( 𝑢 ∈ 𝑈 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝑢 ) = ( 𝑚 · ( 𝑊 ‘ 𝑎 ) ) ∧ ℎ = ( ( - 1 ↑𝑐 ( 2 / ( ( od ‘ 𝐻 ) ‘ ( 𝑊 ‘ 𝑎 ) ) ) ) ↑ 𝑚 ) ) ) )
74	1 2 3 4 5 63 64 8 9 10 11 65 66 67 68 39 69 70 71 72 73	dchrptlem2	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )
75	74	expr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → ( ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 ) )
76	62 75	biimtrrid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → ( ¬ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 ) )
77	76	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ dom 𝑊 ¬ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 ) )
78	61 77	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )