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

Metamath Proof Explorer

Theorem grponpcan

Description: Cancellation law for group division. ( npcan analog.) (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses grpdivf.1 ⊢ 𝑋 = ran 𝐺
grpdivf.3 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
Assertion grponpcan ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 grpdivf.1 ⊢ 𝑋 = ran 𝐺
2 grpdivf.3 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
3 eqid ⊢ ( inv ‘ 𝐺 ) = ( inv ‘ 𝐺 )
4 1 3 2 grpodivval ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) )
5 4 oveq1d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) = ( ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) 𝐺 𝐵 ) )
6 simp1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐺 ∈ GrpOp )
7 simp2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
8 1 3 grpoinvcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 )
9 8 3adant2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 )
10 simp3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
11 1 grpoass ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) 𝐺 𝐵 ) = ( 𝐴 𝐺 ( ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) 𝐺 𝐵 ) ) )
12 6 7 9 10 11 syl13anc ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) 𝐺 𝐵 ) = ( 𝐴 𝐺 ( ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) 𝐺 𝐵 ) ) )
13 eqid ⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
14 1 13 3 grpolinv ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) 𝐺 𝐵 ) = ( GId ‘ 𝐺 ) )
15 14 oveq2d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) 𝐺 𝐵 ) ) = ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) )
16 15 3adant2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) 𝐺 𝐵 ) ) = ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) )
17 1 13 grporid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) = 𝐴 )
18 17 3adant3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) = 𝐴 )
19 16 18 eqtrd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) 𝐺 𝐵 ) ) = 𝐴 )
20 12 19 eqtrd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) 𝐺 𝐵 ) = 𝐴 )
21 5 20 eqtrd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) = 𝐴 )