This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isgrpd2e

Description: Deduce a group from its properties. In this version of isgrpd2 , we don't assume there is an expression for the inverse of x . (Contributed by NM, 10-Aug-2013)

Ref Expression
Hypotheses isgrpd2.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
isgrpd2.p ⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
isgrpd2.z ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐺 ) )
isgrpd2.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
isgrpd2e.n ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 )
Assertion isgrpd2e ( 𝜑 → 𝐺 ∈ Grp )

Proof

Step Hyp Ref Expression
1 isgrpd2.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
2 isgrpd2.p ⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
3 isgrpd2.z ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐺 ) )
4 isgrpd2.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
5 isgrpd2e.n ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 )
6 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 )
7 2 oveqd ⊢ ( 𝜑 → ( 𝑦 + 𝑥 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
8 7 3 eqeq12d ⊢ ( 𝜑 → ( ( 𝑦 + 𝑥 ) = 0 ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
9 1 8 rexeqbidv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 ↔ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
10 1 9 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
11 6 10 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
12 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
13 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
14 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
15 12 13 14 isgrp ⊢ ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
16 4 11 15 sylanbrc ⊢ ( 𝜑 → 𝐺 ∈ Grp )