Metamath Proof Explorer

Theorem mgmpropd

Description: If two structures have the same (nonempty) base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a magma iff the other one is. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses mgmpropd.k ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
mgmpropd.l ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
mgmpropd.b ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
mgmpropd.p ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
Assertion mgmpropd ( 𝜑 → ( 𝐾 ∈ Mgm ↔ 𝐿 ∈ Mgm ) )

Proof

Step Hyp Ref Expression
1 mgmpropd.k ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 mgmpropd.l ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 mgmpropd.b ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
4 mgmpropd.p ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
5 simpl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → 𝜑 )
6 1 eqcomd ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = 𝐵 )
7 6 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↔ 𝑥 ∈ 𝐵 ) )
8 7 biimpcd ⊢ ( 𝑥 ∈ ( Base ‘ 𝐾 ) → ( 𝜑 → 𝑥 ∈ 𝐵 ) )
9 8 adantr ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝜑 → 𝑥 ∈ 𝐵 ) )
10 9 impcom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → 𝑥 ∈ 𝐵 )
11 6 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ ( Base ‘ 𝐾 ) ↔ 𝑦 ∈ 𝐵 ) )
12 11 biimpd ⊢ ( 𝜑 → ( 𝑦 ∈ ( Base ‘ 𝐾 ) → 𝑦 ∈ 𝐵 ) )
13 12 adantld ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → 𝑦 ∈ 𝐵 ) )
14 13 imp ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → 𝑦 ∈ 𝐵 )
15 5 10 14 4 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
16 15 eleq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ↔ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) )
17 16 2ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) )
18 1 2 eqtr3d ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
19 18 eleq2d ⊢ ( 𝜑 → ( ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ↔ ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) )
20 18 19 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) )
21 18 20 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) )
22 17 21 bitrd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) )
23 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑎 𝑎 ∈ 𝐵 )
24 1 eleq2d ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 ↔ 𝑎 ∈ ( Base ‘ 𝐾 ) ) )
25 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
26 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
27 25 26 ismgmn0 ⊢ ( 𝑎 ∈ ( Base ‘ 𝐾 ) → ( 𝐾 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) )
28 24 27 syl6bi ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 → ( 𝐾 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) ) )
29 28 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑎 𝑎 ∈ 𝐵 → ( 𝐾 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) ) )
30 23 29 syl5bi ⊢ ( 𝜑 → ( 𝐵 ≠ ∅ → ( 𝐾 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) ) )
31 3 30 mpd ⊢ ( 𝜑 → ( 𝐾 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) )
32 2 eleq2d ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 ↔ 𝑎 ∈ ( Base ‘ 𝐿 ) ) )
33 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
34 eqid ⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
35 33 34 ismgmn0 ⊢ ( 𝑎 ∈ ( Base ‘ 𝐿 ) → ( 𝐿 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) )
36 32 35 syl6bi ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 → ( 𝐿 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) ) )
37 36 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑎 𝑎 ∈ 𝐵 → ( 𝐿 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) ) )
38 23 37 syl5bi ⊢ ( 𝜑 → ( 𝐵 ≠ ∅ → ( 𝐿 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) ) )
39 3 38 mpd ⊢ ( 𝜑 → ( 𝐿 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) )
40 22 31 39 3bitr4d ⊢ ( 𝜑 → ( 𝐾 ∈ Mgm ↔ 𝐿 ∈ Mgm ) )