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	biimtrdi	⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 → ( 𝐾 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +_g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) ) )
29	28	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑎 𝑎 ∈ 𝐵 → ( 𝐾 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( +_g ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) ) )
30	23 29	biimtrid	⊢ ( 𝜑 → ( 𝐵 ≠ ∅ → ( 𝐾 ∈ 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	biimtrdi	⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 → ( 𝐿 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +_g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) ) )
37	36	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑎 𝑎 ∈ 𝐵 → ( 𝐿 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +_g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) ) )
38	23 37	biimtrid	⊢ ( 𝜑 → ( 𝐵 ≠ ∅ → ( 𝐿 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +_g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) ) )
39	3 38	mpd	⊢ ( 𝜑 → ( 𝐿 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑥 ( +_g ‘ 𝐿 ) 𝑦 ) ∈ ( Base ‘ 𝐿 ) ) )
40	22 31 39	3bitr4d	⊢ ( 𝜑 → ( 𝐾 ∈ Mgm ↔ 𝐿 ∈ Mgm ) )

Metamath Proof Explorer

Theorem mgmpropd

Proof