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

Metamath Proof Explorer

Theorem grpodivdiv

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

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

Proof

Step Hyp Ref Expression
1 grpdivf.1 ⊢ 𝑋 = ran 𝐺
2 grpdivf.3 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
3 simpl ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐺 ∈ GrpOp )
4 simpr1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
5 1 2 grpodivcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐶 ) ∈ 𝑋 )
6 5 3adant3r1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝐷 𝐶 ) ∈ 𝑋 )
7 eqid ⊢ ( inv ‘ 𝐺 ) = ( inv ‘ 𝐺 )
8 1 7 2 grpodivval ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐵 𝐷 𝐶 ) ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝐵 𝐷 𝐶 ) ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ ( 𝐵 𝐷 𝐶 ) ) ) )
9 3 4 6 8 syl3anc ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 ( 𝐵 𝐷 𝐶 ) ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ ( 𝐵 𝐷 𝐶 ) ) ) )
10 1 7 2 grpoinvdiv ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( inv ‘ 𝐺 ) ‘ ( 𝐵 𝐷 𝐶 ) ) = ( 𝐶 𝐷 𝐵 ) )
11 10 3adant3r1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( inv ‘ 𝐺 ) ‘ ( 𝐵 𝐷 𝐶 ) ) = ( 𝐶 𝐷 𝐵 ) )
12 11 oveq2d ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ ( 𝐵 𝐷 𝐶 ) ) ) = ( 𝐴 𝐺 ( 𝐶 𝐷 𝐵 ) ) )
13 9 12 eqtrd ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 ( 𝐵 𝐷 𝐶 ) ) = ( 𝐴 𝐺 ( 𝐶 𝐷 𝐵 ) ) )