| Step | Hyp | Ref
| Expression |
| 1 | | cycsubm.c |
. . 3
⊢ 𝐶 = ran 𝐹 |
| 2 | | cycsubm.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
| 3 | | cycsubm.t |
. . . . . . . 8
⊢ · =
(.g‘𝐺) |
| 4 | 2, 3 | mulgnn0cl 19108 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ ℕ0
∧ 𝐴 ∈ 𝐵) → (𝑥 · 𝐴) ∈ 𝐵) |
| 5 | 4 | 3expa 1119 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑥 ∈ ℕ0)
∧ 𝐴 ∈ 𝐵) → (𝑥 · 𝐴) ∈ 𝐵) |
| 6 | 5 | an32s 652 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ ℕ0) → (𝑥 · 𝐴) ∈ 𝐵) |
| 7 | | cycsubm.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴)) |
| 8 | 6, 7 | fmptd 7134 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → 𝐹:ℕ0⟶𝐵) |
| 9 | 8 | frnd 6744 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → ran 𝐹 ⊆ 𝐵) |
| 10 | 1, 9 | eqsstrid 4022 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → 𝐶 ⊆ 𝐵) |
| 11 | | 0nn0 12541 |
. . . . 5
⊢ 0 ∈
ℕ0 |
| 12 | 11 | a1i 11 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → 0 ∈
ℕ0) |
| 13 | | oveq1 7438 |
. . . . . 6
⊢ (𝑖 = 0 → (𝑖 · 𝐴) = (0 · 𝐴)) |
| 14 | 13 | eqeq2d 2748 |
. . . . 5
⊢ (𝑖 = 0 →
((0g‘𝐺) =
(𝑖 · 𝐴) ↔ (0g‘𝐺) = (0 · 𝐴))) |
| 15 | 14 | adantl 481 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ 𝑖 = 0) → ((0g‘𝐺) = (𝑖 · 𝐴) ↔ (0g‘𝐺) = (0 · 𝐴))) |
| 16 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 17 | 2, 16, 3 | mulg0 19092 |
. . . . . 6
⊢ (𝐴 ∈ 𝐵 → (0 · 𝐴) = (0g‘𝐺)) |
| 18 | 17 | adantl 481 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → (0 · 𝐴) = (0g‘𝐺)) |
| 19 | 18 | eqcomd 2743 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → (0g‘𝐺) = (0 · 𝐴)) |
| 20 | 12, 15, 19 | rspcedvd 3624 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → ∃𝑖 ∈ ℕ0
(0g‘𝐺) =
(𝑖 · 𝐴)) |
| 21 | 2, 3, 7, 1 | cycsubmel 19218 |
. . 3
⊢
((0g‘𝐺) ∈ 𝐶 ↔ ∃𝑖 ∈ ℕ0
(0g‘𝐺) =
(𝑖 · 𝐴)) |
| 22 | 20, 21 | sylibr 234 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → (0g‘𝐺) ∈ 𝐶) |
| 23 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
→ 𝑖 ∈
ℕ0) |
| 24 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
→ 𝑗 ∈
ℕ0) |
| 25 | 23, 24 | nn0addcld 12591 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
→ (𝑖 + 𝑗) ∈
ℕ0) |
| 26 | 25 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝐺 ∈ Mnd
∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝑏 = (𝑗 · 𝐴) ∧ 𝑎 = (𝑖 · 𝐴))) → (𝑖 + 𝑗) ∈
ℕ0) |
| 27 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑖 + 𝑗) → (𝑘 · 𝐴) = ((𝑖 + 𝑗) · 𝐴)) |
| 28 | 27 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑖 + 𝑗) → ((𝑎(+g‘𝐺)𝑏) = (𝑘 · 𝐴) ↔ (𝑎(+g‘𝐺)𝑏) = ((𝑖 + 𝑗) · 𝐴))) |
| 29 | 28 | adantl 481 |
. . . . . . . . . 10
⊢
((((((𝐺 ∈ Mnd
∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝑏 = (𝑗 · 𝐴) ∧ 𝑎 = (𝑖 · 𝐴))) ∧ 𝑘 = (𝑖 + 𝑗)) → ((𝑎(+g‘𝐺)𝑏) = (𝑘 · 𝐴) ↔ (𝑎(+g‘𝐺)𝑏) = ((𝑖 + 𝑗) · 𝐴))) |
| 30 | | oveq12 7440 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑖 · 𝐴) ∧ 𝑏 = (𝑗 · 𝐴)) → (𝑎(+g‘𝐺)𝑏) = ((𝑖 · 𝐴)(+g‘𝐺)(𝑗 · 𝐴))) |
| 31 | 30 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝑏 = (𝑗 · 𝐴) ∧ 𝑎 = (𝑖 · 𝐴)) → (𝑎(+g‘𝐺)𝑏) = ((𝑖 · 𝐴)(+g‘𝐺)(𝑗 · 𝐴))) |
| 32 | | simplll 775 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
→ 𝐺 ∈
Mnd) |
| 33 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
→ 𝐴 ∈ 𝐵) |
| 34 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 35 | 2, 3, 34 | mulgnn0dir 19122 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Mnd ∧ (𝑖 ∈ ℕ0
∧ 𝑗 ∈
ℕ0 ∧ 𝐴
∈ 𝐵)) → ((𝑖 + 𝑗) · 𝐴) = ((𝑖 · 𝐴)(+g‘𝐺)(𝑗 · 𝐴))) |
| 36 | 32, 23, 24, 33, 35 | syl13anc 1374 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
→ ((𝑖 + 𝑗) · 𝐴) = ((𝑖 · 𝐴)(+g‘𝐺)(𝑗 · 𝐴))) |
| 37 | 36 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
→ ((𝑖 · 𝐴)(+g‘𝐺)(𝑗 · 𝐴)) = ((𝑖 + 𝑗) · 𝐴)) |
| 38 | 31, 37 | sylan9eqr 2799 |
. . . . . . . . . 10
⊢
(((((𝐺 ∈ Mnd
∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝑏 = (𝑗 · 𝐴) ∧ 𝑎 = (𝑖 · 𝐴))) → (𝑎(+g‘𝐺)𝑏) = ((𝑖 + 𝑗) · 𝐴)) |
| 39 | 26, 29, 38 | rspcedvd 3624 |
. . . . . . . . 9
⊢
(((((𝐺 ∈ Mnd
∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝑏 = (𝑗 · 𝐴) ∧ 𝑎 = (𝑖 · 𝐴))) → ∃𝑘 ∈ ℕ0 (𝑎(+g‘𝐺)𝑏) = (𝑘 · 𝐴)) |
| 40 | 39 | exp32 420 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
→ (𝑏 = (𝑗 · 𝐴) → (𝑎 = (𝑖 · 𝐴) → ∃𝑘 ∈ ℕ0 (𝑎(+g‘𝐺)𝑏) = (𝑘 · 𝐴)))) |
| 41 | 40 | rexlimdva 3155 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) →
(∃𝑗 ∈
ℕ0 𝑏 =
(𝑗 · 𝐴) → (𝑎 = (𝑖 · 𝐴) → ∃𝑘 ∈ ℕ0 (𝑎(+g‘𝐺)𝑏) = (𝑘 · 𝐴)))) |
| 42 | 41 | com23 86 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑎 = (𝑖 · 𝐴) → (∃𝑗 ∈ ℕ0 𝑏 = (𝑗 · 𝐴) → ∃𝑘 ∈ ℕ0 (𝑎(+g‘𝐺)𝑏) = (𝑘 · 𝐴)))) |
| 43 | 42 | rexlimdva 3155 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → (∃𝑖 ∈ ℕ0 𝑎 = (𝑖 · 𝐴) → (∃𝑗 ∈ ℕ0 𝑏 = (𝑗 · 𝐴) → ∃𝑘 ∈ ℕ0 (𝑎(+g‘𝐺)𝑏) = (𝑘 · 𝐴)))) |
| 44 | 43 | impd 410 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → ((∃𝑖 ∈ ℕ0 𝑎 = (𝑖 · 𝐴) ∧ ∃𝑗 ∈ ℕ0 𝑏 = (𝑗 · 𝐴)) → ∃𝑘 ∈ ℕ0 (𝑎(+g‘𝐺)𝑏) = (𝑘 · 𝐴))) |
| 45 | 2, 3, 7, 1 | cycsubmel 19218 |
. . . . 5
⊢ (𝑎 ∈ 𝐶 ↔ ∃𝑖 ∈ ℕ0 𝑎 = (𝑖 · 𝐴)) |
| 46 | 2, 3, 7, 1 | cycsubmel 19218 |
. . . . 5
⊢ (𝑏 ∈ 𝐶 ↔ ∃𝑗 ∈ ℕ0 𝑏 = (𝑗 · 𝐴)) |
| 47 | 45, 46 | anbi12i 628 |
. . . 4
⊢ ((𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶) ↔ (∃𝑖 ∈ ℕ0 𝑎 = (𝑖 · 𝐴) ∧ ∃𝑗 ∈ ℕ0 𝑏 = (𝑗 · 𝐴))) |
| 48 | 2, 3, 7, 1 | cycsubmel 19218 |
. . . 4
⊢ ((𝑎(+g‘𝐺)𝑏) ∈ 𝐶 ↔ ∃𝑘 ∈ ℕ0 (𝑎(+g‘𝐺)𝑏) = (𝑘 · 𝐴)) |
| 49 | 44, 47, 48 | 3imtr4g 296 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → ((𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶) → (𝑎(+g‘𝐺)𝑏) ∈ 𝐶)) |
| 50 | 49 | ralrimivv 3200 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎(+g‘𝐺)𝑏) ∈ 𝐶) |
| 51 | 2, 16, 34 | issubm 18816 |
. . 3
⊢ (𝐺 ∈ Mnd → (𝐶 ∈ (SubMnd‘𝐺) ↔ (𝐶 ⊆ 𝐵 ∧ (0g‘𝐺) ∈ 𝐶 ∧ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎(+g‘𝐺)𝑏) ∈ 𝐶))) |
| 52 | 51 | adantr 480 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → (𝐶 ∈ (SubMnd‘𝐺) ↔ (𝐶 ⊆ 𝐵 ∧ (0g‘𝐺) ∈ 𝐶 ∧ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐶 (𝑎(+g‘𝐺)𝑏) ∈ 𝐶))) |
| 53 | 10, 22, 50, 52 | mpbir3and 1343 |
1
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → 𝐶 ∈ (SubMnd‘𝐺)) |