Theorem mgm2mgm

Description: Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020)

	Ref	Expression
Assertion	mgm2mgm	⊢ ( 𝑀 ∈ MgmALT ↔ 𝑀 ∈ Mgm )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
2		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
3	1 2	ismgmALT	⊢ ( 𝑀 ∈ MgmALT → ( 𝑀 ∈ MgmALT ↔ ( +g ‘ 𝑀 ) clLaw ( Base ‘ 𝑀 ) ) )
4		fvex	⊢ ( +g ‘ 𝑀 ) ∈ V
5		fvex	⊢ ( Base ‘ 𝑀 ) ∈ V
6		iscllaw	⊢ ( ( ( +g ‘ 𝑀 ) ∈ V ∧ ( Base ‘ 𝑀 ) ∈ V ) → ( ( +g ‘ 𝑀 ) clLaw ( Base ‘ 𝑀 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) )
7	4 5 6	mp2an	⊢ ( ( +g ‘ 𝑀 ) clLaw ( Base ‘ 𝑀 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
8	1 2	ismgm	⊢ ( 𝑀 ∈ MgmALT → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) )
9	8	biimprd	⊢ ( 𝑀 ∈ MgmALT → ( ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) → 𝑀 ∈ Mgm ) )
10	7 9	syl5bi	⊢ ( 𝑀 ∈ MgmALT → ( ( +g ‘ 𝑀 ) clLaw ( Base ‘ 𝑀 ) → 𝑀 ∈ Mgm ) )
11	3 10	sylbid	⊢ ( 𝑀 ∈ MgmALT → ( 𝑀 ∈ MgmALT → 𝑀 ∈ Mgm ) )
12	11	pm2.43i	⊢ ( 𝑀 ∈ MgmALT → 𝑀 ∈ Mgm )
13		mgmplusgiopALT	⊢ ( 𝑀 ∈ Mgm → ( +g ‘ 𝑀 ) clLaw ( Base ‘ 𝑀 ) )
14	1 2	ismgmALT	⊢ ( 𝑀 ∈ Mgm → ( 𝑀 ∈ MgmALT ↔ ( +g ‘ 𝑀 ) clLaw ( Base ‘ 𝑀 ) ) )
15	13 14	mpbird	⊢ ( 𝑀 ∈ Mgm → 𝑀 ∈ MgmALT )
16	12 15	impbii	⊢ ( 𝑀 ∈ MgmALT ↔ 𝑀 ∈ Mgm )