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