Metamath Proof Explorer


Theorem grpprop

Description: If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by NM, 11-Oct-2013)

Ref Expression
Hypotheses grpprop.b ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 )
grpprop.p ( +g𝐾 ) = ( +g𝐿 )
Assertion grpprop ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp )

Proof

Step Hyp Ref Expression
1 grpprop.b ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 )
2 grpprop.p ( +g𝐾 ) = ( +g𝐿 )
3 eqidd ( ⊤ → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
4 1 a1i ( ⊤ → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
5 2 oveqi ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 )
6 5 a1i ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
7 3 4 6 grppropd ( ⊤ → ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp ) )
8 7 mptru ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp )