| Step | Hyp | Ref
| Expression |
| 1 | | cycpm3.c |
. . . . 5
⊢ 𝐶 = (toCyc‘𝐷) |
| 2 | | cycpm3.s |
. . . . 5
⊢ 𝑆 = (SymGrp‘𝐷) |
| 3 | | cycpm3.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
| 4 | | cycpm3.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝐷) |
| 5 | | cycpm3.j |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ 𝐷) |
| 6 | | cycpm3.k |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ 𝐷) |
| 7 | | cycpm3.1 |
. . . . 5
⊢ (𝜑 → 𝐼 ≠ 𝐽) |
| 8 | | cycpm3.2 |
. . . . 5
⊢ (𝜑 → 𝐽 ≠ 𝐾) |
| 9 | | cycpm3.3 |
. . . . 5
⊢ (𝜑 → 𝐾 ≠ 𝐼) |
| 10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | cycpm3cl 33155 |
. . . 4
⊢ (𝜑 → (𝐶‘〈“𝐼𝐽𝐾”〉) ∈ (Base‘𝑆)) |
| 11 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 12 | 2, 11 | symgbasf 19393 |
. . . 4
⊢ ((𝐶‘〈“𝐼𝐽𝐾”〉) ∈ (Base‘𝑆) → (𝐶‘〈“𝐼𝐽𝐾”〉):𝐷⟶𝐷) |
| 13 | 10, 12 | syl 17 |
. . 3
⊢ (𝜑 → (𝐶‘〈“𝐼𝐽𝐾”〉):𝐷⟶𝐷) |
| 14 | 13 | ffnd 6737 |
. 2
⊢ (𝜑 → (𝐶‘〈“𝐼𝐽𝐾”〉) Fn 𝐷) |
| 15 | 2 | symggrp 19418 |
. . . . . 6
⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Grp) |
| 16 | 3, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ Grp) |
| 17 | 9 | necomd 2996 |
. . . . . 6
⊢ (𝜑 → 𝐼 ≠ 𝐾) |
| 18 | 1, 3, 4, 6, 17, 2 | cycpm2cl 33140 |
. . . . 5
⊢ (𝜑 → (𝐶‘〈“𝐼𝐾”〉) ∈ (Base‘𝑆)) |
| 19 | 1, 3, 4, 5, 7, 2 | cycpm2cl 33140 |
. . . . 5
⊢ (𝜑 → (𝐶‘〈“𝐼𝐽”〉) ∈ (Base‘𝑆)) |
| 20 | | cyc3co2.t |
. . . . . 6
⊢ · =
(+g‘𝑆) |
| 21 | 11, 20 | grpcl 18959 |
. . . . 5
⊢ ((𝑆 ∈ Grp ∧ (𝐶‘〈“𝐼𝐾”〉) ∈ (Base‘𝑆) ∧ (𝐶‘〈“𝐼𝐽”〉) ∈ (Base‘𝑆)) → ((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉)) ∈ (Base‘𝑆)) |
| 22 | 16, 18, 19, 21 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉)) ∈ (Base‘𝑆)) |
| 23 | 2, 11 | symgbasf 19393 |
. . . 4
⊢ (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉)) ∈ (Base‘𝑆) → ((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉)):𝐷⟶𝐷) |
| 24 | 22, 23 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉)):𝐷⟶𝐷) |
| 25 | 24 | ffnd 6737 |
. 2
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉)) Fn 𝐷) |
| 26 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | cyc3fv1 33157 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝐼) = 𝐽) |
| 27 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝐼) = 𝐽) |
| 28 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → 𝑥 = 𝐼) |
| 29 | 28 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝐼)) |
| 30 | 2, 11, 20 | symgov 19401 |
. . . . . . . . . . 11
⊢ (((𝐶‘〈“𝐼𝐾”〉) ∈ (Base‘𝑆) ∧ (𝐶‘〈“𝐼𝐽”〉) ∈ (Base‘𝑆)) → ((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉)) = ((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))) |
| 31 | 18, 19, 30 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉)) = ((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))) |
| 32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → ((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉)) = ((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))) |
| 33 | 32 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 34 | 2, 11 | symgbasf 19393 |
. . . . . . . . . . . 12
⊢ ((𝐶‘〈“𝐼𝐽”〉) ∈ (Base‘𝑆) → (𝐶‘〈“𝐼𝐽”〉):𝐷⟶𝐷) |
| 35 | 19, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶‘〈“𝐼𝐽”〉):𝐷⟶𝐷) |
| 36 | 35 | ffund 6740 |
. . . . . . . . . 10
⊢ (𝜑 → Fun (𝐶‘〈“𝐼𝐽”〉)) |
| 37 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → 𝐼 ∈ 𝐷) |
| 38 | 34 | fdmd 6746 |
. . . . . . . . . . . . 13
⊢ ((𝐶‘〈“𝐼𝐽”〉) ∈ (Base‘𝑆) → dom (𝐶‘〈“𝐼𝐽”〉) = 𝐷) |
| 39 | 19, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (𝐶‘〈“𝐼𝐽”〉) = 𝐷) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → dom (𝐶‘〈“𝐼𝐽”〉) = 𝐷) |
| 41 | 37, 28, 40 | 3eltr4d 2856 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → 𝑥 ∈ dom (𝐶‘〈“𝐼𝐽”〉)) |
| 42 | | fvco 7007 |
. . . . . . . . . 10
⊢ ((Fun
(𝐶‘〈“𝐼𝐽”〉) ∧ 𝑥 ∈ dom (𝐶‘〈“𝐼𝐽”〉)) → (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = ((𝐶‘〈“𝐼𝐾”〉)‘((𝐶‘〈“𝐼𝐽”〉)‘𝑥))) |
| 43 | 36, 41, 42 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = ((𝐶‘〈“𝐼𝐾”〉)‘((𝐶‘〈“𝐼𝐽”〉)‘𝑥))) |
| 44 | 28 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → ((𝐶‘〈“𝐼𝐽”〉)‘𝑥) = ((𝐶‘〈“𝐼𝐽”〉)‘𝐼)) |
| 45 | 1, 3, 4, 5, 7, 2 | cyc2fv1 33141 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐽”〉)‘𝐼) = 𝐽) |
| 46 | 45 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → ((𝐶‘〈“𝐼𝐽”〉)‘𝐼) = 𝐽) |
| 47 | 44, 46 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → ((𝐶‘〈“𝐼𝐽”〉)‘𝑥) = 𝐽) |
| 48 | 47 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → ((𝐶‘〈“𝐼𝐾”〉)‘((𝐶‘〈“𝐼𝐽”〉)‘𝑥)) = ((𝐶‘〈“𝐼𝐾”〉)‘𝐽)) |
| 49 | 8 | necomd 2996 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ≠ 𝐽) |
| 50 | 7 | necomd 2996 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ≠ 𝐼) |
| 51 | 1, 2, 3, 4, 6, 5, 17, 49, 50 | cyc2fvx 33154 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐾”〉)‘𝐽) = 𝐽) |
| 52 | 51 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → ((𝐶‘〈“𝐼𝐾”〉)‘𝐽) = 𝐽) |
| 53 | 43, 48, 52 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = 𝐽) |
| 54 | 33, 53 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = 𝐽) |
| 55 | 27, 29, 54 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝐼) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 56 | 55 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ {𝐼, 𝐽, 𝐾}) ∧ 𝑥 = 𝐼) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 57 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | cyc3fv2 33158 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝐽) = 𝐾) |
| 58 | 57 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝐽) = 𝐾) |
| 59 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → 𝑥 = 𝐽) |
| 60 | 59 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝐽)) |
| 61 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → ((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉)) = ((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))) |
| 62 | 61 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 63 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → 𝐽 ∈ 𝐷) |
| 64 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → dom (𝐶‘〈“𝐼𝐽”〉) = 𝐷) |
| 65 | 63, 59, 64 | 3eltr4d 2856 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → 𝑥 ∈ dom (𝐶‘〈“𝐼𝐽”〉)) |
| 66 | 36, 65, 42 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = ((𝐶‘〈“𝐼𝐾”〉)‘((𝐶‘〈“𝐼𝐽”〉)‘𝑥))) |
| 67 | 59 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → ((𝐶‘〈“𝐼𝐽”〉)‘𝑥) = ((𝐶‘〈“𝐼𝐽”〉)‘𝐽)) |
| 68 | 1, 3, 4, 5, 7, 2 | cyc2fv2 33142 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐽”〉)‘𝐽) = 𝐼) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → ((𝐶‘〈“𝐼𝐽”〉)‘𝐽) = 𝐼) |
| 70 | 67, 69 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → ((𝐶‘〈“𝐼𝐽”〉)‘𝑥) = 𝐼) |
| 71 | 70 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → ((𝐶‘〈“𝐼𝐾”〉)‘((𝐶‘〈“𝐼𝐽”〉)‘𝑥)) = ((𝐶‘〈“𝐼𝐾”〉)‘𝐼)) |
| 72 | 1, 3, 4, 6, 17, 2 | cyc2fv1 33141 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐾”〉)‘𝐼) = 𝐾) |
| 73 | 72 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → ((𝐶‘〈“𝐼𝐾”〉)‘𝐼) = 𝐾) |
| 74 | 66, 71, 73 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = 𝐾) |
| 75 | 62, 74 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = 𝐾) |
| 76 | 58, 60, 75 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝐽) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 77 | 76 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ {𝐼, 𝐽, 𝐾}) ∧ 𝑥 = 𝐽) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 78 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | cyc3fv3 33159 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝐾) = 𝐼) |
| 79 | 78 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝐾) = 𝐼) |
| 80 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → 𝑥 = 𝐾) |
| 81 | 80 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝐾)) |
| 82 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → ((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉)) = ((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))) |
| 83 | 82 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 84 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → 𝐾 ∈ 𝐷) |
| 85 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → dom (𝐶‘〈“𝐼𝐽”〉) = 𝐷) |
| 86 | 84, 80, 85 | 3eltr4d 2856 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → 𝑥 ∈ dom (𝐶‘〈“𝐼𝐽”〉)) |
| 87 | 36, 86, 42 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = ((𝐶‘〈“𝐼𝐾”〉)‘((𝐶‘〈“𝐼𝐽”〉)‘𝑥))) |
| 88 | 80 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → ((𝐶‘〈“𝐼𝐽”〉)‘𝑥) = ((𝐶‘〈“𝐼𝐽”〉)‘𝐾)) |
| 89 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | cyc2fvx 33154 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐽”〉)‘𝐾) = 𝐾) |
| 90 | 89 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → ((𝐶‘〈“𝐼𝐽”〉)‘𝐾) = 𝐾) |
| 91 | 88, 90 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → ((𝐶‘〈“𝐼𝐽”〉)‘𝑥) = 𝐾) |
| 92 | 91 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → ((𝐶‘〈“𝐼𝐾”〉)‘((𝐶‘〈“𝐼𝐽”〉)‘𝑥)) = ((𝐶‘〈“𝐼𝐾”〉)‘𝐾)) |
| 93 | 1, 3, 4, 6, 17, 2 | cyc2fv2 33142 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶‘〈“𝐼𝐾”〉)‘𝐾) = 𝐼) |
| 94 | 93 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → ((𝐶‘〈“𝐼𝐾”〉)‘𝐾) = 𝐼) |
| 95 | 87, 92, 94 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = 𝐼) |
| 96 | 83, 95 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = 𝐼) |
| 97 | 79, 81, 96 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝐾) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 98 | 97 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ {𝐼, 𝐽, 𝐾}) ∧ 𝑥 = 𝐾) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 99 | | eltpi 4688 |
. . . . . 6
⊢ (𝑥 ∈ {𝐼, 𝐽, 𝐾} → (𝑥 = 𝐼 ∨ 𝑥 = 𝐽 ∨ 𝑥 = 𝐾)) |
| 100 | 99 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ {𝐼, 𝐽, 𝐾}) → (𝑥 = 𝐼 ∨ 𝑥 = 𝐽 ∨ 𝑥 = 𝐾)) |
| 101 | 56, 77, 98, 100 | mpjao3dan 1434 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ {𝐼, 𝐽, 𝐾}) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 102 | 101 | adantlr 715 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ {𝐼, 𝐽, 𝐾}) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 103 | 35 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → (𝐶‘〈“𝐼𝐽”〉):𝐷⟶𝐷) |
| 104 | 103 | ffund 6740 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → Fun (𝐶‘〈“𝐼𝐽”〉)) |
| 105 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) |
| 106 | 105 | eldifad 3963 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → 𝑥 ∈ 𝐷) |
| 107 | 39 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → dom (𝐶‘〈“𝐼𝐽”〉) = 𝐷) |
| 108 | 106, 107 | eleqtrrd 2844 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → 𝑥 ∈ dom (𝐶‘〈“𝐼𝐽”〉)) |
| 109 | 104, 108,
42 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = ((𝐶‘〈“𝐼𝐾”〉)‘((𝐶‘〈“𝐼𝐽”〉)‘𝑥))) |
| 110 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → 𝐷 ∈ 𝑉) |
| 111 | 4, 5 | s2cld 14910 |
. . . . . . . . 9
⊢ (𝜑 → 〈“𝐼𝐽”〉 ∈ Word 𝐷) |
| 112 | 111 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → 〈“𝐼𝐽”〉 ∈ Word 𝐷) |
| 113 | 4, 5, 7 | s2f1 32929 |
. . . . . . . . 9
⊢ (𝜑 → 〈“𝐼𝐽”〉:dom 〈“𝐼𝐽”〉–1-1→𝐷) |
| 114 | 113 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → 〈“𝐼𝐽”〉:dom 〈“𝐼𝐽”〉–1-1→𝐷) |
| 115 | | tpid1g 4769 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∈ 𝐷 → 𝐼 ∈ {𝐼, 𝐽, 𝐾}) |
| 116 | 4, 115 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ {𝐼, 𝐽, 𝐾}) |
| 117 | | tpid2g 4771 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ 𝐷 → 𝐽 ∈ {𝐼, 𝐽, 𝐾}) |
| 118 | 5, 117 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ {𝐼, 𝐽, 𝐾}) |
| 119 | 116, 118 | prssd 4822 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐼, 𝐽} ⊆ {𝐼, 𝐽, 𝐾}) |
| 120 | 4, 5 | s2rn 15002 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 〈“𝐼𝐽”〉 = {𝐼, 𝐽}) |
| 121 | 120 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐼, 𝐽} = ran 〈“𝐼𝐽”〉) |
| 122 | 4, 5, 6 | s3rn 15003 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 〈“𝐼𝐽𝐾”〉 = {𝐼, 𝐽, 𝐾}) |
| 123 | 122 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐼, 𝐽, 𝐾} = ran 〈“𝐼𝐽𝐾”〉) |
| 124 | 119, 121,
123 | 3sstr3d 4038 |
. . . . . . . . . 10
⊢ (𝜑 → ran 〈“𝐼𝐽”〉 ⊆ ran 〈“𝐼𝐽𝐾”〉) |
| 125 | 124 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ran 〈“𝐼𝐽”〉 ⊆ ran 〈“𝐼𝐽𝐾”〉) |
| 126 | 105 | eldifbd 3964 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ¬ 𝑥 ∈ {𝐼, 𝐽, 𝐾}) |
| 127 | 122 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ran 〈“𝐼𝐽𝐾”〉 = {𝐼, 𝐽, 𝐾}) |
| 128 | 126, 127 | neleqtrrd 2864 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ¬ 𝑥 ∈ ran 〈“𝐼𝐽𝐾”〉) |
| 129 | 125, 128 | ssneldd 3986 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ¬ 𝑥 ∈ ran 〈“𝐼𝐽”〉) |
| 130 | 1, 110, 112, 114, 106, 129 | cycpmfv3 33135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ((𝐶‘〈“𝐼𝐽”〉)‘𝑥) = 𝑥) |
| 131 | 130 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ((𝐶‘〈“𝐼𝐾”〉)‘((𝐶‘〈“𝐼𝐽”〉)‘𝑥)) = ((𝐶‘〈“𝐼𝐾”〉)‘𝑥)) |
| 132 | 4, 6 | s2cld 14910 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝐼𝐾”〉 ∈ Word 𝐷) |
| 133 | 132 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → 〈“𝐼𝐾”〉 ∈ Word 𝐷) |
| 134 | 4, 6, 17 | s2f1 32929 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝐼𝐾”〉:dom 〈“𝐼𝐾”〉–1-1→𝐷) |
| 135 | 134 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → 〈“𝐼𝐾”〉:dom 〈“𝐼𝐾”〉–1-1→𝐷) |
| 136 | | tpid3g 4772 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ 𝐷 → 𝐾 ∈ {𝐼, 𝐽, 𝐾}) |
| 137 | 6, 136 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ {𝐼, 𝐽, 𝐾}) |
| 138 | 116, 137 | prssd 4822 |
. . . . . . . . . 10
⊢ (𝜑 → {𝐼, 𝐾} ⊆ {𝐼, 𝐽, 𝐾}) |
| 139 | 138 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → {𝐼, 𝐾} ⊆ {𝐼, 𝐽, 𝐾}) |
| 140 | 4, 6 | s2rn 15002 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 〈“𝐼𝐾”〉 = {𝐼, 𝐾}) |
| 141 | 140 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝜑 → {𝐼, 𝐾} = ran 〈“𝐼𝐾”〉) |
| 142 | 141 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → {𝐼, 𝐾} = ran 〈“𝐼𝐾”〉) |
| 143 | 123 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → {𝐼, 𝐽, 𝐾} = ran 〈“𝐼𝐽𝐾”〉) |
| 144 | 139, 142,
143 | 3sstr3d 4038 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ran 〈“𝐼𝐾”〉 ⊆ ran 〈“𝐼𝐽𝐾”〉) |
| 145 | 144, 128 | ssneldd 3986 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ¬ 𝑥 ∈ ran 〈“𝐼𝐾”〉) |
| 146 | 1, 110, 133, 135, 106, 145 | cycpmfv3 33135 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ((𝐶‘〈“𝐼𝐾”〉)‘𝑥) = 𝑥) |
| 147 | 109, 131,
146 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = 𝑥) |
| 148 | 31 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉)) = ((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))) |
| 149 | 148 | fveq1d 6908 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) ∘ (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 150 | 4, 5, 6 | s3cld 14911 |
. . . . . . 7
⊢ (𝜑 → 〈“𝐼𝐽𝐾”〉 ∈ Word 𝐷) |
| 151 | 150 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → 〈“𝐼𝐽𝐾”〉 ∈ Word 𝐷) |
| 152 | 4, 5, 6, 7, 8, 9 | s3f1 32931 |
. . . . . . 7
⊢ (𝜑 → 〈“𝐼𝐽𝐾”〉:dom 〈“𝐼𝐽𝐾”〉–1-1→𝐷) |
| 153 | 152 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → 〈“𝐼𝐽𝐾”〉:dom 〈“𝐼𝐽𝐾”〉–1-1→𝐷) |
| 154 | 1, 110, 151, 153, 106, 128 | cycpmfv3 33135 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = 𝑥) |
| 155 | 147, 149,
154 | 3eqtr4rd 2788 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 156 | 155 | adantlr 715 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 157 | | tpssi 4838 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐾 ∈ 𝐷) → {𝐼, 𝐽, 𝐾} ⊆ 𝐷) |
| 158 | 4, 5, 6, 157 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → {𝐼, 𝐽, 𝐾} ⊆ 𝐷) |
| 159 | | undif 4482 |
. . . . . . 7
⊢ ({𝐼, 𝐽, 𝐾} ⊆ 𝐷 ↔ ({𝐼, 𝐽, 𝐾} ∪ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) = 𝐷) |
| 160 | 158, 159 | sylib 218 |
. . . . . 6
⊢ (𝜑 → ({𝐼, 𝐽, 𝐾} ∪ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) = 𝐷) |
| 161 | 160 | eleq2d 2827 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ({𝐼, 𝐽, 𝐾} ∪ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) ↔ 𝑥 ∈ 𝐷)) |
| 162 | 161 | biimpar 477 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ({𝐼, 𝐽, 𝐾} ∪ (𝐷 ∖ {𝐼, 𝐽, 𝐾}))) |
| 163 | | elun 4153 |
. . . 4
⊢ (𝑥 ∈ ({𝐼, 𝐽, 𝐾} ∪ (𝐷 ∖ {𝐼, 𝐽, 𝐾})) ↔ (𝑥 ∈ {𝐼, 𝐽, 𝐾} ∨ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾}))) |
| 164 | 162, 163 | sylib 218 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ {𝐼, 𝐽, 𝐾} ∨ 𝑥 ∈ (𝐷 ∖ {𝐼, 𝐽, 𝐾}))) |
| 165 | 102, 156,
164 | mpjaodan 961 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((𝐶‘〈“𝐼𝐽𝐾”〉)‘𝑥) = (((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))‘𝑥)) |
| 166 | 14, 25, 165 | eqfnfvd 7054 |
1
⊢ (𝜑 → (𝐶‘〈“𝐼𝐽𝐾”〉) = ((𝐶‘〈“𝐼𝐾”〉) · (𝐶‘〈“𝐼𝐽”〉))) |