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

Metamath Proof Explorer

Theorem grplrinv

Description: In a group, every member has a left and right inverse. (Contributed by AV, 1-Sep-2021)

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

Proof

Step Hyp Ref Expression
1 grplrinv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grplrinv.p ⊢ + = ( +g ‘ 𝐺 )
3 grplrinv.i ⊢ 0 = ( 0g ‘ 𝐺 )
4 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
5 1 4 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
6 oveq1 ⊢ ( 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) → ( 𝑦 + 𝑥 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑥 ) )
7 6 eqeq1d ⊢ ( 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) → ( ( 𝑦 + 𝑥 ) = 0 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑥 ) = 0 ) )
8 oveq2 ⊢ ( 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) → ( 𝑥 + 𝑦 ) = ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) )
9 8 eqeq1d ⊢ ( 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) → ( ( 𝑥 + 𝑦 ) = 0 ↔ ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ) )
10 7 9 anbi12d ⊢ ( 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) → ( ( ( 𝑦 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝑦 ) = 0 ) ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑥 ) = 0 ∧ ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ) ) )
11 10 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( ( ( 𝑦 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝑦 ) = 0 ) ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑥 ) = 0 ∧ ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ) ) )
12 1 2 3 4 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑥 ) = 0 )
13 1 2 3 4 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 )
14 12 13 jca ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) + 𝑥 ) = 0 ∧ ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = 0 ) )
15 5 11 14 rspcedvd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝑦 ) = 0 ) )
16 15 ralrimiva ⊢ ( 𝐺 ∈ Grp → ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑦 + 𝑥 ) = 0 ∧ ( 𝑥 + 𝑦 ) = 0 ) )