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 )