Metamath Proof Explorer

Theorem 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 ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrpt.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrpt.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrpt.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
dchrpt.1 ⊢ 1 = ( 1r ‘ 𝑍 )
dchrpt.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
dchrpt.n1 ⊢ ( 𝜑 → 𝐴 ≠ 1 )
dchrpt.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion dchrpt ( 𝜑 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 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.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
9 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) ∧ 𝑤 ∈ Word ( Unit ‘ 𝑍 ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) dom DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ) = ( Unit ‘ 𝑍 ) ) ) → 𝑁 ∈ ℕ )
10 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) ∧ 𝑤 ∈ Word ( Unit ‘ 𝑍 ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) dom DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ) = ( Unit ‘ 𝑍 ) ) ) → 𝐴 ≠ 1 )
11 eqid ⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
12 eqid ⊢ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) = ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) )
13 eqid ⊢ ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) = ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) )
14 oveq1 ⊢ ( 𝑛 = 𝑏 → ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) = ( 𝑏 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) )
15 14 cbvmptv ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑏 ∈ ℤ ↦ ( 𝑏 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) )
16 fveq2 ⊢ ( 𝑘 = 𝑎 → ( 𝑤 ‘ 𝑘 ) = ( 𝑤 ‘ 𝑎 ) )
17 16 oveq2d ⊢ ( 𝑘 = 𝑎 → ( 𝑏 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) = ( 𝑏 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑎 ) ) )
18 17 mpteq2dv ⊢ ( 𝑘 = 𝑎 → ( 𝑏 ∈ ℤ ↦ ( 𝑏 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑏 ∈ ℤ ↦ ( 𝑏 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑎 ) ) ) )
19 15 18 syl5eq ⊢ ( 𝑘 = 𝑎 → ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑏 ∈ ℤ ↦ ( 𝑏 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑎 ) ) ) )
20 19 rneqd ⊢ ( 𝑘 = 𝑎 → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) = ran ( 𝑏 ∈ ℤ ↦ ( 𝑏 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑎 ) ) ) )
21 20 cbvmptv ⊢ ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) = ( 𝑎 ∈ dom 𝑤 ↦ ran ( 𝑏 ∈ ℤ ↦ ( 𝑏 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑎 ) ) ) )
22 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) ∧ 𝑤 ∈ Word ( Unit ‘ 𝑍 ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) dom DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ) = ( Unit ‘ 𝑍 ) ) ) → 𝐴 ∈ ( Unit ‘ 𝑍 ) )
23 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) ∧ 𝑤 ∈ Word ( Unit ‘ 𝑍 ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) dom DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ) = ( Unit ‘ 𝑍 ) ) ) → 𝑤 ∈ Word ( Unit ‘ 𝑍 ) )
24 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) ∧ 𝑤 ∈ Word ( Unit ‘ 𝑍 ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) dom DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ) = ( Unit ‘ 𝑍 ) ) ) → ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) dom DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) )
25 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) ∧ 𝑤 ∈ Word ( Unit ‘ 𝑍 ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) dom DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ) = ( Unit ‘ 𝑍 ) ) ) → ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ) = ( Unit ‘ 𝑍 ) )
26 1 2 3 4 5 9 10 11 12 13 21 22 23 24 25 dchrptlem3 ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) ∧ 𝑤 ∈ Word ( Unit ‘ 𝑍 ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) dom DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ) = ( Unit ‘ 𝑍 ) ) ) → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )
27 26 3adantr1 ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) ∧ 𝑤 ∈ Word ( Unit ‘ 𝑍 ) ) ∧ ( ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) : dom 𝑤 ⟶ { 𝑢 ∈ ( SubGrp ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ∣ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ↾s 𝑢 ) ∈ ( CycGrp ∩ ran pGrp ) } ∧ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) dom DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ) = ( Unit ‘ 𝑍 ) ) ) → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )
28 11 12 unitgrpbas ⊢ ( Unit ‘ 𝑍 ) = ( Base ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) )
29 eqid ⊢ { 𝑢 ∈ ( SubGrp ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ∣ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ↾s 𝑢 ) ∈ ( CycGrp ∩ ran pGrp ) } = { 𝑢 ∈ ( SubGrp ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ∣ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ↾s 𝑢 ) ∈ ( CycGrp ∩ ran pGrp ) }
30 6 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
31 2 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
32 11 12 unitabl ⊢ ( 𝑍 ∈ CRing → ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ∈ Abel )
33 30 31 32 3syl ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ∈ Abel )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) → ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ∈ Abel )
35 2 4 znfi ⊢ ( 𝑁 ∈ ℕ → 𝐵 ∈ Fin )
36 6 35 syl ⊢ ( 𝜑 → 𝐵 ∈ Fin )
37 4 11 unitss ⊢ ( Unit ‘ 𝑍 ) ⊆ 𝐵
38 ssfi ⊢ ( ( 𝐵 ∈ Fin ∧ ( Unit ‘ 𝑍 ) ⊆ 𝐵 ) → ( Unit ‘ 𝑍 ) ∈ Fin )
39 36 37 38 sylancl ⊢ ( 𝜑 → ( Unit ‘ 𝑍 ) ∈ Fin )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) → ( Unit ‘ 𝑍 ) ∈ Fin )
41 eqid ⊢ ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) = ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) )
42 28 29 34 40 13 41 ablfac2 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) → ∃ 𝑤 ∈ Word ( Unit ‘ 𝑍 ) ( ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) : dom 𝑤 ⟶ { 𝑢 ∈ ( SubGrp ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ∣ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ↾s 𝑢 ) ∈ ( CycGrp ∩ ran pGrp ) } ∧ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) dom DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ∧ ( ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) DProd ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s ( Unit ‘ 𝑍 ) ) ) ( 𝑤 ‘ 𝑘 ) ) ) ) ) = ( Unit ‘ 𝑍 ) ) )
43 27 42 r19.29a ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )
44 1 dchrabl ⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )
45 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
46 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
47 3 46 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝐷 )
48 6 44 45 47 4syl ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ 𝐷 )
49 0ne1 ⊢ 0 ≠ 1
50 1 2 3 4 11 48 8 dchrn0 ⊢ ( 𝜑 → ( ( ( 0g ‘ 𝐺 ) ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) )
51 50 necon1bbid ⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ( Unit ‘ 𝑍 ) ↔ ( ( 0g ‘ 𝐺 ) ‘ 𝐴 ) = 0 ) )
52 51 biimpa ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) → ( ( 0g ‘ 𝐺 ) ‘ 𝐴 ) = 0 )
53 52 neeq1d ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) → ( ( ( 0g ‘ 𝐺 ) ‘ 𝐴 ) ≠ 1 ↔ 0 ≠ 1 ) )
54 49 53 mpbiri ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) → ( ( 0g ‘ 𝐺 ) ‘ 𝐴 ) ≠ 1 )
55 fveq1 ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( 𝑥 ‘ 𝐴 ) = ( ( 0g ‘ 𝐺 ) ‘ 𝐴 ) )
56 55 neeq1d ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( ( 𝑥 ‘ 𝐴 ) ≠ 1 ↔ ( ( 0g ‘ 𝐺 ) ‘ 𝐴 ) ≠ 1 ) )
57 56 rspcev ⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝐷 ∧ ( ( 0g ‘ 𝐺 ) ‘ 𝐴 ) ≠ 1 ) → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )
58 48 54 57 syl2an2r ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )
59 43 58 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐷 ( 𝑥 ‘ 𝐴 ) ≠ 1 )