| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | conjghm.x | . . . . . . . . 9
⊢ 𝑋 = (Base‘𝐺) | 
| 2 |  | conjghm.p | . . . . . . . . 9
⊢  + =
(+g‘𝐺) | 
| 3 |  | subgrcl 19150 | . . . . . . . . . 10
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) | 
| 4 | 3 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → 𝐺 ∈ Grp) | 
| 5 |  | eqid 2736 | . . . . . . . . . 10
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 6 |  | conjnmz.1 | . . . . . . . . . . . 12
⊢ 𝑁 = {𝑦 ∈ 𝑋 ∣ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)} | 
| 7 | 6 | ssrab3 4081 | . . . . . . . . . . 11
⊢ 𝑁 ⊆ 𝑋 | 
| 8 |  | simplr 768 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → 𝐴 ∈ 𝑁) | 
| 9 | 7, 8 | sselid 3980 | . . . . . . . . . 10
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → 𝐴 ∈ 𝑋) | 
| 10 | 1, 5, 4, 9 | grpinvcld 19007 | . . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((invg‘𝐺)‘𝐴) ∈ 𝑋) | 
| 11 | 1 | subgss 19146 | . . . . . . . . . . 11
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑋) | 
| 12 | 11 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝑆 ⊆ 𝑋) | 
| 13 | 12 | sselda 3982 | . . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → 𝑤 ∈ 𝑋) | 
| 14 | 1, 2, 4, 10, 13, 9 | grpassd 18964 | . . . . . . . 8
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((((invg‘𝐺)‘𝐴) + 𝑤) + 𝐴) = (((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) | 
| 15 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 16 | 1, 2, 15, 5, 4, 9 | grprinvd 19014 | . . . . . . . . . . . 12
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐴 +
((invg‘𝐺)‘𝐴)) = (0g‘𝐺)) | 
| 17 | 16 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝐴 +
((invg‘𝐺)‘𝐴)) + 𝑤) = ((0g‘𝐺) + 𝑤)) | 
| 18 | 1, 2, 4, 9, 10, 13 | grpassd 18964 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝐴 +
((invg‘𝐺)‘𝐴)) + 𝑤) = (𝐴 +
(((invg‘𝐺)‘𝐴) + 𝑤))) | 
| 19 | 1, 2, 15, 4, 13 | grplidd 18988 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((0g‘𝐺) + 𝑤) = 𝑤) | 
| 20 | 17, 18, 19 | 3eqtr3d 2784 | . . . . . . . . . 10
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐴 +
(((invg‘𝐺)‘𝐴) + 𝑤)) = 𝑤) | 
| 21 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → 𝑤 ∈ 𝑆) | 
| 22 | 20, 21 | eqeltrd 2840 | . . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐴 +
(((invg‘𝐺)‘𝐴) + 𝑤)) ∈ 𝑆) | 
| 23 | 1, 2, 4, 10, 13 | grpcld 18966 | . . . . . . . . . 10
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (((invg‘𝐺)‘𝐴) + 𝑤) ∈ 𝑋) | 
| 24 | 6 | nmzbi 19183 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑁 ∧ (((invg‘𝐺)‘𝐴) + 𝑤) ∈ 𝑋) → ((𝐴 +
(((invg‘𝐺)‘𝐴) + 𝑤)) ∈ 𝑆 ↔ ((((invg‘𝐺)‘𝐴) + 𝑤) + 𝐴) ∈ 𝑆)) | 
| 25 | 8, 23, 24 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝐴 +
(((invg‘𝐺)‘𝐴) + 𝑤)) ∈ 𝑆 ↔ ((((invg‘𝐺)‘𝐴) + 𝑤) + 𝐴) ∈ 𝑆)) | 
| 26 | 22, 25 | mpbid 232 | . . . . . . . 8
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((((invg‘𝐺)‘𝐴) + 𝑤) + 𝐴) ∈ 𝑆) | 
| 27 | 14, 26 | eqeltrrd 2841 | . . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)) ∈ 𝑆) | 
| 28 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑥 =
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)) → (𝐴 + 𝑥) = (𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)))) | 
| 29 | 28 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑥 =
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)) → ((𝐴 + 𝑥) − 𝐴) = ((𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) − 𝐴)) | 
| 30 |  | conjsubg.f | . . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴)) | 
| 31 |  | ovex 7465 | . . . . . . . 8
⊢ ((𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) − 𝐴) ∈ V | 
| 32 | 29, 30, 31 | fvmpt 7015 | . . . . . . 7
⊢
((((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)) ∈ 𝑆 → (𝐹‘(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) = ((𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) − 𝐴)) | 
| 33 | 27, 32 | syl 17 | . . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐹‘(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) = ((𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) − 𝐴)) | 
| 34 | 16 | oveq1d 7447 | . . . . . . . 8
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝐴 +
((invg‘𝐺)‘𝐴)) + (𝑤 + 𝐴)) = ((0g‘𝐺) + (𝑤 + 𝐴))) | 
| 35 | 1, 2, 4, 13, 9 | grpcld 18966 | . . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝑤 + 𝐴) ∈ 𝑋) | 
| 36 | 1, 2, 4, 9, 10, 35 | grpassd 18964 | . . . . . . . 8
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝐴 +
((invg‘𝐺)‘𝐴)) + (𝑤 + 𝐴)) = (𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)))) | 
| 37 | 1, 2, 15, 4, 35 | grplidd 18988 | . . . . . . . 8
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((0g‘𝐺) + (𝑤 + 𝐴)) = (𝑤 + 𝐴)) | 
| 38 | 34, 36, 37 | 3eqtr3d 2784 | . . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) = (𝑤 + 𝐴)) | 
| 39 | 38 | oveq1d 7447 | . . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝐴 +
(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) − 𝐴) = ((𝑤 + 𝐴) − 𝐴)) | 
| 40 |  | conjghm.m | . . . . . . . 8
⊢  − =
(-g‘𝐺) | 
| 41 | 1, 2, 40 | grppncan 19050 | . . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑤 + 𝐴) − 𝐴) = 𝑤) | 
| 42 | 4, 13, 9, 41 | syl3anc 1372 | . . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → ((𝑤 + 𝐴) − 𝐴) = 𝑤) | 
| 43 | 33, 39, 42 | 3eqtrd 2780 | . . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐹‘(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) = 𝑤) | 
| 44 |  | ovex 7465 | . . . . . . 7
⊢ ((𝐴 + 𝑥) − 𝐴) ∈ V | 
| 45 | 44, 30 | fnmpti 6710 | . . . . . 6
⊢ 𝐹 Fn 𝑆 | 
| 46 |  | fnfvelrn 7099 | . . . . . 6
⊢ ((𝐹 Fn 𝑆 ∧ (((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴)) ∈ 𝑆) → (𝐹‘(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) ∈ ran 𝐹) | 
| 47 | 45, 27, 46 | sylancr 587 | . . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → (𝐹‘(((invg‘𝐺)‘𝐴) + (𝑤 + 𝐴))) ∈ ran 𝐹) | 
| 48 | 43, 47 | eqeltrrd 2841 | . . . 4
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑤 ∈ 𝑆) → 𝑤 ∈ ran 𝐹) | 
| 49 | 48 | ex 412 | . . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → (𝑤 ∈ 𝑆 → 𝑤 ∈ ran 𝐹)) | 
| 50 | 49 | ssrdv 3988 | . 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝑆 ⊆ ran 𝐹) | 
| 51 | 3 | ad2antrr 726 | . . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → 𝐺 ∈ Grp) | 
| 52 |  | simplr 768 | . . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ 𝑁) | 
| 53 | 7, 52 | sselid 3980 | . . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ 𝑋) | 
| 54 | 12 | sselda 3982 | . . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑋) | 
| 55 | 1, 2, 40 | grpaddsubass 19049 | . . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝐴 + 𝑥) − 𝐴) = (𝐴 + (𝑥 − 𝐴))) | 
| 56 | 51, 53, 54, 53, 55 | syl13anc 1373 | . . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → ((𝐴 + 𝑥) − 𝐴) = (𝐴 + (𝑥 − 𝐴))) | 
| 57 | 1, 2, 40 | grpnpcan 19051 | . . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝑥 − 𝐴) + 𝐴) = 𝑥) | 
| 58 | 51, 54, 53, 57 | syl3anc 1372 | . . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝐴) + 𝐴) = 𝑥) | 
| 59 |  | simpr 484 | . . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) | 
| 60 | 58, 59 | eqeltrd 2840 | . . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → ((𝑥 − 𝐴) + 𝐴) ∈ 𝑆) | 
| 61 | 1, 40 | grpsubcl 19039 | . . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑥 − 𝐴) ∈ 𝑋) | 
| 62 | 51, 54, 53, 61 | syl3anc 1372 | . . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → (𝑥 − 𝐴) ∈ 𝑋) | 
| 63 | 6 | nmzbi 19183 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑁 ∧ (𝑥 − 𝐴) ∈ 𝑋) → ((𝐴 + (𝑥 − 𝐴)) ∈ 𝑆 ↔ ((𝑥 − 𝐴) + 𝐴) ∈ 𝑆)) | 
| 64 | 52, 62, 63 | syl2anc 584 | . . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → ((𝐴 + (𝑥 − 𝐴)) ∈ 𝑆 ↔ ((𝑥 − 𝐴) + 𝐴) ∈ 𝑆)) | 
| 65 | 60, 64 | mpbird 257 | . . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → (𝐴 + (𝑥 − 𝐴)) ∈ 𝑆) | 
| 66 | 56, 65 | eqeltrd 2840 | . . . 4
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) ∧ 𝑥 ∈ 𝑆) → ((𝐴 + 𝑥) − 𝐴) ∈ 𝑆) | 
| 67 | 66, 30 | fmptd 7133 | . . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝐹:𝑆⟶𝑆) | 
| 68 | 67 | frnd 6743 | . 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → ran 𝐹 ⊆ 𝑆) | 
| 69 | 50, 68 | eqssd 4000 | 1
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝑆 = ran 𝐹) |