Step | Hyp | Ref
| Expression |
1 | | elnmz.1 |
. . . 4
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} |
2 | | ssrab2 3650 |
. . . 4
⊢ {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} ⊆ 𝑋 |
3 | 1, 2 | eqsstri 3598 |
. . 3
⊢ 𝑁 ⊆ 𝑋 |
4 | 3 | a1i 11 |
. 2
⊢ (𝐺 ∈ Grp → 𝑁 ⊆ 𝑋) |
5 | | nmzsubg.2 |
. . . . 5
⊢ 𝑋 = (Base‘𝐺) |
6 | | eqid 2610 |
. . . . 5
⊢
(0g‘𝐺) = (0g‘𝐺) |
7 | 5, 6 | grpidcl 17273 |
. . . 4
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑋) |
8 | | nmzsubg.3 |
. . . . . . . 8
⊢ + =
(+g‘𝐺) |
9 | 5, 8, 6 | grplid 17275 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((0g‘𝐺) + 𝑧) = 𝑧) |
10 | 5, 8, 6 | grprid 17276 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → (𝑧 + (0g‘𝐺)) = 𝑧) |
11 | 9, 10 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((0g‘𝐺) + 𝑧) = (𝑧 + (0g‘𝐺))) |
12 | 11 | eleq1d 2672 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → (((0g‘𝐺) + 𝑧) ∈ 𝑆 ↔ (𝑧 + (0g‘𝐺)) ∈ 𝑆)) |
13 | 12 | ralrimiva 2949 |
. . . 4
⊢ (𝐺 ∈ Grp → ∀𝑧 ∈ 𝑋 (((0g‘𝐺) + 𝑧) ∈ 𝑆 ↔ (𝑧 + (0g‘𝐺)) ∈ 𝑆)) |
14 | 1 | elnmz 17456 |
. . . 4
⊢
((0g‘𝐺) ∈ 𝑁 ↔ ((0g‘𝐺) ∈ 𝑋 ∧ ∀𝑧 ∈ 𝑋 (((0g‘𝐺) + 𝑧) ∈ 𝑆 ↔ (𝑧 + (0g‘𝐺)) ∈ 𝑆))) |
15 | 7, 13, 14 | sylanbrc 695 |
. . 3
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑁) |
16 | | ne0i 3880 |
. . 3
⊢
((0g‘𝐺) ∈ 𝑁 → 𝑁 ≠ ∅) |
17 | 15, 16 | syl 17 |
. 2
⊢ (𝐺 ∈ Grp → 𝑁 ≠ ∅) |
18 | | id 22 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Grp) |
19 | 3 | sseli 3564 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑁 → 𝑧 ∈ 𝑋) |
20 | 3 | sseli 3564 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝑁 → 𝑤 ∈ 𝑋) |
21 | 5, 8 | grpcl 17253 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑧 + 𝑤) ∈ 𝑋) |
22 | 18, 19, 20, 21 | syl3an 1360 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) → (𝑧 + 𝑤) ∈ 𝑋) |
23 | | simpl1 1057 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝐺 ∈ Grp) |
24 | | simpl2 1058 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑧 ∈ 𝑁) |
25 | 3, 24 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
26 | | simpl3 1059 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑤 ∈ 𝑁) |
27 | 3, 26 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑤 ∈ 𝑋) |
28 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋) |
29 | 5, 8 | grpass 17254 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑧 + 𝑤) + 𝑢) = (𝑧 + (𝑤 + 𝑢))) |
30 | 23, 25, 27, 28, 29 | syl13anc 1320 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 + 𝑤) + 𝑢) = (𝑧 + (𝑤 + 𝑢))) |
31 | 30 | eleq1d 2672 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((𝑧 + 𝑤) + 𝑢) ∈ 𝑆 ↔ (𝑧 + (𝑤 + 𝑢)) ∈ 𝑆)) |
32 | 5, 8 | grpcl 17253 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑤 + 𝑢) ∈ 𝑋) |
33 | 23, 27, 28, 32 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑤 + 𝑢) ∈ 𝑋) |
34 | 1 | nmzbi 17457 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑁 ∧ (𝑤 + 𝑢) ∈ 𝑋) → ((𝑧 + (𝑤 + 𝑢)) ∈ 𝑆 ↔ ((𝑤 + 𝑢) + 𝑧) ∈ 𝑆)) |
35 | 24, 33, 34 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 + (𝑤 + 𝑢)) ∈ 𝑆 ↔ ((𝑤 + 𝑢) + 𝑧) ∈ 𝑆)) |
36 | 5, 8 | grpass 17254 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑤 + 𝑢) + 𝑧) = (𝑤 + (𝑢 + 𝑧))) |
37 | 23, 27, 28, 25, 36 | syl13anc 1320 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑤 + 𝑢) + 𝑧) = (𝑤 + (𝑢 + 𝑧))) |
38 | 37 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((𝑤 + 𝑢) + 𝑧) ∈ 𝑆 ↔ (𝑤 + (𝑢 + 𝑧)) ∈ 𝑆)) |
39 | 5, 8 | grpcl 17253 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑢 + 𝑧) ∈ 𝑋) |
40 | 23, 28, 25, 39 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑢 + 𝑧) ∈ 𝑋) |
41 | 1 | nmzbi 17457 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝑁 ∧ (𝑢 + 𝑧) ∈ 𝑋) → ((𝑤 + (𝑢 + 𝑧)) ∈ 𝑆 ↔ ((𝑢 + 𝑧) + 𝑤) ∈ 𝑆)) |
42 | 26, 40, 41 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑤 + (𝑢 + 𝑧)) ∈ 𝑆 ↔ ((𝑢 + 𝑧) + 𝑤) ∈ 𝑆)) |
43 | 35, 38, 42 | 3bitrd 293 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 + (𝑤 + 𝑢)) ∈ 𝑆 ↔ ((𝑢 + 𝑧) + 𝑤) ∈ 𝑆)) |
44 | 5, 8 | grpass 17254 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑧) + 𝑤) = (𝑢 + (𝑧 + 𝑤))) |
45 | 23, 28, 25, 27, 44 | syl13anc 1320 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑢 + 𝑧) + 𝑤) = (𝑢 + (𝑧 + 𝑤))) |
46 | 45 | eleq1d 2672 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((𝑢 + 𝑧) + 𝑤) ∈ 𝑆 ↔ (𝑢 + (𝑧 + 𝑤)) ∈ 𝑆)) |
47 | 31, 43, 46 | 3bitrd 293 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((𝑧 + 𝑤) + 𝑢) ∈ 𝑆 ↔ (𝑢 + (𝑧 + 𝑤)) ∈ 𝑆)) |
48 | 47 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) → ∀𝑢 ∈ 𝑋 (((𝑧 + 𝑤) + 𝑢) ∈ 𝑆 ↔ (𝑢 + (𝑧 + 𝑤)) ∈ 𝑆)) |
49 | 1 | elnmz 17456 |
. . . . . . 7
⊢ ((𝑧 + 𝑤) ∈ 𝑁 ↔ ((𝑧 + 𝑤) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑋 (((𝑧 + 𝑤) + 𝑢) ∈ 𝑆 ↔ (𝑢 + (𝑧 + 𝑤)) ∈ 𝑆))) |
50 | 22, 48, 49 | sylanbrc 695 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) → (𝑧 + 𝑤) ∈ 𝑁) |
51 | 50 | 3expa 1257 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑤 ∈ 𝑁) → (𝑧 + 𝑤) ∈ 𝑁) |
52 | 51 | ralrimiva 2949 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) → ∀𝑤 ∈ 𝑁 (𝑧 + 𝑤) ∈ 𝑁) |
53 | | eqid 2610 |
. . . . . . 7
⊢
(invg‘𝐺) = (invg‘𝐺) |
54 | 5, 53 | grpinvcl 17290 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
55 | 19, 54 | sylan2 490 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
56 | | simplr 788 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑧 ∈ 𝑁) |
57 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝐺 ∈ Grp) |
58 | 55 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((invg‘𝐺)‘𝑧) ∈ 𝑋) |
59 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋) |
60 | 5, 8 | grpcl 17253 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝑧) ∈ 𝑋) → (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑋) |
61 | 57, 59, 58, 60 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑋) |
62 | 5, 8 | grpcl 17253 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧
((invg‘𝐺)‘𝑧) ∈ 𝑋 ∧ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑋) → (((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) ∈ 𝑋) |
63 | 57, 58, 61, 62 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) ∈ 𝑋) |
64 | 1 | nmzbi 17457 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑁 ∧ (((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) ∈ 𝑋) → ((𝑧 +
(((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧)))) ∈ 𝑆 ↔ ((((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) + 𝑧) ∈ 𝑆)) |
65 | 56, 63, 64 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 +
(((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧)))) ∈ 𝑆 ↔ ((((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) + 𝑧) ∈ 𝑆)) |
66 | 3, 56 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
67 | 5, 8, 6, 53 | grprinv 17292 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → (𝑧 +
((invg‘𝐺)‘𝑧)) = (0g‘𝐺)) |
68 | 57, 66, 67 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑧 +
((invg‘𝐺)‘𝑧)) = (0g‘𝐺)) |
69 | 68 | oveq1d 6564 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 +
((invg‘𝐺)‘𝑧)) + (𝑢 +
((invg‘𝐺)‘𝑧))) = ((0g‘𝐺) + (𝑢 +
((invg‘𝐺)‘𝑧)))) |
70 | 5, 8 | grpass 17254 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑧 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝑧) ∈ 𝑋 ∧ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑋)) → ((𝑧 +
((invg‘𝐺)‘𝑧)) + (𝑢 +
((invg‘𝐺)‘𝑧))) = (𝑧 +
(((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))))) |
71 | 57, 66, 58, 61, 70 | syl13anc 1320 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 +
((invg‘𝐺)‘𝑧)) + (𝑢 +
((invg‘𝐺)‘𝑧))) = (𝑧 +
(((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))))) |
72 | 5, 8, 6 | grplid 17275 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑋) → ((0g‘𝐺) + (𝑢 +
((invg‘𝐺)‘𝑧))) = (𝑢 +
((invg‘𝐺)‘𝑧))) |
73 | 57, 61, 72 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐺) + (𝑢 +
((invg‘𝐺)‘𝑧))) = (𝑢 +
((invg‘𝐺)‘𝑧))) |
74 | 69, 71, 73 | 3eqtr3d 2652 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑧 +
(((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧)))) = (𝑢 +
((invg‘𝐺)‘𝑧))) |
75 | 74 | eleq1d 2672 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑧 +
(((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧)))) ∈ 𝑆 ↔ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑆)) |
76 | 5, 8 | grpass 17254 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝑧) ∈ 𝑋 ∧ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) + 𝑧) = (((invg‘𝐺)‘𝑧) + ((𝑢 +
((invg‘𝐺)‘𝑧)) + 𝑧))) |
77 | 57, 58, 61, 66, 76 | syl13anc 1320 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) + 𝑧) = (((invg‘𝐺)‘𝑧) + ((𝑢 +
((invg‘𝐺)‘𝑧)) + 𝑧))) |
78 | 5, 8 | grpass 17254 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝑧) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑢 +
((invg‘𝐺)‘𝑧)) + 𝑧) = (𝑢 +
(((invg‘𝐺)‘𝑧) + 𝑧))) |
79 | 57, 59, 58, 66, 78 | syl13anc 1320 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑢 +
((invg‘𝐺)‘𝑧)) + 𝑧) = (𝑢 +
(((invg‘𝐺)‘𝑧) + 𝑧))) |
80 | 5, 8, 6, 53 | grplinv 17291 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋) → (((invg‘𝐺)‘𝑧) + 𝑧) = (0g‘𝐺)) |
81 | 57, 66, 80 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((invg‘𝐺)‘𝑧) + 𝑧) = (0g‘𝐺)) |
82 | 81 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑢 +
(((invg‘𝐺)‘𝑧) + 𝑧)) = (𝑢 + (0g‘𝐺))) |
83 | 5, 8, 6 | grprid 17276 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋) → (𝑢 + (0g‘𝐺)) = 𝑢) |
84 | 57, 59, 83 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (𝑢 + (0g‘𝐺)) = 𝑢) |
85 | 79, 82, 84 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((𝑢 +
((invg‘𝐺)‘𝑧)) + 𝑧) = 𝑢) |
86 | 85 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((invg‘𝐺)‘𝑧) + ((𝑢 +
((invg‘𝐺)‘𝑧)) + 𝑧)) = (((invg‘𝐺)‘𝑧) + 𝑢)) |
87 | 77, 86 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) + 𝑧) = (((invg‘𝐺)‘𝑧) + 𝑢)) |
88 | 87 | eleq1d 2672 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → (((((invg‘𝐺)‘𝑧) + (𝑢 +
((invg‘𝐺)‘𝑧))) + 𝑧) ∈ 𝑆 ↔ (((invg‘𝐺)‘𝑧) + 𝑢) ∈ 𝑆)) |
89 | 65, 75, 88 | 3bitr3rd 298 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) ∧ 𝑢 ∈ 𝑋) → ((((invg‘𝐺)‘𝑧) + 𝑢) ∈ 𝑆 ↔ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑆)) |
90 | 89 | ralrimiva 2949 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) → ∀𝑢 ∈ 𝑋 ((((invg‘𝐺)‘𝑧) + 𝑢) ∈ 𝑆 ↔ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑆)) |
91 | 1 | elnmz 17456 |
. . . . 5
⊢
(((invg‘𝐺)‘𝑧) ∈ 𝑁 ↔ (((invg‘𝐺)‘𝑧) ∈ 𝑋 ∧ ∀𝑢 ∈ 𝑋 ((((invg‘𝐺)‘𝑧) + 𝑢) ∈ 𝑆 ↔ (𝑢 +
((invg‘𝐺)‘𝑧)) ∈ 𝑆))) |
92 | 55, 90, 91 | sylanbrc 695 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) → ((invg‘𝐺)‘𝑧) ∈ 𝑁) |
93 | 52, 92 | jca 553 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑁) → (∀𝑤 ∈ 𝑁 (𝑧 + 𝑤) ∈ 𝑁 ∧ ((invg‘𝐺)‘𝑧) ∈ 𝑁)) |
94 | 93 | ralrimiva 2949 |
. 2
⊢ (𝐺 ∈ Grp → ∀𝑧 ∈ 𝑁 (∀𝑤 ∈ 𝑁 (𝑧 + 𝑤) ∈ 𝑁 ∧ ((invg‘𝐺)‘𝑧) ∈ 𝑁)) |
95 | 5, 8, 53 | issubg2 17432 |
. 2
⊢ (𝐺 ∈ Grp → (𝑁 ∈ (SubGrp‘𝐺) ↔ (𝑁 ⊆ 𝑋 ∧ 𝑁 ≠ ∅ ∧ ∀𝑧 ∈ 𝑁 (∀𝑤 ∈ 𝑁 (𝑧 + 𝑤) ∈ 𝑁 ∧ ((invg‘𝐺)‘𝑧) ∈ 𝑁)))) |
96 | 4, 17, 94, 95 | mpbir3and 1238 |
1
⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺)) |