Metamath Proof Explorer

Theorem cmnpropd

Description: If two structures have the same group components (properties), one is a commutative monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 ablpropd.1 ⊢ φ → B = Base K
2 ablpropd.2 ⊢ φ → B = Base L
3 ablpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
4 1 2 3 mndpropd ⊢ φ → K ∈ Mnd ↔ L ∈ Mnd
5 3 oveqrspc2v ⊢ φ ∧ u ∈ B ∧ v ∈ B → u + K v = u + L v
6 3 oveqrspc2v ⊢ φ ∧ v ∈ B ∧ u ∈ B → v + K u = v + L u
7 6 ancom2s ⊢ φ ∧ u ∈ B ∧ v ∈ B → v + K u = v + L u
8 5 7 eqeq12d ⊢ φ ∧ u ∈ B ∧ v ∈ B → u + K v = v + K u ↔ u + L v = v + L u
9 8 2ralbidva ⊢ φ → ∀ u ∈ B ∀ v ∈ B u + K v = v + K u ↔ ∀ u ∈ B ∀ v ∈ B u + L v = v + L u
10 1 raleqdv ⊢ φ → ∀ v ∈ B u + K v = v + K u ↔ ∀ v ∈ Base K u + K v = v + K u
11 1 10 raleqbidv ⊢ φ → ∀ u ∈ B ∀ v ∈ B u + K v = v + K u ↔ ∀ u ∈ Base K ∀ v ∈ Base K u + K v = v + K u
12 2 raleqdv ⊢ φ → ∀ v ∈ B u + L v = v + L u ↔ ∀ v ∈ Base L u + L v = v + L u
13 2 12 raleqbidv ⊢ φ → ∀ u ∈ B ∀ v ∈ B u + L v = v + L u ↔ ∀ u ∈ Base L ∀ v ∈ Base L u + L v = v + L u
14 9 11 13 3bitr3d ⊢ φ → ∀ u ∈ Base K ∀ v ∈ Base K u + K v = v + K u ↔ ∀ u ∈ Base L ∀ v ∈ Base L u + L v = v + L u
15 4 14 anbi12d ⊢ φ → K ∈ Mnd ∧ ∀ u ∈ Base K ∀ v ∈ Base K u + K v = v + K u ↔ L ∈ Mnd ∧ ∀ u ∈ Base L ∀ v ∈ Base L u + L v = v + L u
16 eqid ⊢ Base K = Base K
17 eqid ⊢ + K = + K
18 16 17 iscmn ⊢ K ∈ CMnd ↔ K ∈ Mnd ∧ ∀ u ∈ Base K ∀ v ∈ Base K u + K v = v + K u
19 eqid ⊢ Base L = Base L
20 eqid ⊢ + L = + L
21 19 20 iscmn ⊢ L ∈ CMnd ↔ L ∈ Mnd ∧ ∀ u ∈ Base L ∀ v ∈ Base L u + L v = v + L u
22 15 18 21 3bitr4g ⊢ φ → K ∈ CMnd ↔ L ∈ CMnd