Step | Hyp | Ref
| Expression |
1 | | conjnmz.1 |
. . . . 5
⊢ 𝑁 = {𝑦 ∈ 𝑋 ∣ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)} |
2 | 1 | ssrab3 4015 |
. . . 4
⊢ 𝑁 ⊆ 𝑋 |
3 | | simpr 485 |
. . . 4
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝐴 ∈ 𝑁) |
4 | 2, 3 | sselid 3919 |
. . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝐴 ∈ 𝑋) |
5 | | conjghm.x |
. . . 4
⊢ 𝑋 = (Base‘𝐺) |
6 | | conjghm.p |
. . . 4
⊢ + =
(+g‘𝐺) |
7 | | conjghm.m |
. . . 4
⊢ − =
(-g‘𝐺) |
8 | | conjsubg.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴)) |
9 | 5, 6, 7, 8, 1 | conjnmz 18868 |
. . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝑆 = ran 𝐹) |
10 | 4, 9 | jca 512 |
. 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) |
11 | | simprl 768 |
. . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) → 𝐴 ∈ 𝑋) |
12 | | simplrr 775 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) ∧ 𝑤 ∈ 𝑋) → 𝑆 = ran 𝐹) |
13 | 12 | eleq2d 2824 |
. . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) ∧ 𝑤 ∈ 𝑋) → ((𝐴 + 𝑤) ∈ 𝑆 ↔ (𝐴 + 𝑤) ∈ ran 𝐹)) |
14 | | subgrcl 18760 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
15 | 14 | ad3antrrr 727 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → 𝐺 ∈ Grp) |
16 | | simpllr 773 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ 𝑋) |
17 | 5 | subgss 18756 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑋) |
18 | 17 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → 𝑆 ⊆ 𝑋) |
19 | 18 | sselda 3921 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑋) |
20 | 5, 6, 7 | grpaddsubass 18665 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝐴 + 𝑥) − 𝐴) = (𝐴 + (𝑥 − 𝐴))) |
21 | 15, 16, 19, 16, 20 | syl13anc 1371 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → ((𝐴 + 𝑥) − 𝐴) = (𝐴 + (𝑥 − 𝐴))) |
22 | 21 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → (((𝐴 + 𝑥) − 𝐴) = (𝐴 + 𝑤) ↔ (𝐴 + (𝑥 − 𝐴)) = (𝐴 + 𝑤))) |
23 | 5, 7 | grpsubcl 18655 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑥 − 𝐴) ∈ 𝑋) |
24 | 15, 19, 16, 23 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝐴) ∈ 𝑋) |
25 | | simplr 766 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → 𝑤 ∈ 𝑋) |
26 | 5, 6 | grplcan 18637 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ ((𝑥 − 𝐴) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝐴 + (𝑥 − 𝐴)) = (𝐴 + 𝑤) ↔ (𝑥 − 𝐴) = 𝑤)) |
27 | 15, 24, 25, 16, 26 | syl13anc 1371 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → ((𝐴 + (𝑥 − 𝐴)) = (𝐴 + 𝑤) ↔ (𝑥 − 𝐴) = 𝑤)) |
28 | 5, 6, 7 | grpsubadd 18663 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝑥 − 𝐴) = 𝑤 ↔ (𝑤 + 𝐴) = 𝑥)) |
29 | 15, 19, 16, 25, 28 | syl13anc 1371 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝐴) = 𝑤 ↔ (𝑤 + 𝐴) = 𝑥)) |
30 | 22, 27, 29 | 3bitrd 305 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → (((𝐴 + 𝑥) − 𝐴) = (𝐴 + 𝑤) ↔ (𝑤 + 𝐴) = 𝑥)) |
31 | | eqcom 2745 |
. . . . . . . . 9
⊢ ((𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴) ↔ ((𝐴 + 𝑥) − 𝐴) = (𝐴 + 𝑤)) |
32 | | eqcom 2745 |
. . . . . . . . 9
⊢ (𝑥 = (𝑤 + 𝐴) ↔ (𝑤 + 𝐴) = 𝑥) |
33 | 30, 31, 32 | 3bitr4g 314 |
. . . . . . . 8
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → ((𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴) ↔ 𝑥 = (𝑤 + 𝐴))) |
34 | 33 | rexbidva 3225 |
. . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (∃𝑥 ∈ 𝑆 (𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴) ↔ ∃𝑥 ∈ 𝑆 𝑥 = (𝑤 + 𝐴))) |
35 | 34 | adantlrr 718 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) ∧ 𝑤 ∈ 𝑋) → (∃𝑥 ∈ 𝑆 (𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴) ↔ ∃𝑥 ∈ 𝑆 𝑥 = (𝑤 + 𝐴))) |
36 | | ovex 7308 |
. . . . . . 7
⊢ (𝐴 + 𝑤) ∈ V |
37 | | eqeq1 2742 |
. . . . . . . 8
⊢ (𝑦 = (𝐴 + 𝑤) → (𝑦 = ((𝐴 + 𝑥) − 𝐴) ↔ (𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴))) |
38 | 37 | rexbidv 3226 |
. . . . . . 7
⊢ (𝑦 = (𝐴 + 𝑤) → (∃𝑥 ∈ 𝑆 𝑦 = ((𝐴 + 𝑥) − 𝐴) ↔ ∃𝑥 ∈ 𝑆 (𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴))) |
39 | 8 | rnmpt 5864 |
. . . . . . 7
⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝑆 𝑦 = ((𝐴 + 𝑥) − 𝐴)} |
40 | 36, 38, 39 | elab2 3613 |
. . . . . 6
⊢ ((𝐴 + 𝑤) ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑆 (𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴)) |
41 | | risset 3194 |
. . . . . 6
⊢ ((𝑤 + 𝐴) ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑆 𝑥 = (𝑤 + 𝐴)) |
42 | 35, 40, 41 | 3bitr4g 314 |
. . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) ∧ 𝑤 ∈ 𝑋) → ((𝐴 + 𝑤) ∈ ran 𝐹 ↔ (𝑤 + 𝐴) ∈ 𝑆)) |
43 | 13, 42 | bitrd 278 |
. . . 4
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) ∧ 𝑤 ∈ 𝑋) → ((𝐴 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝐴) ∈ 𝑆)) |
44 | 43 | ralrimiva 3103 |
. . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) → ∀𝑤 ∈ 𝑋 ((𝐴 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝐴) ∈ 𝑆)) |
45 | 1 | elnmz 18791 |
. . 3
⊢ (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑤 ∈ 𝑋 ((𝐴 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝐴) ∈ 𝑆))) |
46 | 11, 44, 45 | sylanbrc 583 |
. 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) → 𝐴 ∈ 𝑁) |
47 | 10, 46 | impbida 798 |
1
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹))) |