| Step | Hyp | Ref
| Expression |
| 1 | | elnmz.1 |
. . . 4
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} |
| 2 | 1 | ssrab3 4082 |
. . 3
⊢ 𝑁 ⊆ 𝑋 |
| 3 | 2 | a1i 11 |
. 2
⊢ (𝐺 ∈ Grp → 𝑁 ⊆ 𝑋) |
| 4 | | nmzsubg.2 |
. . . . 5
⊢ 𝑋 = (Base‘𝐺) |
| 5 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 6 | 4, 5 | grpidcl 18983 |
. . . 4
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑋) |
| 7 | | nmzsubg.3 |
. . . . . . . 8
⊢ + =
(+g‘𝐺) |
| 8 | 4, 7, 5 | grplid 18985 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((0g‘𝐺) + 𝑧) = 𝑧) |
| 9 | 4, 7, 5 | grprid 18986 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → (𝑧 + (0g‘𝐺)) = 𝑧) |
| 10 | 8, 9 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((0g‘𝐺) + 𝑧) = (𝑧 + (0g‘𝐺))) |
| 11 | 10 | eleq1d 2826 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → (((0g‘𝐺) + 𝑧) ∈ 𝑆 ↔ (𝑧 + (0g‘𝐺)) ∈ 𝑆)) |
| 12 | 11 | ralrimiva 3146 |
. . . 4
⊢ (𝐺 ∈ Grp → ∀𝑧 ∈ 𝑋 (((0g‘𝐺) + 𝑧) ∈ 𝑆 ↔ (𝑧 + (0g‘𝐺)) ∈ 𝑆)) |
| 13 | 1 | elnmz 19181 |
. . . 4
⊢
((0g‘𝐺) ∈ 𝑁 ↔ ((0g‘𝐺) ∈ 𝑋 ∧ ∀𝑧 ∈ 𝑋 (((0g‘𝐺) + 𝑧) ∈ 𝑆 ↔ (𝑧 + (0g‘𝐺)) ∈ 𝑆))) |
| 14 | 6, 12, 13 | sylanbrc 583 |
. . 3
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑁) |
| 15 | 14 | ne0d 4342 |
. 2
⊢ (𝐺 ∈ Grp → 𝑁 ≠ ∅) |
| 16 | | id 22 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Grp) |
| 17 | 2 | sseli 3979 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑁 → 𝑧 ∈ 𝑋) |
| 18 | 2 | sseli 3979 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝑁 → 𝑤 ∈ 𝑋) |
| 19 | 4, 7 | grpcl 18959 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑧 + 𝑤) ∈ 𝑋) |
| 20 | 16, 17, 18, 19 | syl3an 1161 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) → (𝑧 + 𝑤) ∈ 𝑋) |
| 21 | | simpl1 1192 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝐺 ∈ Grp) |
| 22 | | simpl2 1193 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑧 ∈ 𝑁) |
| 23 | 2, 22 | sselid 3981 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
| 24 | | simpl3 1194 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑤 ∈ 𝑁) |
| 25 | 2, 24 | sselid 3981 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑤 ∈ 𝑋) |
| 26 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋) |
| 27 | 4, 7 | grpass 18960 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑧 + 𝑤) + 𝑢) = (𝑧 + (𝑤 + 𝑢))) |
| 28 | 21, 23, 25, 26, 27 | syl13anc 1374 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 + 𝑤) + 𝑢) = (𝑧 + (𝑤 + 𝑢))) |
| 29 | 28 | eleq1d 2826 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((𝑧 + 𝑤) + 𝑢) ∈ 𝑆 ↔ (𝑧 + (𝑤 + 𝑢)) ∈ 𝑆)) |
| 30 | 4, 7, 21, 25, 26 | grpcld 18965 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑤 + 𝑢) ∈ 𝑋) |
| 31 | 1 | nmzbi 19182 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑁 ∧ (𝑤 + 𝑢) ∈ 𝑋) → ((𝑧 + (𝑤 + 𝑢)) ∈ 𝑆 ↔ ((𝑤 + 𝑢) + 𝑧) ∈ 𝑆)) |
| 32 | 22, 30, 31 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 + (𝑤 + 𝑢)) ∈ 𝑆 ↔ ((𝑤 + 𝑢) + 𝑧) ∈ 𝑆)) |
| 33 | 4, 7 | grpass 18960 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑤 + 𝑢) + 𝑧) = (𝑤 + (𝑢 + 𝑧))) |
| 34 | 21, 25, 26, 23, 33 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑤 + 𝑢) + 𝑧) = (𝑤 + (𝑢 + 𝑧))) |
| 35 | 34 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((𝑤 + 𝑢) + 𝑧) ∈ 𝑆 ↔ (𝑤 + (𝑢 + 𝑧)) ∈ 𝑆)) |
| 36 | 4, 7, 21, 26, 23 | grpcld 18965 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑢 + 𝑧) ∈ 𝑋) |
| 37 | 1 | nmzbi 19182 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝑁 ∧ (𝑢 + 𝑧) ∈ 𝑋) → ((𝑤 + (𝑢 + 𝑧)) ∈ 𝑆 ↔ ((𝑢 + 𝑧) + 𝑤) ∈ 𝑆)) |
| 38 | 24, 36, 37 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑤 + (𝑢 + 𝑧)) ∈ 𝑆 ↔ ((𝑢 + 𝑧) + 𝑤) ∈ 𝑆)) |
| 39 | 32, 35, 38 | 3bitrd 305 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 + (𝑤 + 𝑢)) ∈ 𝑆 ↔ ((𝑢 + 𝑧) + 𝑤) ∈ 𝑆)) |
| 40 | 4, 7 | grpass 18960 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑧) + 𝑤) = (𝑢 + (𝑧 + 𝑤))) |
| 41 | 21, 26, 23, 25, 40 | syl13anc 1374 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑢 + 𝑧) + 𝑤) = (𝑢 + (𝑧 + 𝑤))) |
| 42 | 41 | eleq1d 2826 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((𝑢 + 𝑧) + 𝑤) ∈ 𝑆 ↔ (𝑢 + (𝑧 + 𝑤)) ∈ 𝑆)) |
| 43 | 29, 39, 42 | 3bitrd 305 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((𝑧 + 𝑤) + 𝑢) ∈ 𝑆 ↔ (𝑢 + (𝑧 + 𝑤)) ∈ 𝑆)) |
| 44 | 43 | ralrimiva 3146 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) → ∀𝑢 ∈ 𝑋 (((𝑧 + 𝑤) + 𝑢) ∈ 𝑆 ↔ (𝑢 + (𝑧 + 𝑤)) ∈ 𝑆)) |
| 45 | 1 | elnmz 19181 |
. . . . . . 7
⊢ ((𝑧 + 𝑤) ∈ 𝑁 ↔ ((𝑧 + 𝑤) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑋 (((𝑧 + 𝑤) + 𝑢) ∈ 𝑆 ↔ (𝑢 + (𝑧 + 𝑤)) ∈ 𝑆))) |
| 46 | 20, 44, 45 | sylanbrc 583 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) → (𝑧 + 𝑤) ∈ 𝑁) |
| 47 | 46 | 3expa 1119 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑤 ∈ 𝑁) → (𝑧 + 𝑤) ∈ 𝑁) |
| 48 | 47 | ralrimiva 3146 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) → ∀𝑤 ∈ 𝑁 (𝑧 + 𝑤) ∈ 𝑁) |
| 49 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 50 | 4, 49 | grpinvcl 19005 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
| 51 | 17, 50 | sylan2 593 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
| 52 | | simplr 769 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑧 ∈ 𝑁) |
| 53 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝐺 ∈ Grp) |
| 54 | 51 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
| 55 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋) |
| 56 | 4, 7, 53, 55, 54 | grpcld 18965 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑋) |
| 57 | 4, 7, 53, 54, 56 | grpcld 18965 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) ∈ 𝑋) |
| 58 | 1 | nmzbi 19182 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑁 ∧ (((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) ∈ 𝑋) → ((𝑧 +
(((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧)))) ∈ 𝑆 ↔ ((((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) + 𝑧) ∈ 𝑆)) |
| 59 | 52, 57, 58 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 +
(((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧)))) ∈ 𝑆 ↔ ((((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) + 𝑧) ∈ 𝑆)) |
| 60 | 2, 52 | sselid 3981 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
| 61 | 4, 7, 5, 49 | grprinv 19008 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → (𝑧 +
((invg‘𝐺)‘𝑧)) = (0g‘𝐺)) |
| 62 | 53, 60, 61 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑧 +
((invg‘𝐺)‘𝑧)) = (0g‘𝐺)) |
| 63 | 62 | oveq1d 7446 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 +
((invg‘𝐺)‘𝑧)) + (𝑢 +
((invg‘𝐺)‘𝑧))) = ((0g‘𝐺) + (𝑢 +
((invg‘𝐺)‘𝑧)))) |
| 64 | 4, 7 | grpass 18960 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑧 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝑧) ∈ 𝑋 ∧ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑋)) → ((𝑧 +
((invg‘𝐺)‘𝑧)) + (𝑢 +
((invg‘𝐺)‘𝑧))) = (𝑧 +
(((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))))) |
| 65 | 53, 60, 54, 56, 64 | syl13anc 1374 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 +
((invg‘𝐺)‘𝑧)) + (𝑢 +
((invg‘𝐺)‘𝑧))) = (𝑧 +
(((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))))) |
| 66 | 4, 7, 5 | grplid 18985 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑋) → ((0g‘𝐺) + (𝑢 +
((invg‘𝐺)‘𝑧))) = (𝑢 +
((invg‘𝐺)‘𝑧))) |
| 67 | 53, 56, 66 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐺) + (𝑢 +
((invg‘𝐺)‘𝑧))) = (𝑢 +
((invg‘𝐺)‘𝑧))) |
| 68 | 63, 65, 67 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑧 +
(((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧)))) = (𝑢 +
((invg‘𝐺)‘𝑧))) |
| 69 | 68 | eleq1d 2826 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 +
(((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧)))) ∈ 𝑆 ↔ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑆)) |
| 70 | 4, 7 | grpass 18960 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝑧) ∈ 𝑋 ∧ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) + 𝑧) = (((invg‘𝐺)‘𝑧) + ((𝑢 +
((invg‘𝐺)‘𝑧)) + 𝑧))) |
| 71 | 53, 54, 56, 60, 70 | syl13anc 1374 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) + 𝑧) = (((invg‘𝐺)‘𝑧) + ((𝑢 +
((invg‘𝐺)‘𝑧)) + 𝑧))) |
| 72 | 4, 7 | grpass 18960 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝑧) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑢 +
((invg‘𝐺)‘𝑧)) + 𝑧) = (𝑢 +
(((invg‘𝐺)‘𝑧) + 𝑧))) |
| 73 | 53, 55, 54, 60, 72 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑢 +
((invg‘𝐺)‘𝑧)) + 𝑧) = (𝑢 +
(((invg‘𝐺)‘𝑧) + 𝑧))) |
| 74 | 4, 7, 5, 49 | grplinv 19007 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → (((invg‘𝐺)‘𝑧) + 𝑧) = (0g‘𝐺)) |
| 75 | 53, 60, 74 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((invg‘𝐺)‘𝑧) + 𝑧) = (0g‘𝐺)) |
| 76 | 75 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑢 +
(((invg‘𝐺)‘𝑧) + 𝑧)) = (𝑢 + (0g‘𝐺))) |
| 77 | 4, 7, 5 | grprid 18986 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋) → (𝑢 + (0g‘𝐺)) = 𝑢) |
| 78 | 53, 55, 77 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑢 + (0g‘𝐺)) = 𝑢) |
| 79 | 73, 76, 78 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑢 +
((invg‘𝐺)‘𝑧)) + 𝑧) = 𝑢) |
| 80 | 79 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((invg‘𝐺)‘𝑧) + ((𝑢 +
((invg‘𝐺)‘𝑧)) + 𝑧)) = (((invg‘𝐺)‘𝑧) + 𝑢)) |
| 81 | 71, 80 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) + 𝑧) = (((invg‘𝐺)‘𝑧) + 𝑢)) |
| 82 | 81 | eleq1d 2826 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) + 𝑧) ∈ 𝑆 ↔ (((invg‘𝐺)‘𝑧) + 𝑢) ∈ 𝑆)) |
| 83 | 59, 69, 82 | 3bitr3rd 310 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((((invg‘𝐺)‘𝑧) + 𝑢) ∈ 𝑆 ↔ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑆)) |
| 84 | 83 | ralrimiva 3146 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) → ∀𝑢 ∈ 𝑋 ((((invg‘𝐺)‘𝑧) + 𝑢) ∈ 𝑆 ↔ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑆)) |
| 85 | 1 | elnmz 19181 |
. . . . 5
⊢
(((invg‘𝐺)‘𝑧) ∈ 𝑁 ↔ (((invg‘𝐺)‘𝑧) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑋 ((((invg‘𝐺)‘𝑧) + 𝑢) ∈ 𝑆 ↔ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑆))) |
| 86 | 51, 84, 85 | sylanbrc 583 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) → ((invg‘𝐺)‘𝑧) ∈ 𝑁) |
| 87 | 48, 86 | jca 511 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) → (∀𝑤 ∈ 𝑁 (𝑧 + 𝑤) ∈ 𝑁 ∧ ((invg‘𝐺)‘𝑧) ∈ 𝑁)) |
| 88 | 87 | ralrimiva 3146 |
. 2
⊢ (𝐺 ∈ Grp → ∀𝑧 ∈ 𝑁 (∀𝑤 ∈ 𝑁 (𝑧 + 𝑤) ∈ 𝑁 ∧ ((invg‘𝐺)‘𝑧) ∈ 𝑁)) |
| 89 | 4, 7, 49 | issubg2 19159 |
. 2
⊢ (𝐺 ∈ Grp → (𝑁 ∈ (SubGrp‘𝐺) ↔ (𝑁 ⊆ 𝑋 ∧ 𝑁 ≠ ∅ ∧ ∀𝑧 ∈ 𝑁 (∀𝑤 ∈ 𝑁 (𝑧 + 𝑤) ∈ 𝑁 ∧ ((invg‘𝐺)‘𝑧) ∈ 𝑁)))) |
| 90 | 3, 15, 88, 89 | mpbir3and 1343 |
1
⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺)) |