Step |
Hyp |
Ref |
Expression |
1 |
|
ismgmid.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
ismgmid.o |
⊢ 0 = ( 0g ‘ 𝐺 ) |
3 |
|
ismgmid.p |
⊢ + = ( +g ‘ 𝐺 ) |
4 |
|
mgmidcl.e |
⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) |
5 |
|
eqid |
⊢ 0 = 0 |
6 |
1 2 3 4
|
ismgmid |
⊢ ( 𝜑 → ( ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) ↔ 0 = 0 ) ) |
7 |
5 6
|
mpbiri |
⊢ ( 𝜑 → ( 0 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) ) |
8 |
7
|
simprd |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) |
9 |
|
oveq2 |
⊢ ( 𝑥 = 𝑋 → ( 0 + 𝑥 ) = ( 0 + 𝑋 ) ) |
10 |
|
id |
⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 ) |
11 |
9 10
|
eqeq12d |
⊢ ( 𝑥 = 𝑋 → ( ( 0 + 𝑥 ) = 𝑥 ↔ ( 0 + 𝑋 ) = 𝑋 ) ) |
12 |
|
oveq1 |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 + 0 ) = ( 𝑋 + 0 ) ) |
13 |
12 10
|
eqeq12d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 + 0 ) = 𝑥 ↔ ( 𝑋 + 0 ) = 𝑋 ) ) |
14 |
11 13
|
anbi12d |
⊢ ( 𝑥 = 𝑋 → ( ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ↔ ( ( 0 + 𝑋 ) = 𝑋 ∧ ( 𝑋 + 0 ) = 𝑋 ) ) ) |
15 |
14
|
rspccva |
⊢ ( ( ∀ 𝑥 ∈ 𝐵 ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 + 𝑋 ) = 𝑋 ∧ ( 𝑋 + 0 ) = 𝑋 ) ) |
16 |
8 15
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 + 𝑋 ) = 𝑋 ∧ ( 𝑋 + 0 ) = 𝑋 ) ) |