Metamath Proof Explorer

Theorem grppropd

Description: If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses grppropd.1 ⊢ φ → B = Base K
grppropd.2 ⊢ φ → B = Base L
grppropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
Assertion grppropd ⊢ φ → K ∈ Grp ↔ L ∈ Grp

Proof

Step Hyp Ref Expression
1 grppropd.1 ⊢ φ → B = Base K
2 grppropd.2 ⊢ φ → B = Base L
3 grppropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
4 1 2 3 mndpropd ⊢ φ → K ∈ Mnd ↔ L ∈ Mnd
5 1 2 3 grpidpropd ⊢ φ → 0 K = 0 L
6 5 adantr ⊢ φ ∧ x ∈ B ∧ y ∈ B → 0 K = 0 L
7 3 6 eqeq12d ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = 0 K ↔ x + L y = 0 L
8 7 anass1rs ⊢ φ ∧ y ∈ B ∧ x ∈ B → x + K y = 0 K ↔ x + L y = 0 L
9 8 rexbidva ⊢ φ ∧ y ∈ B → ∃ x ∈ B x + K y = 0 K ↔ ∃ x ∈ B x + L y = 0 L
10 9 ralbidva ⊢ φ → ∀ y ∈ B ∃ x ∈ B x + K y = 0 K ↔ ∀ y ∈ B ∃ x ∈ B x + L y = 0 L
11 1 rexeqdv ⊢ φ → ∃ x ∈ B x + K y = 0 K ↔ ∃ x ∈ Base K x + K y = 0 K
12 1 11 raleqbidv ⊢ φ → ∀ y ∈ B ∃ x ∈ B x + K y = 0 K ↔ ∀ y ∈ Base K ∃ x ∈ Base K x + K y = 0 K
13 2 rexeqdv ⊢ φ → ∃ x ∈ B x + L y = 0 L ↔ ∃ x ∈ Base L x + L y = 0 L
14 2 13 raleqbidv ⊢ φ → ∀ y ∈ B ∃ x ∈ B x + L y = 0 L ↔ ∀ y ∈ Base L ∃ x ∈ Base L x + L y = 0 L
15 10 12 14 3bitr3d ⊢ φ → ∀ y ∈ Base K ∃ x ∈ Base K x + K y = 0 K ↔ ∀ y ∈ Base L ∃ x ∈ Base L x + L y = 0 L
16 4 15 anbi12d ⊢ φ → K ∈ Mnd ∧ ∀ y ∈ Base K ∃ x ∈ Base K x + K y = 0 K ↔ L ∈ Mnd ∧ ∀ y ∈ Base L ∃ x ∈ Base L x + L y = 0 L
17 eqid ⊢ Base K = Base K
18 eqid ⊢ + K = + K
19 eqid ⊢ 0 K = 0 K
20 17 18 19 isgrp ⊢ K ∈ Grp ↔ K ∈ Mnd ∧ ∀ y ∈ Base K ∃ x ∈ Base K x + K y = 0 K
21 eqid ⊢ Base L = Base L
22 eqid ⊢ + L = + L
23 eqid ⊢ 0 L = 0 L
24 21 22 23 isgrp ⊢ L ∈ Grp ↔ L ∈ Mnd ∧ ∀ y ∈ Base L ∃ x ∈ Base L x + L y = 0 L
25 16 20 24 3bitr4g ⊢ φ → K ∈ Grp ↔ L ∈ Grp