This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ismgmd

Description: Deduce a magma from its properties. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses ismgmd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
ismgmd.0 ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
ismgmd.p ⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
ismgmd.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
Assertion ismgmd ( 𝜑 → 𝐺 ∈ Mgm )

Proof

Step Hyp Ref Expression
1 ismgmd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
2 ismgmd.0 ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
3 ismgmd.p ⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
4 ismgmd.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
5 4 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
6 5 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) ∈ 𝐵 )
7 3 oveqd ⊢ ( 𝜑 → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
8 7 1 eleq12d ⊢ ( 𝜑 → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ↔ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ) )
9 1 8 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) ∈ 𝐵 ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ) )
10 1 9 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ) )
11 6 10 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
12 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
13 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
14 12 13 ismgm ⊢ ( 𝐺 ∈ 𝑉 → ( 𝐺 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ) )
15 2 14 syl ⊢ ( 𝜑 → ( 𝐺 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ) )
16 11 15 mpbird ⊢ ( 𝜑 → 𝐺 ∈ Mgm )