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