Step |
Hyp |
Ref |
Expression |
1 |
|
ismgmid.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
ismgmid.o |
⊢ 0 = ( 0g ‘ 𝐺 ) |
3 |
|
ismgmid.p |
⊢ + = ( +g ‘ 𝐺 ) |
4 |
|
mgmidcl.e |
⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) |
5 |
|
id |
⊢ ( 𝑈 ∈ 𝐵 → 𝑈 ∈ 𝐵 ) |
6 |
|
mgmidmo |
⊢ ∃* 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) |
7 |
|
reu5 |
⊢ ( ∃! 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ( ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ∧ ∃* 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ) |
8 |
4 6 7
|
sylanblrc |
⊢ ( 𝜑 → ∃! 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) |
9 |
|
oveq1 |
⊢ ( 𝑒 = 𝑈 → ( 𝑒 + 𝑥 ) = ( 𝑈 + 𝑥 ) ) |
10 |
9
|
eqeq1d |
⊢ ( 𝑒 = 𝑈 → ( ( 𝑒 + 𝑥 ) = 𝑥 ↔ ( 𝑈 + 𝑥 ) = 𝑥 ) ) |
11 |
10
|
ovanraleqv |
⊢ ( 𝑒 = 𝑈 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ) ) |
12 |
11
|
riota2 |
⊢ ( ( 𝑈 ∈ 𝐵 ∧ ∃! 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ↔ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ) ) |
13 |
5 8 12
|
syl2anr |
⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ↔ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ) ) |
14 |
13
|
pm5.32da |
⊢ ( 𝜑 → ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ) ↔ ( 𝑈 ∈ 𝐵 ∧ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ) ) ) |
15 |
|
riotacl |
⊢ ( ∃! 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) → ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ∈ 𝐵 ) |
16 |
8 15
|
syl |
⊢ ( 𝜑 → ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ∈ 𝐵 ) |
17 |
|
eleq1 |
⊢ ( ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 → ( ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ∈ 𝐵 ↔ 𝑈 ∈ 𝐵 ) ) |
18 |
16 17
|
syl5ibcom |
⊢ ( 𝜑 → ( ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 → 𝑈 ∈ 𝐵 ) ) |
19 |
18
|
pm4.71rd |
⊢ ( 𝜑 → ( ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ↔ ( 𝑈 ∈ 𝐵 ∧ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ) ) ) |
20 |
|
df-riota |
⊢ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = ( ℩ 𝑒 ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ) |
21 |
1 3 2
|
grpidval |
⊢ 0 = ( ℩ 𝑒 ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ) |
22 |
20 21
|
eqtr4i |
⊢ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 0 |
23 |
22
|
eqeq1i |
⊢ ( ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ↔ 0 = 𝑈 ) |
24 |
23
|
a1i |
⊢ ( 𝜑 → ( ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = 𝑈 ↔ 0 = 𝑈 ) ) |
25 |
14 19 24
|
3bitr2d |
⊢ ( 𝜑 → ( ( 𝑈 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑈 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑈 ) = 𝑥 ) ) ↔ 0 = 𝑈 ) ) |