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 grpmnd ⊢ ( 𝐻 ∈ Grp → 𝐻 ∈ Mnd )
24 22 23 syl ⊢ ( 𝜑 → 𝐻 ∈ Mnd )
25 13 dmexd ⊢ ( 𝜑 → dom 𝑊 ∈ V )
26 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
27 26 gsumz ⊢ ( ( 𝐻 ∈ Mnd ∧ dom 𝑊 ∈ V ) → ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ ( 0g ‘ 𝐻 ) ) ) = ( 0g ‘ 𝐻 ) )
28 24 25 27 syl2anc ⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ ( 0g ‘ 𝐻 ) ) ) = ( 0g ‘ 𝐻 ) )
29 8 9 5 unitgrpid ⊢ ( 𝑍 ∈ Ring → 1 = ( 0g ‘ 𝐻 ) )
30 20 29 syl ⊢ ( 𝜑 → 1 = ( 0g ‘ 𝐻 ) )
31 30 mpteq2dv ⊢ ( 𝜑 → ( 𝑎 ∈ dom 𝑊 ↦ 1 ) = ( 𝑎 ∈ dom 𝑊 ↦ ( 0g ‘ 𝐻 ) ) )
32 31 oveq2d ⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ 1 ) ) = ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ ( 0g ‘ 𝐻 ) ) ) )
33 28 32 30 3eqtr4d ⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ 1 ) ) = 1 )
34 7 33 neeqtrrd ⊢ ( 𝜑 → 𝐴 ≠ ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ 1 ) ) )
35 zex ⊢ ℤ ∈ V
36 35 mptex ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) ∈ V
37 36 rnex ⊢ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) ∈ V
38 37 11 dmmpti ⊢ dom 𝑆 = dom 𝑊
39 38 a1i ⊢ ( 𝜑 → dom 𝑆 = dom 𝑊 )
40 eqid ⊢ ( 𝐻 dProj 𝑆 ) = ( 𝐻 dProj 𝑆 )
41 12 15 eleqtrrd ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐻 DProd 𝑆 ) )
42 eqid ⊢ { ℎ ∈ X 𝑖 ∈ dom 𝑊 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐻 ) } = { ℎ ∈ X 𝑖 ∈ dom 𝑊 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐻 ) }
43 30 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → 1 = ( 0g ‘ 𝐻 ) )
44 14 39 dprdf2 ⊢ ( 𝜑 → 𝑆 : dom 𝑊 ⟶ ( SubGrp ‘ 𝐻 ) )
45 44 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → ( 𝑆 ‘ 𝑎 ) ∈ ( SubGrp ‘ 𝐻 ) )
46 26 subg0cl ⊢ ( ( 𝑆 ‘ 𝑎 ) ∈ ( SubGrp ‘ 𝐻 ) → ( 0g ‘ 𝐻 ) ∈ ( 𝑆 ‘ 𝑎 ) )
47 45 46 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → ( 0g ‘ 𝐻 ) ∈ ( 𝑆 ‘ 𝑎 ) )
48 43 47 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → 1 ∈ ( 𝑆 ‘ 𝑎 ) )
49 5 fvexi ⊢ 1 ∈ V
50 49 a1i ⊢ ( 𝜑 → 1 ∈ V )
51 25 50 fczfsuppd ⊢ ( 𝜑 → ( dom 𝑊 × { 1 } ) finSupp 1 )
52 fconstmpt ⊢ ( dom 𝑊 × { 1 } ) = ( 𝑎 ∈ dom 𝑊 ↦ 1 )
53 52 eqcomi ⊢ ( 𝑎 ∈ dom 𝑊 ↦ 1 ) = ( dom 𝑊 × { 1 } )
54 53 a1i ⊢ ( 𝜑 → ( 𝑎 ∈ dom 𝑊 ↦ 1 ) = ( dom 𝑊 × { 1 } ) )
55 30 eqcomd ⊢ ( 𝜑 → ( 0g ‘ 𝐻 ) = 1 )
56 51 54 55 3brtr4d ⊢ ( 𝜑 → ( 𝑎 ∈ dom 𝑊 ↦ 1 ) finSupp ( 0g ‘ 𝐻 ) )
57 42 14 39 48 56 dprdwd ⊢ ( 𝜑 → ( 𝑎 ∈ dom 𝑊 ↦ 1 ) ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑊 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐻 ) } )
58 14 39 40 41 26 42 57 dpjeq ⊢ ( 𝜑 → ( 𝐴 = ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ 1 ) ) ↔ ∀ 𝑎 ∈ dom 𝑊 ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 ) )
59 58 necon3abid ⊢ ( 𝜑 → ( 𝐴 ≠ ( 𝐻 Σg ( 𝑎 ∈ dom 𝑊 ↦ 1 ) ) ↔ ¬ ∀ 𝑎 ∈ dom 𝑊 ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 ) )
60 34 59 mpbid ⊢ ( 𝜑 → ¬ ∀ 𝑎 ∈ dom 𝑊 ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 )
61 rexnal ⊢ ( ∃ 𝑎 ∈ dom 𝑊 ¬ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 ↔ ¬ ∀ 𝑎 ∈ dom 𝑊 ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 )
62 60 61 sylibr ⊢ ( 𝜑 → ∃ 𝑎 ∈ dom 𝑊 ¬ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 )
63 df-ne ⊢ ( ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ↔ ¬ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 )
64 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → 𝑁 ∈ ℕ )
65 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → 𝐴 ≠ 1 )
66 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → 𝐴 ∈ 𝑈 )
67 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → 𝑊 ∈ Word 𝑈 )
68 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → 𝐻 dom DProd 𝑆 )
69 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → ( 𝐻 DProd 𝑆 ) = 𝑈 )
70 eqid ⊢ ( od ‘ 𝐻 ) = ( od ‘ 𝐻 )
71 eqid ⊢ ( - 1 ↑𝑐 ( 2 / ( ( od ‘ 𝐻 ) ‘ ( 𝑊 ‘ 𝑎 ) ) ) ) = ( - 1 ↑𝑐 ( 2 / ( ( od ‘ 𝐻 ) ‘ ( 𝑊 ‘ 𝑎 ) ) ) )
72 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → 𝑎 ∈ dom 𝑊 )
73 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 )
74 eqid ⊢ ( 𝑢 ∈ 𝑈 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝑢 ) = ( 𝑚 · ( 𝑊 ‘ 𝑎 ) ) ∧ ℎ = ( ( - 1 ↑𝑐 ( 2 / ( ( od ‘ 𝐻 ) ‘ ( 𝑊 ‘ 𝑎 ) ) ) ) ↑ 𝑚 ) ) ) ) = ( 𝑢 ∈ 𝑈 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝑢 ) = ( 𝑚 · ( 𝑊 ‘ 𝑎 ) ) ∧ ℎ = ( ( - 1 ↑𝑐 ( 2 / ( ( od ‘ 𝐻 ) ‘ ( 𝑊 ‘ 𝑎 ) ) ) ) ↑ 𝑚 ) ) ) )
75 1 2 3 4 5 64 65 8 9 10 11 66 67 68 69 40 70 71 72 73 74 dchrptlem2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ dom 𝑊 ∧ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 ) ) → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )
76 75 expr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → ( ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) ≠ 1 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 ) )
77 63 76 syl5bir ⊢ ( ( 𝜑 ∧ 𝑎 ∈ dom 𝑊 ) → ( ¬ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 ) )
78 77 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ dom 𝑊 ¬ ( ( ( 𝐻 dProj 𝑆 ) ‘ 𝑎 ) ‘ 𝐴 ) = 1 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 ) )
79 62 78 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )