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 ) )