| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sgrp1.m | . . 3
⊢ 𝑀 = {〈(Base‘ndx),
{𝐼}〉,
〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} | 
| 2 | 1 | mgm1 18671 | . 2
⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mgm) | 
| 3 |  | df-ov 7434 | . . . . . 6
⊢ (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = ({〈〈𝐼, 𝐼〉, 𝐼〉}‘〈𝐼, 𝐼〉) | 
| 4 |  | opex 5469 | . . . . . . 7
⊢
〈𝐼, 𝐼〉 ∈ V | 
| 5 |  | fvsng 7200 | . . . . . . 7
⊢
((〈𝐼, 𝐼〉 ∈ V ∧ 𝐼 ∈ 𝑉) → ({〈〈𝐼, 𝐼〉, 𝐼〉}‘〈𝐼, 𝐼〉) = 𝐼) | 
| 6 | 4, 5 | mpan 690 | . . . . . 6
⊢ (𝐼 ∈ 𝑉 → ({〈〈𝐼, 𝐼〉, 𝐼〉}‘〈𝐼, 𝐼〉) = 𝐼) | 
| 7 | 3, 6 | eqtrid 2789 | . . . . 5
⊢ (𝐼 ∈ 𝑉 → (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = 𝐼) | 
| 8 | 7 | oveq1d 7446 | . . . 4
⊢ (𝐼 ∈ 𝑉 → ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼)) | 
| 9 | 7 | oveq2d 7447 | . . . 4
⊢ (𝐼 ∈ 𝑉 → (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼)) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼)) | 
| 10 | 8, 9 | eqtr4d 2780 | . . 3
⊢ (𝐼 ∈ 𝑉 → ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼))) | 
| 11 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝑥 = 𝐼 → (𝑥{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦)) | 
| 12 | 11 | oveq1d 7446 | . . . . . . 7
⊢ (𝑥 = 𝐼 → ((𝑥{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) | 
| 13 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑥 = 𝐼 → (𝑥{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧))) | 
| 14 | 12, 13 | eqeq12d 2753 | . . . . . 6
⊢ (𝑥 = 𝐼 → (((𝑥{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝑥{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) ↔ ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)))) | 
| 15 | 14 | 2ralbidv 3221 | . . . . 5
⊢ (𝑥 = 𝐼 → (∀𝑦 ∈ {𝐼}∀𝑧 ∈ {𝐼} ((𝑥{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝑥{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) ↔ ∀𝑦 ∈ {𝐼}∀𝑧 ∈ {𝐼} ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)))) | 
| 16 | 15 | ralsng 4675 | . . . 4
⊢ (𝐼 ∈ 𝑉 → (∀𝑥 ∈ {𝐼}∀𝑦 ∈ {𝐼}∀𝑧 ∈ {𝐼} ((𝑥{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝑥{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) ↔ ∀𝑦 ∈ {𝐼}∀𝑧 ∈ {𝐼} ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)))) | 
| 17 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑦 = 𝐼 → (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼)) | 
| 18 | 17 | oveq1d 7446 | . . . . . . 7
⊢ (𝑦 = 𝐼 → ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) | 
| 19 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝑦 = 𝐼 → (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) | 
| 20 | 19 | oveq2d 7447 | . . . . . . 7
⊢ (𝑦 = 𝐼 → (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧))) | 
| 21 | 18, 20 | eqeq12d 2753 | . . . . . 6
⊢ (𝑦 = 𝐼 → (((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) ↔ ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)))) | 
| 22 | 21 | ralbidv 3178 | . . . . 5
⊢ (𝑦 = 𝐼 → (∀𝑧 ∈ {𝐼} ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) ↔ ∀𝑧 ∈ {𝐼} ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)))) | 
| 23 | 22 | ralsng 4675 | . . . 4
⊢ (𝐼 ∈ 𝑉 → (∀𝑦 ∈ {𝐼}∀𝑧 ∈ {𝐼} ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) ↔ ∀𝑧 ∈ {𝐼} ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)))) | 
| 24 |  | oveq2 7439 | . . . . . 6
⊢ (𝑧 = 𝐼 → ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝐼)) | 
| 25 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑧 = 𝐼 → (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼)) | 
| 26 | 25 | oveq2d 7447 | . . . . . 6
⊢ (𝑧 = 𝐼 → (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼))) | 
| 27 | 24, 26 | eqeq12d 2753 | . . . . 5
⊢ (𝑧 = 𝐼 → (((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) ↔ ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼)))) | 
| 28 | 27 | ralsng 4675 | . . . 4
⊢ (𝐼 ∈ 𝑉 → (∀𝑧 ∈ {𝐼} ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) ↔ ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼)))) | 
| 29 | 16, 23, 28 | 3bitrd 305 | . . 3
⊢ (𝐼 ∈ 𝑉 → (∀𝑥 ∈ {𝐼}∀𝑦 ∈ {𝐼}∀𝑧 ∈ {𝐼} ((𝑥{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝑥{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)) ↔ ((𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼){〈〈𝐼, 𝐼〉, 𝐼〉}𝐼) = (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉} (𝐼{〈〈𝐼, 𝐼〉, 𝐼〉}𝐼)))) | 
| 30 | 10, 29 | mpbird 257 | . 2
⊢ (𝐼 ∈ 𝑉 → ∀𝑥 ∈ {𝐼}∀𝑦 ∈ {𝐼}∀𝑧 ∈ {𝐼} ((𝑥{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝑥{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧))) | 
| 31 |  | snex 5436 | . . . 4
⊢ {𝐼} ∈ V | 
| 32 | 1 | grpbase 17330 | . . . 4
⊢ ({𝐼} ∈ V → {𝐼} = (Base‘𝑀)) | 
| 33 | 31, 32 | ax-mp 5 | . . 3
⊢ {𝐼} = (Base‘𝑀) | 
| 34 |  | snex 5436 | . . . 4
⊢
{〈〈𝐼,
𝐼〉, 𝐼〉} ∈ V | 
| 35 | 1 | grpplusg 17332 | . . . 4
⊢
({〈〈𝐼,
𝐼〉, 𝐼〉} ∈ V → {〈〈𝐼, 𝐼〉, 𝐼〉} = (+g‘𝑀)) | 
| 36 | 34, 35 | ax-mp 5 | . . 3
⊢
{〈〈𝐼,
𝐼〉, 𝐼〉} = (+g‘𝑀) | 
| 37 | 33, 36 | issgrp 18733 | . 2
⊢ (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥 ∈ {𝐼}∀𝑦 ∈ {𝐼}∀𝑧 ∈ {𝐼} ((𝑥{〈〈𝐼, 𝐼〉, 𝐼〉}𝑦){〈〈𝐼, 𝐼〉, 𝐼〉}𝑧) = (𝑥{〈〈𝐼, 𝐼〉, 𝐼〉} (𝑦{〈〈𝐼, 𝐼〉, 𝐼〉}𝑧)))) | 
| 38 | 2, 30, 37 | sylanbrc 583 | 1
⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Smgrp) |