Step |
Hyp |
Ref |
Expression |
1 |
|
simpgnideld.1 |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
simpgnideld.2 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
3 |
|
simpgnideld.3 |
⊢ ( 𝜑 → 𝐺 ∈ SimpGrp ) |
4 |
1 2 3
|
simpgntrivd |
⊢ ( 𝜑 → ¬ 𝐵 = { 0 } ) |
5 |
3
|
simpggrpd |
⊢ ( 𝜑 → 𝐺 ∈ Grp ) |
6 |
|
grpmnd |
⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd ) |
7 |
1 2
|
mndidcl |
⊢ ( 𝐺 ∈ Mnd → 0 ∈ 𝐵 ) |
8 |
5 6 7
|
3syl |
⊢ ( 𝜑 → 0 ∈ 𝐵 ) |
9 |
8
|
ne0d |
⊢ ( 𝜑 → 𝐵 ≠ ∅ ) |
10 |
|
eqsn |
⊢ ( 𝐵 ≠ ∅ → ( 𝐵 = { 0 } ↔ ∀ 𝑥 ∈ 𝐵 𝑥 = 0 ) ) |
11 |
9 10
|
syl |
⊢ ( 𝜑 → ( 𝐵 = { 0 } ↔ ∀ 𝑥 ∈ 𝐵 𝑥 = 0 ) ) |
12 |
4 11
|
mtbid |
⊢ ( 𝜑 → ¬ ∀ 𝑥 ∈ 𝐵 𝑥 = 0 ) |
13 |
|
rexnal |
⊢ ( ∃ 𝑥 ∈ 𝐵 ¬ 𝑥 = 0 ↔ ¬ ∀ 𝑥 ∈ 𝐵 𝑥 = 0 ) |
14 |
12 13
|
sylibr |
⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ¬ 𝑥 = 0 ) |