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 |
|
nnnn0 |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 ) |
8 |
7
|
adantr |
⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℕ0 ) |
9 |
2 4 5
|
znzrhfo |
⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ 𝐵 ) |
10 |
|
fof |
⊢ ( 𝐿 : ℤ –onto→ 𝐵 → 𝐿 : ℤ ⟶ 𝐵 ) |
11 |
8 9 10
|
3syl |
⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝐿 : ℤ ⟶ 𝐵 ) |
12 |
11
|
ffvelrnda |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( 𝐿 ‘ 𝐴 ) ∈ 𝐵 ) |
13 |
|
eqeq1 |
⊢ ( 𝑦 = ( 𝐿 ‘ 𝐴 ) → ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ↔ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) |
14 |
13
|
anbi1d |
⊢ ( 𝑦 = ( 𝐿 ‘ 𝐴 ) → ( ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ↔ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ) |
15 |
14
|
rexbidv |
⊢ ( 𝑦 = ( 𝐿 ‘ 𝐴 ) → ( ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ↔ ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ) |
16 |
15
|
iotabidv |
⊢ ( 𝑦 = ( 𝐿 ‘ 𝐴 ) → ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) = ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ) |
17 |
|
iotaex |
⊢ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ∈ V |
18 |
16 6 17
|
fvmpt3i |
⊢ ( ( 𝐿 ‘ 𝐴 ) ∈ 𝐵 → ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) = ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ) |
19 |
12 18
|
syl |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) = ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ) |
20 |
|
ovex |
⊢ ( 𝐴 /L 𝑁 ) ∈ V |
21 |
|
simprr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) |
22 |
|
simplll |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → 𝑁 ∈ ℕ ) |
23 |
22 7
|
syl |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → 𝑁 ∈ ℕ0 ) |
24 |
|
simplr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → 𝐴 ∈ ℤ ) |
25 |
|
simprl |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → 𝑚 ∈ ℤ ) |
26 |
2 5
|
zndvds |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ↔ 𝑁 ∥ ( 𝐴 − 𝑚 ) ) ) |
27 |
23 24 25 26
|
syl3anc |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ↔ 𝑁 ∥ ( 𝐴 − 𝑚 ) ) ) |
28 |
21 27
|
mpbid |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → 𝑁 ∥ ( 𝐴 − 𝑚 ) ) |
29 |
|
moddvds |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( 𝐴 mod 𝑁 ) = ( 𝑚 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝐴 − 𝑚 ) ) ) |
30 |
22 24 25 29
|
syl3anc |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ( 𝐴 mod 𝑁 ) = ( 𝑚 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝐴 − 𝑚 ) ) ) |
31 |
28 30
|
mpbird |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( 𝐴 mod 𝑁 ) = ( 𝑚 mod 𝑁 ) ) |
32 |
31
|
oveq1d |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( ( 𝑚 mod 𝑁 ) /L 𝑁 ) ) |
33 |
|
simpllr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ¬ 2 ∥ 𝑁 ) |
34 |
|
lgsmod |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( 𝐴 /L 𝑁 ) ) |
35 |
24 22 33 34
|
syl3anc |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ( 𝐴 mod 𝑁 ) /L 𝑁 ) = ( 𝐴 /L 𝑁 ) ) |
36 |
|
lgsmod |
⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( 𝑚 mod 𝑁 ) /L 𝑁 ) = ( 𝑚 /L 𝑁 ) ) |
37 |
25 22 33 36
|
syl3anc |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ( 𝑚 mod 𝑁 ) /L 𝑁 ) = ( 𝑚 /L 𝑁 ) ) |
38 |
32 35 37
|
3eqtr3d |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( 𝐴 /L 𝑁 ) = ( 𝑚 /L 𝑁 ) ) |
39 |
38
|
eqeq2d |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ℎ = ( 𝐴 /L 𝑁 ) ↔ ℎ = ( 𝑚 /L 𝑁 ) ) ) |
40 |
39
|
biimprd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) ) → ( ℎ = ( 𝑚 /L 𝑁 ) → ℎ = ( 𝐴 /L 𝑁 ) ) ) |
41 |
40
|
anassrs |
⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) ∧ ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) → ( ℎ = ( 𝑚 /L 𝑁 ) → ℎ = ( 𝐴 /L 𝑁 ) ) ) |
42 |
41
|
expimpd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) → ℎ = ( 𝐴 /L 𝑁 ) ) ) |
43 |
42
|
rexlimdva |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) → ℎ = ( 𝐴 /L 𝑁 ) ) ) |
44 |
|
fveq2 |
⊢ ( 𝑚 = 𝐴 → ( 𝐿 ‘ 𝑚 ) = ( 𝐿 ‘ 𝐴 ) ) |
45 |
44
|
eqcomd |
⊢ ( 𝑚 = 𝐴 → ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ) |
46 |
45
|
biantrurd |
⊢ ( 𝑚 = 𝐴 → ( ℎ = ( 𝑚 /L 𝑁 ) ↔ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ) |
47 |
|
oveq1 |
⊢ ( 𝑚 = 𝐴 → ( 𝑚 /L 𝑁 ) = ( 𝐴 /L 𝑁 ) ) |
48 |
47
|
eqeq2d |
⊢ ( 𝑚 = 𝐴 → ( ℎ = ( 𝑚 /L 𝑁 ) ↔ ℎ = ( 𝐴 /L 𝑁 ) ) ) |
49 |
46 48
|
bitr3d |
⊢ ( 𝑚 = 𝐴 → ( ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ↔ ℎ = ( 𝐴 /L 𝑁 ) ) ) |
50 |
49
|
rspcev |
⊢ ( ( 𝐴 ∈ ℤ ∧ ℎ = ( 𝐴 /L 𝑁 ) ) → ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) |
51 |
50
|
ex |
⊢ ( 𝐴 ∈ ℤ → ( ℎ = ( 𝐴 /L 𝑁 ) → ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ) |
52 |
51
|
adantl |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( ℎ = ( 𝐴 /L 𝑁 ) → ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ) |
53 |
43 52
|
impbid |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ↔ ℎ = ( 𝐴 /L 𝑁 ) ) ) |
54 |
53
|
adantr |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝐴 /L 𝑁 ) ∈ V ) → ( ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ↔ ℎ = ( 𝐴 /L 𝑁 ) ) ) |
55 |
54
|
iota5 |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) ∧ ( 𝐴 /L 𝑁 ) ∈ V ) → ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) = ( 𝐴 /L 𝑁 ) ) |
56 |
20 55
|
mpan2 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) = ( 𝐴 /L 𝑁 ) ) |
57 |
19 56
|
eqtrd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝐴 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) = ( 𝐴 /L 𝑁 ) ) |