Proof of Theorem lgsdchrval
Step | Hyp | Ref
| Expression |
1 | | nnnn0 11996 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
2 | 1 | adantr 484 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑁 ∈
ℕ0) |
3 | | lgsdchr.z |
. . . . . 6
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
4 | | lgsdchr.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑍) |
5 | | lgsdchr.l |
. . . . . 6
⊢ 𝐿 = (ℤRHom‘𝑍) |
6 | 3, 4, 5 | znzrhfo 20379 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→𝐵) |
7 | | fof 6603 |
. . . . 5
⊢ (𝐿:ℤ–onto→𝐵 → 𝐿:ℤ⟶𝐵) |
8 | 2, 6, 7 | 3syl 18 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝐿:ℤ⟶𝐵) |
9 | 8 | ffvelrnda 6874 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) → (𝐿‘𝐴) ∈ 𝐵) |
10 | | eqeq1 2743 |
. . . . . . 7
⊢ (𝑦 = (𝐿‘𝐴) → (𝑦 = (𝐿‘𝑚) ↔ (𝐿‘𝐴) = (𝐿‘𝑚))) |
11 | 10 | anbi1d 633 |
. . . . . 6
⊢ (𝑦 = (𝐿‘𝐴) → ((𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) ↔ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
12 | 11 | rexbidv 3208 |
. . . . 5
⊢ (𝑦 = (𝐿‘𝐴) → (∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) ↔ ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
13 | 12 | iotabidv 6334 |
. . . 4
⊢ (𝑦 = (𝐿‘𝐴) → (℩ℎ∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))) = (℩ℎ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
14 | | lgsdchr.x |
. . . 4
⊢ 𝑋 = (𝑦 ∈ 𝐵 ↦ (℩ℎ∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
15 | | iotaex 6330 |
. . . 4
⊢
(℩ℎ∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))) ∈ V |
16 | 13, 14, 15 | fvmpt3i 6793 |
. . 3
⊢ ((𝐿‘𝐴) ∈ 𝐵 → (𝑋‘(𝐿‘𝐴)) = (℩ℎ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
17 | 9, 16 | syl 17 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) → (𝑋‘(𝐿‘𝐴)) = (℩ℎ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
18 | | ovex 7216 |
. . 3
⊢ (𝐴 /L 𝑁) ∈ V |
19 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → (𝐿‘𝐴) = (𝐿‘𝑚)) |
20 | | simplll 775 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → 𝑁 ∈ ℕ) |
21 | 20, 1 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → 𝑁 ∈
ℕ0) |
22 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → 𝐴 ∈ ℤ) |
23 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → 𝑚 ∈ ℤ) |
24 | 3, 5 | zndvds 20381 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ
∧ 𝑚 ∈ ℤ)
→ ((𝐿‘𝐴) = (𝐿‘𝑚) ↔ 𝑁 ∥ (𝐴 − 𝑚))) |
25 | 21, 22, 23, 24 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → ((𝐿‘𝐴) = (𝐿‘𝑚) ↔ 𝑁 ∥ (𝐴 − 𝑚))) |
26 | 19, 25 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → 𝑁 ∥ (𝐴 − 𝑚)) |
27 | | moddvds 15723 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝐴 mod 𝑁) = (𝑚 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝑚))) |
28 | 20, 22, 23, 27 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → ((𝐴 mod 𝑁) = (𝑚 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝑚))) |
29 | 26, 28 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → (𝐴 mod 𝑁) = (𝑚 mod 𝑁)) |
30 | 29 | oveq1d 7198 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → ((𝐴 mod 𝑁) /L 𝑁) = ((𝑚 mod 𝑁) /L 𝑁)) |
31 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → ¬ 2 ∥ 𝑁) |
32 | | lgsmod 26072 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑁) = (𝐴 /L 𝑁)) |
33 | 22, 20, 31, 32 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → ((𝐴 mod 𝑁) /L 𝑁) = (𝐴 /L 𝑁)) |
34 | | lgsmod 26072 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → ((𝑚 mod 𝑁) /L 𝑁) = (𝑚 /L 𝑁)) |
35 | 23, 20, 31, 34 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → ((𝑚 mod 𝑁) /L 𝑁) = (𝑚 /L 𝑁)) |
36 | 30, 33, 35 | 3eqtr3d 2782 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → (𝐴 /L 𝑁) = (𝑚 /L 𝑁)) |
37 | 36 | eqeq2d 2750 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → (ℎ = (𝐴 /L 𝑁) ↔ ℎ = (𝑚 /L 𝑁))) |
38 | 37 | biimprd 251 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝐿‘𝐴) = (𝐿‘𝑚))) → (ℎ = (𝑚 /L 𝑁) → ℎ = (𝐴 /L 𝑁))) |
39 | 38 | anassrs 471 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ ¬ 2 ∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ 𝑚 ∈ ℤ) ∧ (𝐿‘𝐴) = (𝐿‘𝑚)) → (ℎ = (𝑚 /L 𝑁) → ℎ = (𝐴 /L 𝑁))) |
40 | 39 | expimpd 457 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → (((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) → ℎ = (𝐴 /L 𝑁))) |
41 | 40 | rexlimdva 3195 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) →
(∃𝑚 ∈ ℤ
((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) → ℎ = (𝐴 /L 𝑁))) |
42 | | fveq2 6687 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝐴 → (𝐿‘𝑚) = (𝐿‘𝐴)) |
43 | 42 | eqcomd 2745 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝐴 → (𝐿‘𝐴) = (𝐿‘𝑚)) |
44 | 43 | biantrurd 536 |
. . . . . . . . . 10
⊢ (𝑚 = 𝐴 → (ℎ = (𝑚 /L 𝑁) ↔ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
45 | | oveq1 7190 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝐴 → (𝑚 /L 𝑁) = (𝐴 /L 𝑁)) |
46 | 45 | eqeq2d 2750 |
. . . . . . . . . 10
⊢ (𝑚 = 𝐴 → (ℎ = (𝑚 /L 𝑁) ↔ ℎ = (𝐴 /L 𝑁))) |
47 | 44, 46 | bitr3d 284 |
. . . . . . . . 9
⊢ (𝑚 = 𝐴 → (((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) ↔ ℎ = (𝐴 /L 𝑁))) |
48 | 47 | rspcev 3529 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ ℎ = (𝐴 /L 𝑁)) → ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))) |
49 | 48 | ex 416 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ → (ℎ = (𝐴 /L 𝑁) → ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
50 | 49 | adantl 485 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) → (ℎ = (𝐴 /L 𝑁) → ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
51 | 41, 50 | impbid 215 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) →
(∃𝑚 ∈ ℤ
((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) ↔ ℎ = (𝐴 /L 𝑁))) |
52 | 51 | adantr 484 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝐴 /L 𝑁) ∈ V) → (∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)) ↔ ℎ = (𝐴 /L 𝑁))) |
53 | 52 | iota5 6333 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) ∧ (𝐴 /L 𝑁) ∈ V) → (℩ℎ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))) = (𝐴 /L 𝑁)) |
54 | 18, 53 | mpan2 691 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) →
(℩ℎ∃𝑚 ∈ ℤ ((𝐿‘𝐴) = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))) = (𝐴 /L 𝑁)) |
55 | 17, 54 | eqtrd 2774 |
1
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝐴 ∈ ℤ) → (𝑋‘(𝐿‘𝐴)) = (𝐴 /L 𝑁)) |