| Step | Hyp | Ref
| Expression |
| 1 | | conjnmz.1 |
. . . . 5
⊢ 𝑁 = {𝑦 ∈ 𝑋 ∣ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)} |
| 2 | 1 | ssrab3 4082 |
. . . 4
⊢ 𝑁 ⊆ 𝑋 |
| 3 | | simpr 484 |
. . . 4
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝐴 ∈ 𝑁) |
| 4 | 2, 3 | sselid 3981 |
. . 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 19270 |
. . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝑆 = ran 𝐹) |
| 10 | 4, 9 | jca 511 |
. 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) |
| 11 | | simprl 771 |
. . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) → 𝐴 ∈ 𝑋) |
| 12 | | simplrr 778 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) ∧ 𝑤 ∈ 𝑋) → 𝑆 = ran 𝐹) |
| 13 | 12 | eleq2d 2827 |
. . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) ∧ 𝑤 ∈ 𝑋) → ((𝐴 + 𝑤) ∈ 𝑆 ↔ (𝐴 + 𝑤) ∈ ran 𝐹)) |
| 14 | | subgrcl 19149 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
| 15 | 14 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → 𝐺 ∈ Grp) |
| 16 | | simpllr 776 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ 𝑋) |
| 17 | 5 | subgss 19145 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑋) |
| 18 | 17 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → 𝑆 ⊆ 𝑋) |
| 19 | 18 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑋) |
| 20 | 5, 6, 7 | grpaddsubass 19048 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝐴 + 𝑥) − 𝐴) = (𝐴 + (𝑥 − 𝐴))) |
| 21 | 15, 16, 19, 16, 20 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → ((𝐴 + 𝑥) − 𝐴) = (𝐴 + (𝑥 − 𝐴))) |
| 22 | 21 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → (((𝐴 + 𝑥) − 𝐴) = (𝐴 + 𝑤) ↔ (𝐴 + (𝑥 − 𝐴)) = (𝐴 + 𝑤))) |
| 23 | 5, 7 | grpsubcl 19038 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑥 − 𝐴) ∈ 𝑋) |
| 24 | 15, 19, 16, 23 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝐴) ∈ 𝑋) |
| 25 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → 𝑤 ∈ 𝑋) |
| 26 | 5, 6 | grplcan 19018 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ ((𝑥 − 𝐴) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝐴 + (𝑥 − 𝐴)) = (𝐴 + 𝑤) ↔ (𝑥 − 𝐴) = 𝑤)) |
| 27 | 15, 24, 25, 16, 26 | syl13anc 1374 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → ((𝐴 + (𝑥 − 𝐴)) = (𝐴 + 𝑤) ↔ (𝑥 − 𝐴) = 𝑤)) |
| 28 | 5, 6, 7 | grpsubadd 19046 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝑥 − 𝐴) = 𝑤 ↔ (𝑤 + 𝐴) = 𝑥)) |
| 29 | 15, 19, 16, 25, 28 | syl13anc 1374 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝐴) = 𝑤 ↔ (𝑤 + 𝐴) = 𝑥)) |
| 30 | 22, 27, 29 | 3bitrd 305 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → (((𝐴 + 𝑥) − 𝐴) = (𝐴 + 𝑤) ↔ (𝑤 + 𝐴) = 𝑥)) |
| 31 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴) ↔ ((𝐴 + 𝑥) − 𝐴) = (𝐴 + 𝑤)) |
| 32 | | eqcom 2744 |
. . . . . . . . 9
⊢ (𝑥 = (𝑤 + 𝐴) ↔ (𝑤 + 𝐴) = 𝑥) |
| 33 | 30, 31, 32 | 3bitr4g 314 |
. . . . . . . 8
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ 𝑥 ∈ 𝑆) → ((𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴) ↔ 𝑥 = (𝑤 + 𝐴))) |
| 34 | 33 | rexbidva 3177 |
. . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → (∃𝑥 ∈ 𝑆 (𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴) ↔ ∃𝑥 ∈ 𝑆 𝑥 = (𝑤 + 𝐴))) |
| 35 | 34 | adantlrr 721 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) ∧ 𝑤 ∈ 𝑋) → (∃𝑥 ∈ 𝑆 (𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴) ↔ ∃𝑥 ∈ 𝑆 𝑥 = (𝑤 + 𝐴))) |
| 36 | | ovex 7464 |
. . . . . . 7
⊢ (𝐴 + 𝑤) ∈ V |
| 37 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑦 = (𝐴 + 𝑤) → (𝑦 = ((𝐴 + 𝑥) − 𝐴) ↔ (𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴))) |
| 38 | 37 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑦 = (𝐴 + 𝑤) → (∃𝑥 ∈ 𝑆 𝑦 = ((𝐴 + 𝑥) − 𝐴) ↔ ∃𝑥 ∈ 𝑆 (𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴))) |
| 39 | 8 | rnmpt 5968 |
. . . . . . 7
⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝑆 𝑦 = ((𝐴 + 𝑥) − 𝐴)} |
| 40 | 36, 38, 39 | elab2 3682 |
. . . . . 6
⊢ ((𝐴 + 𝑤) ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑆 (𝐴 + 𝑤) = ((𝐴 + 𝑥) − 𝐴)) |
| 41 | | risset 3233 |
. . . . . 6
⊢ ((𝑤 + 𝐴) ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑆 𝑥 = (𝑤 + 𝐴)) |
| 42 | 35, 40, 41 | 3bitr4g 314 |
. . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) ∧ 𝑤 ∈ 𝑋) → ((𝐴 + 𝑤) ∈ ran 𝐹 ↔ (𝑤 + 𝐴) ∈ 𝑆)) |
| 43 | 13, 42 | bitrd 279 |
. . . 4
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) ∧ 𝑤 ∈ 𝑋) → ((𝐴 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝐴) ∈ 𝑆)) |
| 44 | 43 | ralrimiva 3146 |
. . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) → ∀𝑤 ∈ 𝑋 ((𝐴 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝐴) ∈ 𝑆)) |
| 45 | 1 | elnmz 19181 |
. . 3
⊢ (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑤 ∈ 𝑋 ((𝐴 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝐴) ∈ 𝑆))) |
| 46 | 11, 44, 45 | sylanbrc 583 |
. 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)) → 𝐴 ∈ 𝑁) |
| 47 | 10, 46 | impbida 801 |
1
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹))) |