Theorem ismgm

Description: The predicate "is a magma". (Contributed by FL, 2-Nov-2009) (Revised by AV, 6-Jan-2020)

	Ref	Expression
Hypotheses	ismgm.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	ismgm.o	⊢ ⚬ = ( +g ‘ 𝑀 )
Assertion	ismgm	⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ismgm.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		ismgm.o	⊢ ⚬ = ( +g ‘ 𝑀 )
3		fvexd	⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) ∈ V )
4		fveq2	⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
5	4 1	eqtr4di	⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = 𝐵 )
6		fvexd	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑚 ) ∈ V )
7		fveq2	⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) = ( +g ‘ 𝑀 ) )
8	7	adantr	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑚 ) = ( +g ‘ 𝑀 ) )
9	8 2	eqtr4di	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑚 ) = ⚬ )
10		simplr	⊢ ( ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) ∧ 𝑜 = ⚬ ) → 𝑏 = 𝐵 )
11		oveq	⊢ ( 𝑜 = ⚬ → ( 𝑥 𝑜 𝑦 ) = ( 𝑥 ⚬ 𝑦 ) )
12	11	adantl	⊢ ( ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) ∧ 𝑜 = ⚬ ) → ( 𝑥 𝑜 𝑦 ) = ( 𝑥 ⚬ 𝑦 ) )
13	12 10	eleq12d	⊢ ( ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) ∧ 𝑜 = ⚬ ) → ( ( 𝑥 𝑜 𝑦 ) ∈ 𝑏 ↔ ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) )
14	10 13	raleqbidv	⊢ ( ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) ∧ 𝑜 = ⚬ ) → ( ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑜 𝑦 ) ∈ 𝑏 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) )
15	10 14	raleqbidv	⊢ ( ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) ∧ 𝑜 = ⚬ ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑜 𝑦 ) ∈ 𝑏 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) )
16	6 9 15	sbcied2	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( [ ( +g ‘ 𝑚 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑜 𝑦 ) ∈ 𝑏 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) )
17	3 5 16	sbcied2	⊢ ( 𝑚 = 𝑀 → ( [ ( Base ‘ 𝑚 ) / 𝑏 ] [ ( +g ‘ 𝑚 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑜 𝑦 ) ∈ 𝑏 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) )
18		df-mgm	⊢ Mgm = { 𝑚 ∣ [ ( Base ‘ 𝑚 ) / 𝑏 ] [ ( +g ‘ 𝑚 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑜 𝑦 ) ∈ 𝑏 }
19	17 18	elab2g	⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ⚬ 𝑦 ) ∈ 𝐵 ) )