Metamath Proof Explorer

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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 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 syl5bir ⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → ( ¬ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 ) )
77 76 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ dom 𝑊 ¬ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 ) )
78 61 77 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )