Theorem opifismgm

Description: A structure with a group addition operation expressed by a conditional operator is a magma if both values of the conditional operator are contained in the base set. (Contributed by AV, 9-Feb-2020)

	Ref	Expression
Hypotheses	opifismgm.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	opifismgm.p	⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝜓 , 𝐶 , 𝐷 ) )
	opifismgm.n	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
	opifismgm.c	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
	opifismgm.d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐷 ∈ 𝐵 )
Assertion	opifismgm	⊢ ( 𝜑 → 𝑀 ∈ Mgm )

Proof

Step	Hyp	Ref	Expression
1		opifismgm.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		opifismgm.p	⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝜓 , 𝐶 , 𝐷 ) )
3		opifismgm.n	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
4		opifismgm.c	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
5		opifismgm.d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐷 ∈ 𝐵 )
6	4 5	ifcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → if ( 𝜓 , 𝐶 , 𝐷 ) ∈ 𝐵 )
7	6	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 if ( 𝜓 , 𝐶 , 𝐷 ) ∈ 𝐵 )
8	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 if ( 𝜓 , 𝐶 , 𝐷 ) ∈ 𝐵 )
9		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
10		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
11	2	ovmpoelrn	⊢ ( ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 if ( 𝜓 , 𝐶 , 𝐷 ) ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 )
12	8 9 10 11	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 )
13	12	ralrimivva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 )
14		n0	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐵 )
15		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
16	1 15	ismgmn0	⊢ ( 𝑥 ∈ 𝐵 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) )
17	16	exlimiv	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐵 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) )
18	14 17	sylbi	⊢ ( 𝐵 ≠ ∅ → ( 𝑀 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) )
19	3 18	syl	⊢ ( 𝜑 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) )
20	13 19	mpbird	⊢ ( 𝜑 → 𝑀 ∈ Mgm )