Step | Hyp | Ref
| Expression |
1 | | subgrcl 18760 |
. . . . . . . . . 10
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
2 | 1 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → 𝐺 ∈ Grp) |
3 | | conjnmz.1 |
. . . . . . . . . . . 12
⊢ 𝑁 = {𝑦 ∈ 𝑋 ∣ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)} |
4 | 3 | ssrab3 4015 |
. . . . . . . . . . 11
⊢ 𝑁 ⊆ 𝑋 |
5 | | simplr 766 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → 𝐴 ∈ 𝑁) |
6 | 4, 5 | sselid 3919 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → 𝐴 ∈ 𝑋) |
7 | | conjghm.x |
. . . . . . . . . . 11
⊢ 𝑋 = (Base‘𝐺) |
8 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(invg‘𝐺) = (invg‘𝐺) |
9 | 7, 8 | grpinvcl 18627 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ((invg‘𝐺)‘𝐴) ∈ 𝑋) |
10 | 2, 6, 9 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((invg‘𝐺)‘𝐴) ∈ 𝑋) |
11 | 7 | subgss 18756 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑋) |
12 | 11 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝑆 ⊆ 𝑋) |
13 | 12 | sselda 3921 |
. . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → 𝑤 ∈ 𝑋) |
14 | | conjghm.p |
. . . . . . . . . 10
⊢ + =
(+g‘𝐺) |
15 | 7, 14 | grpass 18586 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝐴) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((((invg‘𝐺)‘𝐴) + 𝑤) + 𝐴) = (((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) |
16 | 2, 10, 13, 6, 15 | syl13anc 1371 |
. . . . . . . 8
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((((invg‘𝐺)‘𝐴) + 𝑤) + 𝐴) = (((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) |
17 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐺) = (0g‘𝐺) |
18 | 7, 14, 17, 8 | grprinv 18629 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐴 +
((invg‘𝐺)‘𝐴)) = (0g‘𝐺)) |
19 | 2, 6, 18 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐴 +
((invg‘𝐺)‘𝐴)) = (0g‘𝐺)) |
20 | 19 | oveq1d 7290 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝐴 +
((invg‘𝐺)‘𝐴)) + 𝑤) = ((0g‘𝐺) + 𝑤)) |
21 | 7, 14 | grpass 18586 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝐴 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝐴) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝐴 +
((invg‘𝐺)‘𝐴)) + 𝑤) = (𝐴 +
(((invg‘𝐺)‘𝐴) + 𝑤))) |
22 | 2, 6, 10, 13, 21 | syl13anc 1371 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝐴 +
((invg‘𝐺)‘𝐴)) + 𝑤) = (𝐴 +
(((invg‘𝐺)‘𝐴) + 𝑤))) |
23 | 7, 14, 17 | grplid 18609 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋) → ((0g‘𝐺) + 𝑤) = 𝑤) |
24 | 2, 13, 23 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((0g‘𝐺) + 𝑤) = 𝑤) |
25 | 20, 22, 24 | 3eqtr3d 2786 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐴 +
(((invg‘𝐺)‘𝐴) + 𝑤)) = 𝑤) |
26 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → 𝑤 ∈ 𝑆) |
27 | 25, 26 | eqeltrd 2839 |
. . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐴 +
(((invg‘𝐺)‘𝐴) + 𝑤)) ∈ 𝑆) |
28 | 7, 14 | grpcl 18585 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧
((invg‘𝐺)‘𝐴) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (((invg‘𝐺)‘𝐴) + 𝑤) ∈ 𝑋) |
29 | 2, 10, 13, 28 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (((invg‘𝐺)‘𝐴) + 𝑤) ∈ 𝑋) |
30 | 3 | nmzbi 18792 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑁 ∧ (((invg‘𝐺)‘𝐴) + 𝑤) ∈ 𝑋) → ((𝐴 +
(((invg‘𝐺)‘𝐴) + 𝑤)) ∈ 𝑆 ↔ ((((invg‘𝐺)‘𝐴) + 𝑤) + 𝐴) ∈ 𝑆)) |
31 | 5, 29, 30 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝐴 +
(((invg‘𝐺)‘𝐴) + 𝑤)) ∈ 𝑆 ↔ ((((invg‘𝐺)‘𝐴) + 𝑤) + 𝐴) ∈ 𝑆)) |
32 | 27, 31 | mpbid 231 |
. . . . . . . 8
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((((invg‘𝐺)‘𝐴) + 𝑤) + 𝐴) ∈ 𝑆) |
33 | 16, 32 | eqeltrrd 2840 |
. . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)) ∈ 𝑆) |
34 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝑥 =
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)) → (𝐴 + 𝑥) = (𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)))) |
35 | 34 | oveq1d 7290 |
. . . . . . . 8
⊢ (𝑥 =
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)) → ((𝐴 + 𝑥) − 𝐴) = ((𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) − 𝐴)) |
36 | | conjsubg.f |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴)) |
37 | | ovex 7308 |
. . . . . . . 8
⊢ ((𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) − 𝐴) ∈ V |
38 | 35, 36, 37 | fvmpt 6875 |
. . . . . . 7
⊢
((((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)) ∈ 𝑆 → (𝐹‘(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) = ((𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) − 𝐴)) |
39 | 33, 38 | syl 17 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐹‘(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) = ((𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) − 𝐴)) |
40 | 19 | oveq1d 7290 |
. . . . . . . 8
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝐴 +
((invg‘𝐺)‘𝐴)) + (𝑤 + 𝐴)) = ((0g‘𝐺) + (𝑤 + 𝐴))) |
41 | 7, 14 | grpcl 18585 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑤 + 𝐴) ∈ 𝑋) |
42 | 2, 13, 6, 41 | syl3anc 1370 |
. . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝑤 + 𝐴) ∈ 𝑋) |
43 | 7, 14 | grpass 18586 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝐴 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝐴) ∈ 𝑋 ∧ (𝑤 + 𝐴) ∈ 𝑋)) → ((𝐴 +
((invg‘𝐺)‘𝐴)) + (𝑤 + 𝐴)) = (𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)))) |
44 | 2, 6, 10, 42, 43 | syl13anc 1371 |
. . . . . . . 8
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝐴 +
((invg‘𝐺)‘𝐴)) + (𝑤 + 𝐴)) = (𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)))) |
45 | 7, 14, 17 | grplid 18609 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝑤 + 𝐴) ∈ 𝑋) → ((0g‘𝐺) + (𝑤 + 𝐴)) = (𝑤 + 𝐴)) |
46 | 2, 42, 45 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((0g‘𝐺) + (𝑤 + 𝐴)) = (𝑤 + 𝐴)) |
47 | 40, 44, 46 | 3eqtr3d 2786 |
. . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) = (𝑤 + 𝐴)) |
48 | 47 | oveq1d 7290 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) − 𝐴) = ((𝑤 + 𝐴) − 𝐴)) |
49 | | conjghm.m |
. . . . . . . 8
⊢ − =
(-g‘𝐺) |
50 | 7, 14, 49 | grppncan 18666 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑤 + 𝐴) − 𝐴) = 𝑤) |
51 | 2, 13, 6, 50 | syl3anc 1370 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝑤 + 𝐴) − 𝐴) = 𝑤) |
52 | 39, 48, 51 | 3eqtrd 2782 |
. . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐹‘(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) = 𝑤) |
53 | | ovex 7308 |
. . . . . . 7
⊢ ((𝐴 + 𝑥) − 𝐴) ∈ V |
54 | 53, 36 | fnmpti 6576 |
. . . . . 6
⊢ 𝐹 Fn 𝑆 |
55 | | fnfvelrn 6958 |
. . . . . 6
⊢ ((𝐹 Fn 𝑆 ∧ (((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)) ∈ 𝑆) → (𝐹‘(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) ∈ ran 𝐹) |
56 | 54, 33, 55 | sylancr 587 |
. . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐹‘(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) ∈ ran 𝐹) |
57 | 52, 56 | eqeltrrd 2840 |
. . . 4
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → 𝑤 ∈ ran 𝐹) |
58 | 57 | ex 413 |
. . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → (𝑤 ∈ 𝑆 → 𝑤 ∈ ran 𝐹)) |
59 | 58 | ssrdv 3927 |
. 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝑆 ⊆ ran 𝐹) |
60 | 1 | ad2antrr 723 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → 𝐺 ∈ Grp) |
61 | | simplr 766 |
. . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ 𝑁) |
62 | 4, 61 | sselid 3919 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ 𝑋) |
63 | 12 | sselda 3921 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑋) |
64 | 7, 14, 49 | grpaddsubass 18665 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝐴 + 𝑥) − 𝐴) = (𝐴 + (𝑥 − 𝐴))) |
65 | 60, 62, 63, 62, 64 | syl13anc 1371 |
. . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → ((𝐴 + 𝑥) − 𝐴) = (𝐴 + (𝑥 − 𝐴))) |
66 | 7, 14, 49 | grpnpcan 18667 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑥 − 𝐴) + 𝐴) = 𝑥) |
67 | 60, 63, 62, 66 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝐴) + 𝐴) = 𝑥) |
68 | | simpr 485 |
. . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
69 | 67, 68 | eqeltrd 2839 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝐴) + 𝐴) ∈ 𝑆) |
70 | 7, 49 | grpsubcl 18655 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑥 − 𝐴) ∈ 𝑋) |
71 | 60, 63, 62, 70 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝐴) ∈ 𝑋) |
72 | 3 | nmzbi 18792 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑁 ∧ (𝑥 − 𝐴) ∈ 𝑋) → ((𝐴 + (𝑥 − 𝐴)) ∈ 𝑆 ↔ ((𝑥 − 𝐴) + 𝐴) ∈ 𝑆)) |
73 | 61, 71, 72 | syl2anc 584 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → ((𝐴 + (𝑥 − 𝐴)) ∈ 𝑆 ↔ ((𝑥 − 𝐴) + 𝐴) ∈ 𝑆)) |
74 | 69, 73 | mpbird 256 |
. . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → (𝐴 + (𝑥 − 𝐴)) ∈ 𝑆) |
75 | 65, 74 | eqeltrd 2839 |
. . . 4
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → ((𝐴 + 𝑥) − 𝐴) ∈ 𝑆) |
76 | 75, 36 | fmptd 6988 |
. . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝐹:𝑆⟶𝑆) |
77 | 76 | frnd 6608 |
. 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → ran 𝐹 ⊆ 𝑆) |
78 | 59, 77 | eqssd 3938 |
1
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝑆 = ran 𝐹) |