Metamath Proof Explorer

Theorem grpomuldivass

Description: Associative-type law for multiplication and division. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 grpdivf.1 ⊢ 𝑋 = ran 𝐺
2 grpdivf.3 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
3 simpr1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
4 simpr2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
5 eqid ⊢ ( inv ‘ 𝐺 ) = ( inv ‘ 𝐺 )
6 1 5 grpoinvcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐶 ∈ 𝑋 ) → ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 )
7 6 3ad2antr3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 )
8 3 4 7 3jca ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 ) )
9 1 grpoass ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) = ( 𝐴 𝐺 ( 𝐵 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) ) )
10 8 9 syldan ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) = ( 𝐴 𝐺 ( 𝐵 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) ) )
11 simpl ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐺 ∈ GrpOp )
12 1 grpocl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
13 12 3adant3r3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
14 simpr3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐶 ∈ 𝑋 )
15 1 5 2 grpodivval ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐷 𝐶 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) )
16 11 13 14 15 syl3anc ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐷 𝐶 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) )
17 1 5 2 grpodivval ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐶 ) = ( 𝐵 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) )
18 17 3adant3r1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝐷 𝐶 ) = ( 𝐵 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) )
19 18 oveq2d ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐺 ( 𝐵 𝐷 𝐶 ) ) = ( 𝐴 𝐺 ( 𝐵 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) ) )
20 10 16 19 3eqtr4d ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐷 𝐶 ) = ( 𝐴 𝐺 ( 𝐵 𝐷 𝐶 ) ) )