Metamath Proof Explorer


Theorem grpidinv

Description: A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006) (Revised by AV, 1-Sep-2021)

Ref Expression
Hypotheses grpidinv.b 𝐵 = ( Base ‘ 𝐺 )
grpidinv.p + = ( +g𝐺 )
Assertion grpidinv ( 𝐺 ∈ Grp → ∃ 𝑢𝐵𝑥𝐵 ( ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦𝐵 ( ( 𝑦 + 𝑥 ) = 𝑢 ∧ ( 𝑥 + 𝑦 ) = 𝑢 ) ) )

Proof

Step Hyp Ref Expression
1 grpidinv.b 𝐵 = ( Base ‘ 𝐺 )
2 grpidinv.p + = ( +g𝐺 )
3 eqid ( 0g𝐺 ) = ( 0g𝐺 )
4 1 3 grpidcl ( 𝐺 ∈ Grp → ( 0g𝐺 ) ∈ 𝐵 )
5 oveq1 ( 𝑢 = ( 0g𝐺 ) → ( 𝑢 + 𝑥 ) = ( ( 0g𝐺 ) + 𝑥 ) )
6 5 eqeq1d ( 𝑢 = ( 0g𝐺 ) → ( ( 𝑢 + 𝑥 ) = 𝑥 ↔ ( ( 0g𝐺 ) + 𝑥 ) = 𝑥 ) )
7 oveq2 ( 𝑢 = ( 0g𝐺 ) → ( 𝑥 + 𝑢 ) = ( 𝑥 + ( 0g𝐺 ) ) )
8 7 eqeq1d ( 𝑢 = ( 0g𝐺 ) → ( ( 𝑥 + 𝑢 ) = 𝑥 ↔ ( 𝑥 + ( 0g𝐺 ) ) = 𝑥 ) )
9 6 8 anbi12d ( 𝑢 = ( 0g𝐺 ) → ( ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ↔ ( ( ( 0g𝐺 ) + 𝑥 ) = 𝑥 ∧ ( 𝑥 + ( 0g𝐺 ) ) = 𝑥 ) ) )
10 eqeq2 ( 𝑢 = ( 0g𝐺 ) → ( ( 𝑦 + 𝑥 ) = 𝑢 ↔ ( 𝑦 + 𝑥 ) = ( 0g𝐺 ) ) )
11 eqeq2 ( 𝑢 = ( 0g𝐺 ) → ( ( 𝑥 + 𝑦 ) = 𝑢 ↔ ( 𝑥 + 𝑦 ) = ( 0g𝐺 ) ) )
12 10 11 anbi12d ( 𝑢 = ( 0g𝐺 ) → ( ( ( 𝑦 + 𝑥 ) = 𝑢 ∧ ( 𝑥 + 𝑦 ) = 𝑢 ) ↔ ( ( 𝑦 + 𝑥 ) = ( 0g𝐺 ) ∧ ( 𝑥 + 𝑦 ) = ( 0g𝐺 ) ) ) )
13 12 rexbidv ( 𝑢 = ( 0g𝐺 ) → ( ∃ 𝑦𝐵 ( ( 𝑦 + 𝑥 ) = 𝑢 ∧ ( 𝑥 + 𝑦 ) = 𝑢 ) ↔ ∃ 𝑦𝐵 ( ( 𝑦 + 𝑥 ) = ( 0g𝐺 ) ∧ ( 𝑥 + 𝑦 ) = ( 0g𝐺 ) ) ) )
14 9 13 anbi12d ( 𝑢 = ( 0g𝐺 ) → ( ( ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦𝐵 ( ( 𝑦 + 𝑥 ) = 𝑢 ∧ ( 𝑥 + 𝑦 ) = 𝑢 ) ) ↔ ( ( ( ( 0g𝐺 ) + 𝑥 ) = 𝑥 ∧ ( 𝑥 + ( 0g𝐺 ) ) = 𝑥 ) ∧ ∃ 𝑦𝐵 ( ( 𝑦 + 𝑥 ) = ( 0g𝐺 ) ∧ ( 𝑥 + 𝑦 ) = ( 0g𝐺 ) ) ) ) )
15 14 ralbidv ( 𝑢 = ( 0g𝐺 ) → ( ∀ 𝑥𝐵 ( ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦𝐵 ( ( 𝑦 + 𝑥 ) = 𝑢 ∧ ( 𝑥 + 𝑦 ) = 𝑢 ) ) ↔ ∀ 𝑥𝐵 ( ( ( ( 0g𝐺 ) + 𝑥 ) = 𝑥 ∧ ( 𝑥 + ( 0g𝐺 ) ) = 𝑥 ) ∧ ∃ 𝑦𝐵 ( ( 𝑦 + 𝑥 ) = ( 0g𝐺 ) ∧ ( 𝑥 + 𝑦 ) = ( 0g𝐺 ) ) ) ) )
16 15 adantl ( ( 𝐺 ∈ Grp ∧ 𝑢 = ( 0g𝐺 ) ) → ( ∀ 𝑥𝐵 ( ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦𝐵 ( ( 𝑦 + 𝑥 ) = 𝑢 ∧ ( 𝑥 + 𝑦 ) = 𝑢 ) ) ↔ ∀ 𝑥𝐵 ( ( ( ( 0g𝐺 ) + 𝑥 ) = 𝑥 ∧ ( 𝑥 + ( 0g𝐺 ) ) = 𝑥 ) ∧ ∃ 𝑦𝐵 ( ( 𝑦 + 𝑥 ) = ( 0g𝐺 ) ∧ ( 𝑥 + 𝑦 ) = ( 0g𝐺 ) ) ) ) )
17 1 2 3 grpidinv2 ( ( 𝐺 ∈ Grp ∧ 𝑥𝐵 ) → ( ( ( ( 0g𝐺 ) + 𝑥 ) = 𝑥 ∧ ( 𝑥 + ( 0g𝐺 ) ) = 𝑥 ) ∧ ∃ 𝑦𝐵 ( ( 𝑦 + 𝑥 ) = ( 0g𝐺 ) ∧ ( 𝑥 + 𝑦 ) = ( 0g𝐺 ) ) ) )
18 17 ralrimiva ( 𝐺 ∈ Grp → ∀ 𝑥𝐵 ( ( ( ( 0g𝐺 ) + 𝑥 ) = 𝑥 ∧ ( 𝑥 + ( 0g𝐺 ) ) = 𝑥 ) ∧ ∃ 𝑦𝐵 ( ( 𝑦 + 𝑥 ) = ( 0g𝐺 ) ∧ ( 𝑥 + 𝑦 ) = ( 0g𝐺 ) ) ) )
19 4 16 18 rspcedvd ( 𝐺 ∈ Grp → ∃ 𝑢𝐵𝑥𝐵 ( ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦𝐵 ( ( 𝑦 + 𝑥 ) = 𝑢 ∧ ( 𝑥 + 𝑦 ) = 𝑢 ) ) )