Theorem grpidlcan

Description: If left adding an element of a group to an arbitrary element of the group results in this element, the added element is the identity element and vice versa. (Contributed by AV, 15-Mar-2019)

	Ref	Expression
Hypotheses	grpidrcan.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpidrcan.p	⊢ + = ( +g ‘ 𝐺 )
	grpidrcan.o	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	grpidlcan	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑍 + 𝑋 ) = 𝑋 ↔ 𝑍 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		grpidrcan.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpidrcan.p	⊢ + = ( +g ‘ 𝐺 )
3		grpidrcan.o	⊢ 0 = ( 0g ‘ 𝐺 )
4	1 2 3	grplid	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 0 + 𝑋 ) = 𝑋 )
5	4	3adant3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 0 + 𝑋 ) = 𝑋 )
6	5	eqeq2d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑍 + 𝑋 ) = ( 0 + 𝑋 ) ↔ ( 𝑍 + 𝑋 ) = 𝑋 ) )
7		simp1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → 𝐺 ∈ Grp )
8		simp3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → 𝑍 ∈ 𝐵 )
9	1 3	grpidcl	⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 )
10	9	3ad2ant1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → 0 ∈ 𝐵 )
11		simp2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
12	1 2	grprcan	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑍 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑍 + 𝑋 ) = ( 0 + 𝑋 ) ↔ 𝑍 = 0 ) )
13	7 8 10 11 12	syl13anc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑍 + 𝑋 ) = ( 0 + 𝑋 ) ↔ 𝑍 = 0 ) )
14	6 13	bitr3d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑍 + 𝑋 ) = 𝑋 ↔ 𝑍 = 0 ) )