Step | Hyp | Ref
| Expression |
1 | | grplmulf1o.n |
. 2
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑋 + 𝑥)) |
2 | | grplmulf1o.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
3 | | grplmulf1o.p |
. . . 4
⊢ + =
(+g‘𝐺) |
4 | 2, 3 | grpcl 17430 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑋 + 𝑥) ∈ 𝐵) |
5 | 4 | 3expa 1265 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑋 + 𝑥) ∈ 𝐵) |
6 | | simpl 473 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → 𝐺 ∈ Grp) |
7 | | eqid 2622 |
. . . . 5
⊢
(invg‘𝐺) = (invg‘𝐺) |
8 | 2, 7 | grpinvcl 17467 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((invg‘𝐺)‘𝑋) ∈ 𝐵) |
9 | 6, 8 | jca 554 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝐺 ∈ Grp ∧
((invg‘𝐺)‘𝑋) ∈ 𝐵)) |
10 | 2, 3 | grpcl 17430 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧
((invg‘𝐺)‘𝑋) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (((invg‘𝐺)‘𝑋) + 𝑦) ∈ 𝐵) |
11 | 10 | 3expa 1265 |
. . 3
⊢ (((𝐺 ∈ Grp ∧
((invg‘𝐺)‘𝑋) ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (((invg‘𝐺)‘𝑋) + 𝑦) ∈ 𝐵) |
12 | 9, 11 | sylan 488 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (((invg‘𝐺)‘𝑋) + 𝑦) ∈ 𝐵) |
13 | | eqcom 2629 |
. . 3
⊢ (𝑥 =
(((invg‘𝐺)‘𝑋) + 𝑦) ↔ (((invg‘𝐺)‘𝑋) + 𝑦) = 𝑥) |
14 | 6 | adantr 481 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺 ∈ Grp) |
15 | 12 | adantrl 752 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((invg‘𝐺)‘𝑋) + 𝑦) ∈ 𝐵) |
16 | | simprl 794 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
17 | | simplr 792 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
18 | 2, 3 | grplcan 17477 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧
((((invg‘𝐺)‘𝑋) + 𝑦) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → ((𝑋 +
(((invg‘𝐺)‘𝑋) + 𝑦)) = (𝑋 + 𝑥) ↔ (((invg‘𝐺)‘𝑋) + 𝑦) = 𝑥)) |
19 | 14, 15, 16, 17, 18 | syl13anc 1328 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑋 +
(((invg‘𝐺)‘𝑋) + 𝑦)) = (𝑋 + 𝑥) ↔ (((invg‘𝐺)‘𝑋) + 𝑦) = 𝑥)) |
20 | | eqid 2622 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
21 | 2, 3, 20, 7 | grprinv 17469 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 +
((invg‘𝐺)‘𝑋)) = (0g‘𝐺)) |
22 | 21 | adantr 481 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑋 +
((invg‘𝐺)‘𝑋)) = (0g‘𝐺)) |
23 | 22 | oveq1d 6665 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑋 +
((invg‘𝐺)‘𝑋)) + 𝑦) = ((0g‘𝐺) + 𝑦)) |
24 | 8 | adantr 481 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((invg‘𝐺)‘𝑋) ∈ 𝐵) |
25 | | simprr 796 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
26 | 2, 3 | grpass 17431 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑋) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑋 +
((invg‘𝐺)‘𝑋)) + 𝑦) = (𝑋 +
(((invg‘𝐺)‘𝑋) + 𝑦))) |
27 | 14, 17, 24, 25, 26 | syl13anc 1328 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑋 +
((invg‘𝐺)‘𝑋)) + 𝑦) = (𝑋 +
(((invg‘𝐺)‘𝑋) + 𝑦))) |
28 | 2, 3, 20 | grplid 17452 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵) → ((0g‘𝐺) + 𝑦) = 𝑦) |
29 | 28 | ad2ant2rl 785 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((0g‘𝐺) + 𝑦) = 𝑦) |
30 | 23, 27, 29 | 3eqtr3d 2664 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑋 +
(((invg‘𝐺)‘𝑋) + 𝑦)) = 𝑦) |
31 | 30 | eqeq1d 2624 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑋 +
(((invg‘𝐺)‘𝑋) + 𝑦)) = (𝑋 + 𝑥) ↔ 𝑦 = (𝑋 + 𝑥))) |
32 | 19, 31 | bitr3d 270 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((((invg‘𝐺)‘𝑋) + 𝑦) = 𝑥 ↔ 𝑦 = (𝑋 + 𝑥))) |
33 | 13, 32 | syl5bb 272 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = (((invg‘𝐺)‘𝑋) + 𝑦) ↔ 𝑦 = (𝑋 + 𝑥))) |
34 | 1, 5, 12, 33 | f1o2d 6887 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → 𝐹:𝐵–1-1-onto→𝐵) |