| Step | Hyp | Ref
| Expression |
| 1 | | grpinv.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) |
| 2 | | grpinv.p |
. . . . . . . . . 10
⊢ + =
(+g‘𝐺) |
| 3 | | grpinv.u |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝐺) |
| 4 | | grpinv.n |
. . . . . . . . . 10
⊢ 𝑁 = (invg‘𝐺) |
| 5 | 1, 2, 3, 4 | grpinvval 18998 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (𝑁‘𝑥) = (℩𝑒 ∈ 𝐵 (𝑒 + 𝑥) = 0 )) |
| 6 | 5 | ad2antlr 727 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑀:𝐵⟶𝐵) ∧ 𝑥 ∈ 𝐵) ∧ ((𝑀‘𝑥) + 𝑥) = 0 ) → (𝑁‘𝑥) = (℩𝑒 ∈ 𝐵 (𝑒 + 𝑥) = 0 )) |
| 7 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑀:𝐵⟶𝐵) ∧ 𝑥 ∈ 𝐵) ∧ ((𝑀‘𝑥) + 𝑥) = 0 ) → ((𝑀‘𝑥) + 𝑥) = 0 ) |
| 8 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑀:𝐵⟶𝐵) ∧ 𝑥 ∈ 𝐵) ∧ ((𝑀‘𝑥) + 𝑥) = 0 ) → 𝑀:𝐵⟶𝐵) |
| 9 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑀:𝐵⟶𝐵) ∧ 𝑥 ∈ 𝐵) ∧ ((𝑀‘𝑥) + 𝑥) = 0 ) → 𝑥 ∈ 𝐵) |
| 10 | 8, 9 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑀:𝐵⟶𝐵) ∧ 𝑥 ∈ 𝐵) ∧ ((𝑀‘𝑥) + 𝑥) = 0 ) → (𝑀‘𝑥) ∈ 𝐵) |
| 11 | 1, 2, 3 | grpinveu 18992 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵) → ∃!𝑒 ∈ 𝐵 (𝑒 + 𝑥) = 0 ) |
| 12 | 11 | ad4ant13 751 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑀:𝐵⟶𝐵) ∧ 𝑥 ∈ 𝐵) ∧ ((𝑀‘𝑥) + 𝑥) = 0 ) → ∃!𝑒 ∈ 𝐵 (𝑒 + 𝑥) = 0 ) |
| 13 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑒 = (𝑀‘𝑥) → (𝑒 + 𝑥) = ((𝑀‘𝑥) + 𝑥)) |
| 14 | 13 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑒 = (𝑀‘𝑥) → ((𝑒 + 𝑥) = 0 ↔ ((𝑀‘𝑥) + 𝑥) = 0 )) |
| 15 | 14 | riota2 7413 |
. . . . . . . . . 10
⊢ (((𝑀‘𝑥) ∈ 𝐵 ∧ ∃!𝑒 ∈ 𝐵 (𝑒 + 𝑥) = 0 ) → (((𝑀‘𝑥) + 𝑥) = 0 ↔
(℩𝑒 ∈
𝐵 (𝑒 + 𝑥) = 0 ) = (𝑀‘𝑥))) |
| 16 | 10, 12, 15 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑀:𝐵⟶𝐵) ∧ 𝑥 ∈ 𝐵) ∧ ((𝑀‘𝑥) + 𝑥) = 0 ) → (((𝑀‘𝑥) + 𝑥) = 0 ↔
(℩𝑒 ∈
𝐵 (𝑒 + 𝑥) = 0 ) = (𝑀‘𝑥))) |
| 17 | 7, 16 | mpbid 232 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑀:𝐵⟶𝐵) ∧ 𝑥 ∈ 𝐵) ∧ ((𝑀‘𝑥) + 𝑥) = 0 ) →
(℩𝑒 ∈
𝐵 (𝑒 + 𝑥) = 0 ) = (𝑀‘𝑥)) |
| 18 | 6, 17 | eqtrd 2777 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑀:𝐵⟶𝐵) ∧ 𝑥 ∈ 𝐵) ∧ ((𝑀‘𝑥) + 𝑥) = 0 ) → (𝑁‘𝑥) = (𝑀‘𝑥)) |
| 19 | 18 | ex 412 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑀:𝐵⟶𝐵) ∧ 𝑥 ∈ 𝐵) → (((𝑀‘𝑥) + 𝑥) = 0 → (𝑁‘𝑥) = (𝑀‘𝑥))) |
| 20 | 19 | ralimdva 3167 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑀:𝐵⟶𝐵) → (∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 → ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) = (𝑀‘𝑥))) |
| 21 | 20 | impr 454 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑀:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 )) → ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) = (𝑀‘𝑥)) |
| 22 | 1, 4 | grpinvfn 18999 |
. . . . 5
⊢ 𝑁 Fn 𝐵 |
| 23 | | ffn 6736 |
. . . . . 6
⊢ (𝑀:𝐵⟶𝐵 → 𝑀 Fn 𝐵) |
| 24 | 23 | ad2antrl 728 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑀:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 )) → 𝑀 Fn 𝐵) |
| 25 | | eqfnfv 7051 |
. . . . 5
⊢ ((𝑁 Fn 𝐵 ∧ 𝑀 Fn 𝐵) → (𝑁 = 𝑀 ↔ ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) = (𝑀‘𝑥))) |
| 26 | 22, 24, 25 | sylancr 587 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑀:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 )) → (𝑁 = 𝑀 ↔ ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) = (𝑀‘𝑥))) |
| 27 | 21, 26 | mpbird 257 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑀:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 )) → 𝑁 = 𝑀) |
| 28 | 27 | ex 412 |
. 2
⊢ (𝐺 ∈ Grp → ((𝑀:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 ) → 𝑁 = 𝑀)) |
| 29 | 1, 4 | grpinvf 19004 |
. . . 4
⊢ (𝐺 ∈ Grp → 𝑁:𝐵⟶𝐵) |
| 30 | 1, 2, 3, 4 | grplinv 19007 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵) → ((𝑁‘𝑥) + 𝑥) = 0 ) |
| 31 | 30 | ralrimiva 3146 |
. . . 4
⊢ (𝐺 ∈ Grp → ∀𝑥 ∈ 𝐵 ((𝑁‘𝑥) + 𝑥) = 0 ) |
| 32 | 29, 31 | jca 511 |
. . 3
⊢ (𝐺 ∈ Grp → (𝑁:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑁‘𝑥) + 𝑥) = 0 )) |
| 33 | | feq1 6716 |
. . . 4
⊢ (𝑁 = 𝑀 → (𝑁:𝐵⟶𝐵 ↔ 𝑀:𝐵⟶𝐵)) |
| 34 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑁 = 𝑀 → (𝑁‘𝑥) = (𝑀‘𝑥)) |
| 35 | 34 | oveq1d 7446 |
. . . . . 6
⊢ (𝑁 = 𝑀 → ((𝑁‘𝑥) + 𝑥) = ((𝑀‘𝑥) + 𝑥)) |
| 36 | 35 | eqeq1d 2739 |
. . . . 5
⊢ (𝑁 = 𝑀 → (((𝑁‘𝑥) + 𝑥) = 0 ↔ ((𝑀‘𝑥) + 𝑥) = 0 )) |
| 37 | 36 | ralbidv 3178 |
. . . 4
⊢ (𝑁 = 𝑀 → (∀𝑥 ∈ 𝐵 ((𝑁‘𝑥) + 𝑥) = 0 ↔ ∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 )) |
| 38 | 33, 37 | anbi12d 632 |
. . 3
⊢ (𝑁 = 𝑀 → ((𝑁:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑁‘𝑥) + 𝑥) = 0 ) ↔ (𝑀:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 ))) |
| 39 | 32, 38 | syl5ibcom 245 |
. 2
⊢ (𝐺 ∈ Grp → (𝑁 = 𝑀 → (𝑀:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 ))) |
| 40 | 28, 39 | impbid 212 |
1
⊢ (𝐺 ∈ Grp → ((𝑀:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 ) ↔ 𝑁 = 𝑀)) |