Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) |
2 |
|
eqid |
⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 ) |
3 |
1 2
|
mgmcl |
⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) |
4 |
3
|
3expb |
⊢ ( ( 𝑀 ∈ Mgm ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) |
5 |
4
|
ralrimivva |
⊢ ( 𝑀 ∈ Mgm → ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) |
6 |
|
fvex |
⊢ ( +g ‘ 𝑀 ) ∈ V |
7 |
|
fvex |
⊢ ( Base ‘ 𝑀 ) ∈ V |
8 |
6 7
|
pm3.2i |
⊢ ( ( +g ‘ 𝑀 ) ∈ V ∧ ( Base ‘ 𝑀 ) ∈ V ) |
9 |
|
iscllaw |
⊢ ( ( ( +g ‘ 𝑀 ) ∈ V ∧ ( Base ‘ 𝑀 ) ∈ V ) → ( ( +g ‘ 𝑀 ) clLaw ( Base ‘ 𝑀 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) ) |
10 |
8 9
|
mp1i |
⊢ ( 𝑀 ∈ Mgm → ( ( +g ‘ 𝑀 ) clLaw ( Base ‘ 𝑀 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) ) |
11 |
5 10
|
mpbird |
⊢ ( 𝑀 ∈ Mgm → ( +g ‘ 𝑀 ) clLaw ( Base ‘ 𝑀 ) ) |