Metamath Proof Explorer

Theorem lgsdchr

Description: The Legendre symbol function X ( m ) = ( m /L N ) , where N is an odd positive number, is a real Dirichlet character modulo N . (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses lgsdchr.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
lgsdchr.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
lgsdchr.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
lgsdchr.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
lgsdchr.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
lgsdchr.x ⊢ 𝑋 = ( 𝑦 ∈ 𝐵 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
Assertion lgsdchr ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑋 ∈ 𝐷 ∧ 𝑋 : 𝐵 ⟶ ℝ ) )

Proof

Step Hyp Ref Expression
1 lgsdchr.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 lgsdchr.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 lgsdchr.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 lgsdchr.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
5 lgsdchr.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
6 lgsdchr.x ⊢ 𝑋 = ( 𝑦 ∈ 𝐵 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
7 iotaex ⊢ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ∈ V
8 7 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑦 ∈ 𝐵 ) → ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ∈ V )
9 6 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑋 = ( 𝑦 ∈ 𝐵 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ) )
10 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
11 10 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℕ0 )
12 2 4 5 znzrhfo ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ 𝐵 )
13 11 12 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝐿 : ℤ –onto→ 𝐵 )
14 foelrn ⊢ ( ( 𝐿 : ℤ –onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) )
15 13 14 sylan ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) )
16 1 2 3 4 5 6 lgsdchrval ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑎 /L 𝑁 ) )
17 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → 𝑎 ∈ ℤ )
18 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
19 18 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → 𝑁 ∈ ℤ )
20 lgscl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑎 /L 𝑁 ) ∈ ℤ )
21 17 19 20 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑎 /L 𝑁 ) ∈ ℤ )
22 21 zred ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑎 /L 𝑁 ) ∈ ℝ )
23 16 22 eqeltrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) ∈ ℝ )
24 fveq2 ⊢ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( 𝑋 ‘ 𝑥 ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) )
25 24 eleq1d ⊢ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( ( 𝑋 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) ∈ ℝ ) )
26 23 25 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℝ ) )
27 26 rexlimdva ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℝ ) )
28 27 imp ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℝ )
29 15 28 syldan ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℝ )
30 8 9 29 fmpt2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑋 : 𝐵 ⟶ ℝ )
31 ax-resscn ⊢ ℝ ⊆ ℂ
32 fss ⊢ ( ( 𝑋 : 𝐵 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝑋 : 𝐵 ⟶ ℂ )
33 30 31 32 sylancl ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑋 : 𝐵 ⟶ ℂ )
34 eqid ⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
35 4 34 unitss ⊢ ( Unit ‘ 𝑍 ) ⊆ 𝐵
36 foelrn ⊢ ( ( 𝐿 : ℤ –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑏 ∈ ℤ 𝑦 = ( 𝐿 ‘ 𝑏 ) )
37 13 36 sylan ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑏 ∈ ℤ 𝑦 = ( 𝐿 ‘ 𝑏 ) )
38 15 37 anim12dan ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ ∃ 𝑏 ∈ ℤ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) )
39 reeanv ⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) ↔ ( ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ ∃ 𝑏 ∈ ℤ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) )
40 17 adantrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℤ )
41 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℤ )
42 11 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑁 ∈ ℕ0 )
43 lgsdirnn0 ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑎 · 𝑏 ) /L 𝑁 ) = ( ( 𝑎 /L 𝑁 ) · ( 𝑏 /L 𝑁 ) ) )
44 40 41 42 43 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑎 · 𝑏 ) /L 𝑁 ) = ( ( 𝑎 /L 𝑁 ) · ( 𝑏 /L 𝑁 ) ) )
45 2 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
46 11 45 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑍 ∈ CRing )
47 crngring ⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
48 46 47 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑍 ∈ Ring )
49 48 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑍 ∈ Ring )
50 5 zrhrhm ⊢ ( 𝑍 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑍 ) )
51 49 50 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐿 ∈ ( ℤring RingHom 𝑍 ) )
52 zringbas ⊢ ℤ = ( Base ‘ ℤring )
53 zringmulr ⊢ · = ( .r ‘ ℤring )
54 eqid ⊢ ( .r ‘ 𝑍 ) = ( .r ‘ 𝑍 )
55 52 53 54 rhmmul ⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑍 ) ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝐿 ‘ ( 𝑎 · 𝑏 ) ) = ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) )
56 51 40 41 55 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝐿 ‘ ( 𝑎 · 𝑏 ) ) = ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) )
57 56 fveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑎 · 𝑏 ) ) ) = ( 𝑋 ‘ ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) ) )
58 zmulcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 · 𝑏 ) ∈ ℤ )
59 1 2 3 4 5 6 lgsdchrval ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 · 𝑏 ) ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑎 · 𝑏 ) ) ) = ( ( 𝑎 · 𝑏 ) /L 𝑁 ) )
60 58 59 sylan2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑎 · 𝑏 ) ) ) = ( ( 𝑎 · 𝑏 ) /L 𝑁 ) )
61 57 60 eqtr3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑋 ‘ ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) ) = ( ( 𝑎 · 𝑏 ) /L 𝑁 ) )
62 16 adantrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑎 /L 𝑁 ) )
63 1 2 3 4 5 6 lgsdchrval ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑏 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) = ( 𝑏 /L 𝑁 ) )
64 63 adantrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) = ( 𝑏 /L 𝑁 ) )
65 62 64 oveq12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) ) = ( ( 𝑎 /L 𝑁 ) · ( 𝑏 /L 𝑁 ) ) )
66 44 61 65 3eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑋 ‘ ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) ) )
67 oveq12 ⊢ ( ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) = ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) )
68 67 fveq2d ⊢ ( ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( 𝑋 ‘ ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) ) )
69 fveq2 ⊢ ( 𝑦 = ( 𝐿 ‘ 𝑏 ) → ( 𝑋 ‘ 𝑦 ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) )
70 24 69 oveqan12d ⊢ ( ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) ) )
71 68 70 eqeq12d ⊢ ( ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ↔ ( 𝑋 ‘ ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) ) ) )
72 66 71 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
73 72 rexlimdvva ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
74 39 73 syl5bir ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ ∃ 𝑏 ∈ ℤ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
75 74 imp ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ ∃ 𝑏 ∈ ℤ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
76 38 75 syldan ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
77 76 ralrimivva ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
78 ss2ralv ⊢ ( ( Unit ‘ 𝑍 ) ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ ( Unit ‘ 𝑍 ) ∀ 𝑦 ∈ ( Unit ‘ 𝑍 ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
79 35 77 78 mpsyl ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ∀ 𝑥 ∈ ( Unit ‘ 𝑍 ) ∀ 𝑦 ∈ ( Unit ‘ 𝑍 ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
80 1z ⊢ 1 ∈ ℤ
81 1 2 3 4 5 6 lgsdchrval ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 1 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = ( 1 /L 𝑁 ) )
82 80 81 mpan2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = ( 1 /L 𝑁 ) )
83 eqid ⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
84 5 83 zrh1 ⊢ ( 𝑍 ∈ Ring → ( 𝐿 ‘ 1 ) = ( 1r ‘ 𝑍 ) )
85 48 84 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝐿 ‘ 1 ) = ( 1r ‘ 𝑍 ) )
86 85 fveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
87 18 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℤ )
88 1lgs ⊢ ( 𝑁 ∈ ℤ → ( 1 /L 𝑁 ) = 1 )
89 87 88 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 1 /L 𝑁 ) = 1 )
90 82 86 89 3eqtr3d ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
91 lgsne0 ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑎 /L 𝑁 ) ≠ 0 ↔ ( 𝑎 gcd 𝑁 ) = 1 ) )
92 17 19 91 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝑎 /L 𝑁 ) ≠ 0 ↔ ( 𝑎 gcd 𝑁 ) = 1 ) )
93 92 biimpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝑎 /L 𝑁 ) ≠ 0 → ( 𝑎 gcd 𝑁 ) = 1 ) )
94 16 neeq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) ≠ 0 ↔ ( 𝑎 /L 𝑁 ) ≠ 0 ) )
95 2 34 5 znunit ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑎 ∈ ℤ ) → ( ( 𝐿 ‘ 𝑎 ) ∈ ( Unit ‘ 𝑍 ) ↔ ( 𝑎 gcd 𝑁 ) = 1 ) )
96 11 95 sylan ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝐿 ‘ 𝑎 ) ∈ ( Unit ‘ 𝑍 ) ↔ ( 𝑎 gcd 𝑁 ) = 1 ) )
97 93 94 96 3imtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) ≠ 0 → ( 𝐿 ‘ 𝑎 ) ∈ ( Unit ‘ 𝑍 ) ) )
98 24 neeq1d ⊢ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 ↔ ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) ≠ 0 ) )
99 eleq1 ⊢ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( 𝑥 ∈ ( Unit ‘ 𝑍 ) ↔ ( 𝐿 ‘ 𝑎 ) ∈ ( Unit ‘ 𝑍 ) ) )
100 98 99 imbi12d ⊢ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ↔ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) ≠ 0 → ( 𝐿 ‘ 𝑎 ) ∈ ( Unit ‘ 𝑍 ) ) ) )
101 97 100 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) )
102 101 rexlimdva ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) )
103 102 imp ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) )
104 15 103 syldan ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) )
105 104 ralrimiva ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) )
106 79 90 105 3jca ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ∀ 𝑥 ∈ ( Unit ‘ 𝑍 ) ∀ 𝑦 ∈ ( Unit ‘ 𝑍 ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ∧ ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) )
107 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℕ )
108 1 2 4 34 107 3 dchrelbas3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 : 𝐵 ⟶ ℂ ∧ ( ∀ 𝑥 ∈ ( Unit ‘ 𝑍 ) ∀ 𝑦 ∈ ( Unit ‘ 𝑍 ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ∧ ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) ) ) )
109 33 106 108 mpbir2and ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑋 ∈ 𝐷 )
110 109 30 jca ⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑋 ∈ 𝐷 ∧ 𝑋 : 𝐵 ⟶ ℝ ) )