This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpidrcan

Description: If right 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 grpidrcan ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 + 𝑍 ) = 𝑋 ↔ 𝑍 = 0 ) )

Proof

Step Hyp Ref Expression
1 grpidrcan.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grpidrcan.p ⊢ + = ( +g ‘ 𝐺 )
3 grpidrcan.o ⊢ 0 = ( 0g ‘ 𝐺 )
4 1 2 3 grprid ⊢ ( ( 𝐺 ∈ 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 grplcan ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑍 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑍 ) = ( 𝑋 + 0 ) ↔ 𝑍 = 0 ) )
13 7 8 10 11 12 syl13anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 + 𝑍 ) = ( 𝑋 + 0 ) ↔ 𝑍 = 0 ) )
14 6 13 bitr3d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 + 𝑍 ) = 𝑋 ↔ 𝑍 = 0 ) )