| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → 𝜑) | 
| 2 |  | mgmpropd.k | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) | 
| 3 | 2 | eqcomd 2743 | . . . . . . . . . 10
⊢ (𝜑 → (Base‘𝐾) = 𝐵) | 
| 4 | 3 | eleq2d 2827 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↔ 𝑥 ∈ 𝐵)) | 
| 5 | 4 | biimpcd 249 | . . . . . . . 8
⊢ (𝑥 ∈ (Base‘𝐾) → (𝜑 → 𝑥 ∈ 𝐵)) | 
| 6 | 5 | adantr 480 | . . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝜑 → 𝑥 ∈ 𝐵)) | 
| 7 | 6 | impcom 407 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → 𝑥 ∈ 𝐵) | 
| 8 | 3 | eleq2d 2827 | . . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ (Base‘𝐾) ↔ 𝑦 ∈ 𝐵)) | 
| 9 | 8 | biimpd 229 | . . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (Base‘𝐾) → 𝑦 ∈ 𝐵)) | 
| 10 | 9 | adantld 490 | . . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑦 ∈ 𝐵)) | 
| 11 | 10 | imp 406 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → 𝑦 ∈ 𝐵) | 
| 12 |  | mgmpropd.p | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) | 
| 13 | 1, 7, 11, 12 | syl12anc 837 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) | 
| 14 | 13 | eleq1d 2826 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → ((𝑥(+g‘𝐾)𝑦) ∈ (Base‘𝐾) ↔ (𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐾))) | 
| 15 | 14 | 2ralbidva 3219 | . . 3
⊢ (𝜑 → (∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) ∈ (Base‘𝐾) ↔ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐾))) | 
| 16 |  | mgmpropd.l | . . . . 5
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) | 
| 17 | 2, 16 | eqtr3d 2779 | . . . 4
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) | 
| 18 | 17 | eleq2d 2827 | . . . . 5
⊢ (𝜑 → ((𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐾) ↔ (𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐿))) | 
| 19 | 17, 18 | raleqbidv 3346 | . . . 4
⊢ (𝜑 → (∀𝑦 ∈ (Base‘𝐾)(𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐾) ↔ ∀𝑦 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐿))) | 
| 20 | 17, 19 | raleqbidv 3346 | . . 3
⊢ (𝜑 → (∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐾) ↔ ∀𝑥 ∈ (Base‘𝐿)∀𝑦 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐿))) | 
| 21 | 15, 20 | bitrd 279 | . 2
⊢ (𝜑 → (∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) ∈ (Base‘𝐾) ↔ ∀𝑥 ∈ (Base‘𝐿)∀𝑦 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐿))) | 
| 22 |  | mgmpropd.b | . . 3
⊢ (𝜑 → 𝐵 ≠ ∅) | 
| 23 |  | n0 4353 | . . . 4
⊢ (𝐵 ≠ ∅ ↔
∃𝑎 𝑎 ∈ 𝐵) | 
| 24 | 2 | eleq2d 2827 | . . . . . 6
⊢ (𝜑 → (𝑎 ∈ 𝐵 ↔ 𝑎 ∈ (Base‘𝐾))) | 
| 25 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 26 |  | eqid 2737 | . . . . . . 7
⊢
(+g‘𝐾) = (+g‘𝐾) | 
| 27 | 25, 26 | ismgmn0 18655 | . . . . . 6
⊢ (𝑎 ∈ (Base‘𝐾) → (𝐾 ∈ Mgm ↔ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) ∈ (Base‘𝐾))) | 
| 28 | 24, 27 | biimtrdi 253 | . . . . 5
⊢ (𝜑 → (𝑎 ∈ 𝐵 → (𝐾 ∈ Mgm ↔ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) ∈ (Base‘𝐾)))) | 
| 29 | 28 | exlimdv 1933 | . . . 4
⊢ (𝜑 → (∃𝑎 𝑎 ∈ 𝐵 → (𝐾 ∈ Mgm ↔ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) ∈ (Base‘𝐾)))) | 
| 30 | 23, 29 | biimtrid 242 | . . 3
⊢ (𝜑 → (𝐵 ≠ ∅ → (𝐾 ∈ Mgm ↔ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) ∈ (Base‘𝐾)))) | 
| 31 | 22, 30 | mpd 15 | . 2
⊢ (𝜑 → (𝐾 ∈ Mgm ↔ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(+g‘𝐾)𝑦) ∈ (Base‘𝐾))) | 
| 32 | 16 | eleq2d 2827 | . . . . . 6
⊢ (𝜑 → (𝑎 ∈ 𝐵 ↔ 𝑎 ∈ (Base‘𝐿))) | 
| 33 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝐿) =
(Base‘𝐿) | 
| 34 |  | eqid 2737 | . . . . . . 7
⊢
(+g‘𝐿) = (+g‘𝐿) | 
| 35 | 33, 34 | ismgmn0 18655 | . . . . . 6
⊢ (𝑎 ∈ (Base‘𝐿) → (𝐿 ∈ Mgm ↔ ∀𝑥 ∈ (Base‘𝐿)∀𝑦 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐿))) | 
| 36 | 32, 35 | biimtrdi 253 | . . . . 5
⊢ (𝜑 → (𝑎 ∈ 𝐵 → (𝐿 ∈ Mgm ↔ ∀𝑥 ∈ (Base‘𝐿)∀𝑦 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐿)))) | 
| 37 | 36 | exlimdv 1933 | . . . 4
⊢ (𝜑 → (∃𝑎 𝑎 ∈ 𝐵 → (𝐿 ∈ Mgm ↔ ∀𝑥 ∈ (Base‘𝐿)∀𝑦 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐿)))) | 
| 38 | 23, 37 | biimtrid 242 | . . 3
⊢ (𝜑 → (𝐵 ≠ ∅ → (𝐿 ∈ Mgm ↔ ∀𝑥 ∈ (Base‘𝐿)∀𝑦 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐿)))) | 
| 39 | 22, 38 | mpd 15 | . 2
⊢ (𝜑 → (𝐿 ∈ Mgm ↔ ∀𝑥 ∈ (Base‘𝐿)∀𝑦 ∈ (Base‘𝐿)(𝑥(+g‘𝐿)𝑦) ∈ (Base‘𝐿))) | 
| 40 | 21, 31, 39 | 3bitr4d 311 | 1
⊢ (𝜑 → (𝐾 ∈ Mgm ↔ 𝐿 ∈ Mgm)) |