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

Metamath Proof Explorer

Theorem grpidinv2

Description: A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010) (Revised by AV, 1-Sep-2021)

Ref Expression
Hypotheses grplrinv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
grplrinv.p ⊢ + = ( +g ‘ 𝐺 )
grplrinv.i ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion grpidinv2 ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ) → ( ( ( 0 + 𝐴 ) = 𝐴 ∧ ( 𝐴 + 0 ) = 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑦 ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 grplrinv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grplrinv.p ⊢ + = ( +g ‘ 𝐺 )
3 grplrinv.i ⊢ 0 = ( 0g ‘ 𝐺 )
4 1 2 3 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ) → ( 0 + 𝐴 ) = 𝐴 )
5 1 2 3 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 + 0 ) = 𝐴 )
6 1 2 3 grplrinv ⊢ ( 𝐺 ∈ Grp → ∀ 𝑧 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑦 ) = 0 ) )
7 oveq2 ⊢ ( 𝑧 = 𝐴 → ( 𝑦 + 𝑧 ) = ( 𝑦 + 𝐴 ) )
8 7 eqeq1d ⊢ ( 𝑧 = 𝐴 → ( ( 𝑦 + 𝑧 ) = 0 ↔ ( 𝑦 + 𝐴 ) = 0 ) )
9 oveq1 ⊢ ( 𝑧 = 𝐴 → ( 𝑧 + 𝑦 ) = ( 𝐴 + 𝑦 ) )
10 9 eqeq1d ⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 + 𝑦 ) = 0 ↔ ( 𝐴 + 𝑦 ) = 0 ) )
11 8 10 anbi12d ⊢ ( 𝑧 = 𝐴 → ( ( ( 𝑦 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑦 ) = 0 ) ↔ ( ( 𝑦 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑦 ) = 0 ) ) )
12 11 rexbidv ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑦 ) = 0 ) ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑦 ) = 0 ) ) )
13 12 rspcv ⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑧 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝑧 ) = 0 ∧ ( 𝑧 + 𝑦 ) = 0 ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑦 ) = 0 ) ) )
14 6 13 mpan9 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑦 ) = 0 ) )
15 4 5 14 jca31 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ) → ( ( ( 0 + 𝐴 ) = 𝐴 ∧ ( 𝐴 + 0 ) = 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝐴 ) = 0 ∧ ( 𝐴 + 𝑦 ) = 0 ) ) )