Proof of Theorem lgsdchrval
Step | Hyp | Ref
| Expression |
1 | | nnnn0 12476 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
2 | 1 | adantr 482 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑁 ∈
ℕ0) |
3 | | lgsdchr.z |
. . . . . 6
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
4 | | lgsdchr.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑍) |
5 | | lgsdchr.l |
. . . . . 6
⊢ 𝐿 = (ℤRHom‘𝑍) |
6 | 3, 4, 5 | znzrhfo 21095 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→𝐵) |
7 | | fof 6803 |
. . . . 5
⊢ (𝐿:ℤ–onto→𝐵 → 𝐿:ℤ⟶𝐵) |
8 | 2, 6, 7 | 3syl 18 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝐿:ℤ⟶𝐵) |
9 | 8 | ffvelcdmda 7084 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) → (𝐿‘𝐴) ∈ 𝐵) |
10 | | eqeq1 2737 |
. . . . . . 7
⊢ (𝑦 = (𝐿‘𝐴) → (𝑦 = (𝐿‘𝑚) ↔ (𝐿‘𝐴) = (𝐿‘𝑚))) |
11 | 10 | anbi1d 631 |
. . . . . 6
⊢ (𝑦 = (𝐿‘𝐴) → ((𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) ↔ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
12 | 11 | rexbidv 3179 |
. . . . 5
⊢ (𝑦 = (𝐿‘𝐴) → (∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) ↔ ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
13 | 12 | iotabidv 6525 |
. . . 4
⊢ (𝑦 = (𝐿‘𝐴) → (℩ℎ∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))) = (℩ℎ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
14 | | lgsdchr.x |
. . . 4
⊢ 𝑋 = (𝑦 ∈ 𝐵 ↦ (℩ℎ∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
15 | | iotaex 6514 |
. . . 4
⊢
(℩ℎ∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))) ∈ V |
16 | 13, 14, 15 | fvmpt3i 7001 |
. . 3
⊢ ((𝐿‘𝐴) ∈ 𝐵 → (𝑋‘(𝐿‘𝐴)) = (℩ℎ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
17 | 9, 16 | syl 17 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) → (𝑋‘(𝐿‘𝐴)) = (℩ℎ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
18 | | ovex 7439 |
. . 3
⊢ (𝐴 /L 𝑁) ∈ V |
19 | | simprr 772 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → (𝐿‘𝐴) = (𝐿‘𝑚)) |
20 | | simplll 774 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → 𝑁 ∈ ℕ) |
21 | 20, 1 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → 𝑁 ∈
ℕ0) |
22 | | simplr 768 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → 𝐴 ∈ ℤ) |
23 | | simprl 770 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → 𝑚 ∈ ℤ) |
24 | 3, 5 | zndvds 21097 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝑚 ∈ ℤ)
→ ((𝐿‘𝐴) = (𝐿‘𝑚) ↔ 𝑁 ∥ (𝐴 − 𝑚))) |
25 | 21, 22, 23, 24 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → ((𝐿‘𝐴) = (𝐿‘𝑚) ↔ 𝑁 ∥ (𝐴 − 𝑚))) |
26 | 19, 25 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → 𝑁 ∥ (𝐴 − 𝑚)) |
27 | | moddvds 16205 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝐴 mod 𝑁) = (𝑚 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝑚))) |
28 | 20, 22, 23, 27 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → ((𝐴 mod 𝑁) = (𝑚 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝑚))) |
29 | 26, 28 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → (𝐴 mod 𝑁) = (𝑚 mod 𝑁)) |
30 | 29 | oveq1d 7421 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → ((𝐴 mod 𝑁) /L 𝑁) = ((𝑚 mod 𝑁) /L 𝑁)) |
31 | | simpllr 775 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → ¬ 2 ∥ 𝑁) |
32 | | lgsmod 26816 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑁) = (𝐴 /L 𝑁)) |
33 | 22, 20, 31, 32 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → ((𝐴 mod 𝑁) /L 𝑁) = (𝐴 /L 𝑁)) |
34 | | lgsmod 26816 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → ((𝑚 mod 𝑁) /L 𝑁) = (𝑚 /L 𝑁)) |
35 | 23, 20, 31, 34 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → ((𝑚 mod 𝑁) /L 𝑁) = (𝑚 /L 𝑁)) |
36 | 30, 33, 35 | 3eqtr3d 2781 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → (𝐴 /L 𝑁) = (𝑚 /L 𝑁)) |
37 | 36 | eqeq2d 2744 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → (ℎ = (𝐴 /L 𝑁) ↔ ℎ = (𝑚 /L 𝑁))) |
38 | 37 | biimprd 247 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → (ℎ = (𝑚 /L 𝑁) → ℎ = (𝐴 /L 𝑁))) |
39 | 38 | anassrs 469 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ ¬ 2 ∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ 𝑚 ∈ ℤ) ∧ (𝐿‘𝐴) = (𝐿‘𝑚)) → (ℎ = (𝑚 /L 𝑁) → ℎ = (𝐴 /L 𝑁))) |
40 | 39 | expimpd 455 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → (((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) → ℎ = (𝐴 /L 𝑁))) |
41 | 40 | rexlimdva 3156 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) →
(∃𝑚 ∈ ℤ
((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) → ℎ = (𝐴 /L 𝑁))) |
42 | | fveq2 6889 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝐴 → (𝐿‘𝑚) = (𝐿‘𝐴)) |
43 | 42 | eqcomd 2739 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝐴 → (𝐿‘𝐴) = (𝐿‘𝑚)) |
44 | 43 | biantrurd 534 |
. . . . . . . . . 10
⊢ (𝑚 = 𝐴 → (ℎ = (𝑚 /L 𝑁) ↔ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
45 | | oveq1 7413 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝐴 → (𝑚 /L 𝑁) = (𝐴 /L 𝑁)) |
46 | 45 | eqeq2d 2744 |
. . . . . . . . . 10
⊢ (𝑚 = 𝐴 → (ℎ = (𝑚 /L 𝑁) ↔ ℎ = (𝐴 /L 𝑁))) |
47 | 44, 46 | bitr3d 281 |
. . . . . . . . 9
⊢ (𝑚 = 𝐴 → (((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) ↔ ℎ = (𝐴 /L 𝑁))) |
48 | 47 | rspcev 3613 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ℎ = (𝐴 /L 𝑁)) → ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))) |
49 | 48 | ex 414 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ → (ℎ = (𝐴 /L 𝑁) → ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
50 | 49 | adantl 483 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) → (ℎ = (𝐴 /L 𝑁) → ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
51 | 41, 50 | impbid 211 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) →
(∃𝑚 ∈ ℤ
((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) ↔ ℎ = (𝐴 /L 𝑁))) |
52 | 51 | adantr 482 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝐴 /L 𝑁) ∈ V) → (∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) ↔ ℎ = (𝐴 /L 𝑁))) |
53 | 52 | iota5 6524 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝐴 /L 𝑁) ∈ V) → (℩ℎ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))) = (𝐴 /L 𝑁)) |
54 | 18, 53 | mpan2 690 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) →
(℩ℎ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))) = (𝐴 /L 𝑁)) |
55 | 17, 54 | eqtrd 2773 |
1
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) → (𝑋‘(𝐿‘𝐴)) = (𝐴 /L 𝑁)) |