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

Metamath Proof Explorer

Theorem grpoinvdiv

Description: Inverse of a group division. (Contributed by NM, 24-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses grpdiv.1 ⊢ 𝑋 = ran 𝐺
grpdiv.2 ⊢ 𝑁 = ( inv ‘ 𝐺 )
grpdiv.3 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
Assertion grpoinvdiv ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐷 𝐵 ) ) = ( 𝐵 𝐷 𝐴 ) )

Proof

Step Hyp Ref Expression
1 grpdiv.1 ⊢ 𝑋 = ran 𝐺
2 grpdiv.2 ⊢ 𝑁 = ( inv ‘ 𝐺 )
3 grpdiv.3 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
4 1 2 3 grpodivval ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) )
5 4 fveq2d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐷 𝐵 ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) ) )
6 1 2 grpoinvcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 )
7 6 3adant2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 )
8 1 2 grpoinvop ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) ) = ( ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
9 7 8 syld3an3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) ) = ( ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
10 1 2 grpo2inv ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) = 𝐵 )
11 10 3adant2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) = 𝐵 )
12 11 oveq1d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( 𝐵 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
13 1 2 3 grpodivval ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐵 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
14 13 3com23 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐵 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
15 12 14 eqtr4d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( 𝐵 𝐷 𝐴 ) )
16 5 9 15 3eqtrd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐷 𝐵 ) ) = ( 𝐵 𝐷 𝐴 ) )