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 ⊢ B = Base M
opifismgm.p ⊢ + M = x ∈ B , y ∈ B ⟼ if ψ C D
opifismgm.n ⊢ φ → B ≠ ∅
opifismgm.c ⊢ φ ∧ x ∈ B ∧ y ∈ B → C ∈ B
opifismgm.d ⊢ φ ∧ x ∈ B ∧ y ∈ B → D ∈ B
Assertion opifismgm ⊢ φ → M ∈ Mgm

Proof

Step Hyp Ref Expression
1 opifismgm.b ⊢ B = Base M
2 opifismgm.p ⊢ + M = x ∈ B , y ∈ B ⟼ if ψ C D
3 opifismgm.n ⊢ φ → B ≠ ∅
4 opifismgm.c ⊢ φ ∧ x ∈ B ∧ y ∈ B → C ∈ B
5 opifismgm.d ⊢ φ ∧ x ∈ B ∧ y ∈ B → D ∈ B
6 4 5 ifcld ⊢ φ ∧ x ∈ B ∧ y ∈ B → if ψ C D ∈ B
7 6 ralrimivva ⊢ φ → ∀ x ∈ B ∀ y ∈ B if ψ C D ∈ B
8 7 adantr ⊢ φ ∧ a ∈ B ∧ b ∈ B → ∀ x ∈ B ∀ y ∈ B if ψ C D ∈ B
9 simprl ⊢ φ ∧ a ∈ B ∧ b ∈ B → a ∈ B
10 simprr ⊢ φ ∧ a ∈ B ∧ b ∈ B → b ∈ B
11 2 ovmpoelrn ⊢ ∀ x ∈ B ∀ y ∈ B if ψ C D ∈ B ∧ a ∈ B ∧ b ∈ B → a + M b ∈ B
12 8 9 10 11 syl3anc ⊢ φ ∧ a ∈ B ∧ b ∈ B → a + M b ∈ B
13 12 ralrimivva ⊢ φ → ∀ a ∈ B ∀ b ∈ B a + M b ∈ B
14 n0 ⊢ B ≠ ∅ ↔ ∃ x x ∈ B
15 eqid ⊢ + M = + M
16 1 15 ismgmn0 ⊢ x ∈ B → M ∈ Mgm ↔ ∀ a ∈ B ∀ b ∈ B a + M b ∈ B
17 16 exlimiv ⊢ ∃ x x ∈ B → M ∈ Mgm ↔ ∀ a ∈ B ∀ b ∈ B a + M b ∈ B
18 14 17 sylbi ⊢ B ≠ ∅ → M ∈ Mgm ↔ ∀ a ∈ B ∀ b ∈ B a + M b ∈ B
19 3 18 syl ⊢ φ → M ∈ Mgm ↔ ∀ a ∈ B ∀ b ∈ B a + M b ∈ B
20 13 19 mpbird ⊢ φ → M ∈ Mgm