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

Metamath Proof Explorer

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 )