Step |
Hyp |
Ref |
Expression |
1 |
|
simpgnsgbid.1 |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
simpgnsgbid.2 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
3 |
|
simpgnsgbid.3 |
⊢ ( 𝜑 → 𝐺 ∈ Grp ) |
4 |
|
simpgnsgbid.4 |
⊢ ( 𝜑 → ¬ { 0 } = 𝐵 ) |
5 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝐺 ∈ SimpGrp ) → 𝐺 ∈ SimpGrp ) |
6 |
1 2 5
|
simpgnsgd |
⊢ ( ( 𝜑 ∧ 𝐺 ∈ SimpGrp ) → ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) |
7 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) → 𝐺 ∈ Grp ) |
8 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) → ¬ { 0 } = 𝐵 ) |
9 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) |
10 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) |
11 |
9 10
|
eleqtrd |
⊢ ( ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝑥 ∈ { { 0 } , 𝐵 } ) |
12 |
|
elpri |
⊢ ( 𝑥 ∈ { { 0 } , 𝐵 } → ( 𝑥 = { 0 } ∨ 𝑥 = 𝐵 ) ) |
13 |
11 12
|
syl |
⊢ ( ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝑥 = { 0 } ∨ 𝑥 = 𝐵 ) ) |
14 |
1 2 7 8 13
|
2nsgsimpgd |
⊢ ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) → 𝐺 ∈ SimpGrp ) |
15 |
6 14
|
impbida |
⊢ ( 𝜑 → ( 𝐺 ∈ SimpGrp ↔ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) ) |