Step | Hyp | Ref
| Expression |
1 | | fiabv.a |
. . . . . 6
⊢ 𝐴 = (AbsVal‘𝑅) |
2 | | fiabv.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
3 | 1, 2 | abvf 20838 |
. . . . 5
⊢ (𝑎 ∈ 𝐴 → 𝑎:𝐵⟶ℝ) |
4 | 3 | ffnd 6748 |
. . . 4
⊢ (𝑎 ∈ 𝐴 → 𝑎 Fn 𝐵) |
5 | 4 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 Fn 𝐵) |
6 | | fiabv.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Domn) |
7 | | fiabv.0 |
. . . . . . . 8
⊢ 0 =
(0g‘𝑅) |
8 | | fiabv.t |
. . . . . . . 8
⊢ 𝑇 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1)) |
9 | 1, 2, 7, 8 | abvtrivg 20856 |
. . . . . . 7
⊢ (𝑅 ∈ Domn → 𝑇 ∈ 𝐴) |
10 | 6, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ 𝐴) |
11 | 1, 2 | abvf 20838 |
. . . . . 6
⊢ (𝑇 ∈ 𝐴 → 𝑇:𝐵⟶ℝ) |
12 | 10, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑇:𝐵⟶ℝ) |
13 | 12 | ffnd 6748 |
. . . 4
⊢ (𝜑 → 𝑇 Fn 𝐵) |
14 | 13 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑇 Fn 𝐵) |
15 | | fveq2 6920 |
. . . . 5
⊢ (𝑏 = 0 → (𝑎‘𝑏) = (𝑎‘ 0 )) |
16 | | fveq2 6920 |
. . . . 5
⊢ (𝑏 = 0 → (𝑇‘𝑏) = (𝑇‘ 0 )) |
17 | 15, 16 | eqeq12d 2756 |
. . . 4
⊢ (𝑏 = 0 → ((𝑎‘𝑏) = (𝑇‘𝑏) ↔ (𝑎‘ 0 ) = (𝑇‘ 0 ))) |
18 | | eqid 2740 |
. . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) |
19 | | eqid 2740 |
. . . . . . 7
⊢
(.g‘(mulGrp‘𝑅)) =
(.g‘(mulGrp‘𝑅)) |
20 | 6 | ad3antrrr 729 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) → 𝑅 ∈ Domn) |
21 | | fiabv.f |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ Fin) |
22 | 21 | ad3antrrr 729 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) → 𝐵 ∈ Fin) |
23 | | eldifsn 4811 |
. . . . . . . . 9
⊢ (𝑏 ∈ (𝐵 ∖ { 0 }) ↔ (𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 )) |
24 | 23 | biimpri 228 |
. . . . . . . 8
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) → 𝑏 ∈ (𝐵 ∖ { 0 })) |
25 | 24 | adantll 713 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) → 𝑏 ∈ (𝐵 ∖ { 0 })) |
26 | 2, 7, 18, 19, 20, 22, 25 | fidomncyc 42490 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) → ∃𝑛 ∈ ℕ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅)) |
27 | | simprr 772 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅)) |
28 | 27 | fveq2d 6924 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → (𝑎‘(𝑛(.g‘(mulGrp‘𝑅))𝑏)) = (𝑎‘(1r‘𝑅))) |
29 | | domnnzr 20728 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
30 | 6, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ NzRing) |
31 | 30 | ad4antr 731 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → 𝑅 ∈ NzRing) |
32 | | simp-4r 783 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → 𝑎 ∈ 𝐴) |
33 | | simpllr 775 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → 𝑏 ∈ 𝐵) |
34 | | simprl 770 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → 𝑛 ∈ ℕ) |
35 | 34 | nnnn0d 12613 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → 𝑛 ∈ ℕ0) |
36 | 1, 19, 2, 31, 32, 33, 35 | abvexp 42487 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → (𝑎‘(𝑛(.g‘(mulGrp‘𝑅))𝑏)) = ((𝑎‘𝑏)↑𝑛)) |
37 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴) |
38 | 18, 7 | nzrnz 20541 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ NzRing →
(1r‘𝑅)
≠ 0
) |
39 | 29, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Domn →
(1r‘𝑅)
≠ 0
) |
40 | 6, 39 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (1r‘𝑅) ≠ 0 ) |
41 | 40 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (1r‘𝑅) ≠ 0 ) |
42 | 1, 18, 7 | abv1z 20847 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ 𝐴 ∧ (1r‘𝑅) ≠ 0 ) → (𝑎‘(1r‘𝑅)) = 1) |
43 | 37, 41, 42 | syl2anc 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎‘(1r‘𝑅)) = 1) |
44 | 43 | ad3antrrr 729 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → (𝑎‘(1r‘𝑅)) = 1) |
45 | 28, 36, 44 | 3eqtr3d 2788 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → ((𝑎‘𝑏)↑𝑛) = 1) |
46 | 1, 2 | abvcl 20839 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑎‘𝑏) ∈ ℝ) |
47 | 32, 33, 46 | syl2anc 583 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → (𝑎‘𝑏) ∈ ℝ) |
48 | 1, 2 | abvge0 20840 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 0 ≤ (𝑎‘𝑏)) |
49 | 32, 33, 48 | syl2anc 583 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → 0 ≤ (𝑎‘𝑏)) |
50 | 47, 34, 49 | expeq1d 42311 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → (((𝑎‘𝑏)↑𝑛) = 1 ↔ (𝑎‘𝑏) = 1)) |
51 | 45, 50 | mpbid 232 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ (𝑛 ∈ ℕ ∧ (𝑛(.g‘(mulGrp‘𝑅))𝑏) = (1r‘𝑅))) → (𝑎‘𝑏) = 1) |
52 | 26, 51 | rexlimddv 3167 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) → (𝑎‘𝑏) = 1) |
53 | | eqeq1 2744 |
. . . . . . . . 9
⊢ (𝑥 = 𝑏 → (𝑥 = 0 ↔ 𝑏 = 0 )) |
54 | 53 | ifbid 4571 |
. . . . . . . 8
⊢ (𝑥 = 𝑏 → if(𝑥 = 0 , 0, 1) = if(𝑏 = 0 , 0, 1)) |
55 | | ifnefalse 4560 |
. . . . . . . . 9
⊢ (𝑏 ≠ 0 → if(𝑏 = 0 , 0, 1) =
1) |
56 | 55 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) → if(𝑏 = 0 , 0, 1) =
1) |
57 | 54, 56 | sylan9eqr 2802 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) ∧ 𝑥 = 𝑏) → if(𝑥 = 0 , 0, 1) =
1) |
58 | | simplr 768 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) → 𝑏 ∈ 𝐵) |
59 | | 1cnd 11285 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) → 1 ∈
ℂ) |
60 | 8, 57, 58, 59 | fvmptd2 7037 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) → (𝑇‘𝑏) = 1) |
61 | 60 | adantllr 718 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) → (𝑇‘𝑏) = 1) |
62 | 52, 61 | eqtr4d 2783 |
. . . 4
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 ≠ 0 ) → (𝑎‘𝑏) = (𝑇‘𝑏)) |
63 | 1, 7 | abv0 20846 |
. . . . . . 7
⊢ (𝑎 ∈ 𝐴 → (𝑎‘ 0 ) = 0) |
64 | 63 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎‘ 0 ) = 0) |
65 | 1, 7 | abv0 20846 |
. . . . . . . 8
⊢ (𝑇 ∈ 𝐴 → (𝑇‘ 0 ) = 0) |
66 | 10, 65 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘ 0 ) = 0) |
67 | 66 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑇‘ 0 ) = 0) |
68 | 64, 67 | eqtr4d 2783 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎‘ 0 ) = (𝑇‘ 0 )) |
69 | 68 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) → (𝑎‘ 0 ) = (𝑇‘ 0 )) |
70 | 17, 62, 69 | pm2.61ne 3033 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) → (𝑎‘𝑏) = (𝑇‘𝑏)) |
71 | 5, 14, 70 | eqfnfvd 7067 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 = 𝑇) |
72 | 71, 10 | eqsnd 4855 |
1
⊢ (𝜑 → 𝐴 = {𝑇}) |