Proof of Theorem subgmulg
| Step | Hyp | Ref
| Expression |
| 1 | | subgmulg.h |
. . . . . 6
⊢ 𝐻 = (𝐺 ↾s 𝑆) |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 3 | 1, 2 | subg0 19150 |
. . . . 5
⊢ (𝑆 ∈ (SubGrp‘𝐺) →
(0g‘𝐺) =
(0g‘𝐻)) |
| 4 | 3 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (0g‘𝐺) = (0g‘𝐻)) |
| 5 | 4 | ifeq1d 4545 |
. . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → if(𝑁 = 0, (0g‘𝐺), if(0 < 𝑁, (seq1((+g‘𝐺), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁)))) = if(𝑁 = 0, (0g‘𝐻), if(0 < 𝑁, (seq1((+g‘𝐺), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁))))) |
| 6 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 7 | 1, 6 | ressplusg 17334 |
. . . . . . . . . 10
⊢ (𝑆 ∈ (SubGrp‘𝐺) →
(+g‘𝐺) =
(+g‘𝐻)) |
| 8 | 7 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (+g‘𝐺) = (+g‘𝐻)) |
| 9 | 8 | seqeq2d 14049 |
. . . . . . . 8
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → seq1((+g‘𝐺), (ℕ × {𝑋})) =
seq1((+g‘𝐻), (ℕ × {𝑋}))) |
| 10 | 9 | adantr 480 |
. . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ ¬ 𝑁 = 0) → seq1((+g‘𝐺), (ℕ × {𝑋})) =
seq1((+g‘𝐻), (ℕ × {𝑋}))) |
| 11 | 10 | fveq1d 6908 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ ¬ 𝑁 = 0) →
(seq1((+g‘𝐺), (ℕ × {𝑋}))‘𝑁) = (seq1((+g‘𝐻), (ℕ × {𝑋}))‘𝑁)) |
| 12 | 11 | ifeq1d 4545 |
. . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ ¬ 𝑁 = 0) → if(0 < 𝑁, (seq1((+g‘𝐺), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁))) = if(0 < 𝑁, (seq1((+g‘𝐻), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁)))) |
| 13 | | simp2 1138 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → 𝑁 ∈ ℤ) |
| 14 | 13 | zred 12722 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → 𝑁 ∈ ℝ) |
| 15 | | 0re 11263 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
| 16 | | axlttri 11332 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 0 ∈
ℝ) → (𝑁 < 0
↔ ¬ (𝑁 = 0 ∨ 0
< 𝑁))) |
| 17 | 14, 15, 16 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 < 0 ↔ ¬ (𝑁 = 0 ∨ 0 < 𝑁))) |
| 18 | | ioran 986 |
. . . . . . . . . . 11
⊢ (¬
(𝑁 = 0 ∨ 0 < 𝑁) ↔ (¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁)) |
| 19 | 17, 18 | bitrdi 287 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 < 0 ↔ (¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁))) |
| 20 | 19 | biimpar 477 |
. . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ (¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁)) → 𝑁 < 0) |
| 21 | | simpl1 1192 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ 𝑁 < 0) → 𝑆 ∈ (SubGrp‘𝐺)) |
| 22 | 13 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ 𝑁 < 0) → 𝑁 ∈ ℤ) |
| 23 | 22 | znegcld 12724 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ 𝑁 < 0) → -𝑁 ∈ ℤ) |
| 24 | 14 | lt0neg1d 11832 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 < 0 ↔ 0 < -𝑁)) |
| 25 | 24 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ 𝑁 < 0) → 0 < -𝑁) |
| 26 | | elnnz 12623 |
. . . . . . . . . . . . 13
⊢ (-𝑁 ∈ ℕ ↔ (-𝑁 ∈ ℤ ∧ 0 <
-𝑁)) |
| 27 | 23, 25, 26 | sylanbrc 583 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ 𝑁 < 0) → -𝑁 ∈ ℕ) |
| 28 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 29 | 28 | subgss 19145 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) |
| 30 | 29 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ (Base‘𝐺)) |
| 31 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆) |
| 32 | 30, 31 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ (Base‘𝐺)) |
| 33 | 32 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ 𝑁 < 0) → 𝑋 ∈ (Base‘𝐺)) |
| 34 | | subgmulgcl.t |
. . . . . . . . . . . . 13
⊢ · =
(.g‘𝐺) |
| 35 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
seq1((+g‘𝐺), (ℕ × {𝑋})) = seq1((+g‘𝐺), (ℕ × {𝑋})) |
| 36 | 28, 6, 34, 35 | mulgnn 19093 |
. . . . . . . . . . . 12
⊢ ((-𝑁 ∈ ℕ ∧ 𝑋 ∈ (Base‘𝐺)) → (-𝑁 · 𝑋) = (seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁)) |
| 37 | 27, 33, 36 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ 𝑁 < 0) → (-𝑁 · 𝑋) = (seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁)) |
| 38 | 31 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ 𝑁 < 0) → 𝑋 ∈ 𝑆) |
| 39 | 34 | subgmulgcl 19157 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ -𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (-𝑁 · 𝑋) ∈ 𝑆) |
| 40 | 21, 23, 38, 39 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ 𝑁 < 0) → (-𝑁 · 𝑋) ∈ 𝑆) |
| 41 | 37, 40 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ 𝑁 < 0) →
(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁) ∈ 𝑆) |
| 42 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 43 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(invg‘𝐻) = (invg‘𝐻) |
| 44 | 1, 42, 43 | subginv 19151 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧
(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁) ∈ 𝑆) → ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁)) = ((invg‘𝐻)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁))) |
| 45 | 21, 41, 44 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ 𝑁 < 0) →
((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁)) = ((invg‘𝐻)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁))) |
| 46 | 20, 45 | syldan 591 |
. . . . . . . 8
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ (¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁)) → ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁)) = ((invg‘𝐻)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁))) |
| 47 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ (¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁)) → seq1((+g‘𝐺), (ℕ × {𝑋})) =
seq1((+g‘𝐻), (ℕ × {𝑋}))) |
| 48 | 47 | fveq1d 6908 |
. . . . . . . . 9
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ (¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁)) → (seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁) = (seq1((+g‘𝐻), (ℕ × {𝑋}))‘-𝑁)) |
| 49 | 48 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ (¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁)) → ((invg‘𝐻)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁)) = ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑋}))‘-𝑁))) |
| 50 | 46, 49 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ (¬ 𝑁 = 0 ∧ ¬ 0 < 𝑁)) → ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁)) = ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑋}))‘-𝑁))) |
| 51 | 50 | anassrs 467 |
. . . . . 6
⊢ ((((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁)) = ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑋}))‘-𝑁))) |
| 52 | 51 | ifeq2da 4558 |
. . . . 5
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ ¬ 𝑁 = 0) → if(0 < 𝑁, (seq1((+g‘𝐻), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁))) = if(0 < 𝑁, (seq1((+g‘𝐻), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑋}))‘-𝑁)))) |
| 53 | 12, 52 | eqtrd 2777 |
. . . 4
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) ∧ ¬ 𝑁 = 0) → if(0 < 𝑁, (seq1((+g‘𝐺), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁))) = if(0 < 𝑁, (seq1((+g‘𝐻), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑋}))‘-𝑁)))) |
| 54 | 53 | ifeq2da 4558 |
. . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → if(𝑁 = 0, (0g‘𝐻), if(0 < 𝑁, (seq1((+g‘𝐺), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁)))) = if(𝑁 = 0, (0g‘𝐻), if(0 < 𝑁, (seq1((+g‘𝐻), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑋}))‘-𝑁))))) |
| 55 | 5, 54 | eqtrd 2777 |
. 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → if(𝑁 = 0, (0g‘𝐺), if(0 < 𝑁, (seq1((+g‘𝐺), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁)))) = if(𝑁 = 0, (0g‘𝐻), if(0 < 𝑁, (seq1((+g‘𝐻), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑋}))‘-𝑁))))) |
| 56 | 28, 6, 2, 42, 34, 35 | mulgval 19089 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ (Base‘𝐺)) → (𝑁 · 𝑋) = if(𝑁 = 0, (0g‘𝐺), if(0 < 𝑁, (seq1((+g‘𝐺), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁))))) |
| 57 | 13, 32, 56 | syl2anc 584 |
. 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) = if(𝑁 = 0, (0g‘𝐺), if(0 < 𝑁, (seq1((+g‘𝐺), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐺)‘(seq1((+g‘𝐺), (ℕ × {𝑋}))‘-𝑁))))) |
| 58 | 1 | subgbas 19148 |
. . . . 5
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘𝐻)) |
| 59 | 58 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → 𝑆 = (Base‘𝐻)) |
| 60 | 31, 59 | eleqtrd 2843 |
. . 3
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ (Base‘𝐻)) |
| 61 | | eqid 2737 |
. . . 4
⊢
(Base‘𝐻) =
(Base‘𝐻) |
| 62 | | eqid 2737 |
. . . 4
⊢
(+g‘𝐻) = (+g‘𝐻) |
| 63 | | eqid 2737 |
. . . 4
⊢
(0g‘𝐻) = (0g‘𝐻) |
| 64 | | subgmulg.t |
. . . 4
⊢ ∙ =
(.g‘𝐻) |
| 65 | | eqid 2737 |
. . . 4
⊢
seq1((+g‘𝐻), (ℕ × {𝑋})) = seq1((+g‘𝐻), (ℕ × {𝑋})) |
| 66 | 61, 62, 63, 43, 64, 65 | mulgval 19089 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ (Base‘𝐻)) → (𝑁 ∙ 𝑋) = if(𝑁 = 0, (0g‘𝐻), if(0 < 𝑁, (seq1((+g‘𝐻), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑋}))‘-𝑁))))) |
| 67 | 13, 60, 66 | syl2anc 584 |
. 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 ∙ 𝑋) = if(𝑁 = 0, (0g‘𝐻), if(0 < 𝑁, (seq1((+g‘𝐻), (ℕ × {𝑋}))‘𝑁), ((invg‘𝐻)‘(seq1((+g‘𝐻), (ℕ × {𝑋}))‘-𝑁))))) |
| 68 | 55, 57, 67 | 3eqtr4d 2787 |
1
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) = (𝑁 ∙ 𝑋)) |