Metamath Proof Explorer

Theorem ablodivdiv4

Description: Law for double group division. (Contributed by NM, 29-Feb-2008) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 abldiv.1 ⊢ 𝑋 = ran 𝐺
2 abldiv.3 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
3 ablogrpo ⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
4 simpl ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐺 ∈ GrpOp )
5 1 2 grpodivcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ 𝑋 )
6 5 3adant3r3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ 𝑋 )
7 simpr3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐶 ∈ 𝑋 )
8 eqid ⊢ ( inv ‘ 𝐺 ) = ( inv ‘ 𝐺 )
9 1 8 2 grpodivval ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 𝐷 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) 𝐷 𝐶 ) = ( ( 𝐴 𝐷 𝐵 ) 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) )
10 4 6 7 9 syl3anc ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) 𝐷 𝐶 ) = ( ( 𝐴 𝐷 𝐵 ) 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) )
11 3 10 sylan ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) 𝐷 𝐶 ) = ( ( 𝐴 𝐷 𝐵 ) 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) )
12 simpr1 ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
13 simpr2 ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
14 simp3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ∈ 𝑋 )
15 1 8 grpoinvcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐶 ∈ 𝑋 ) → ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 )
16 3 14 15 syl2an ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 )
17 12 13 16 3jca ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 ) )
18 1 2 ablodivdiv ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 ) ) → ( 𝐴 𝐷 ( 𝐵 𝐷 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) ) = ( ( 𝐴 𝐷 𝐵 ) 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) )
19 17 18 syldan ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 ( 𝐵 𝐷 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) ) = ( ( 𝐴 𝐷 𝐵 ) 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) )
20 1 8 2 grpodivinv ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝐷 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) = ( 𝐵 𝐺 𝐶 ) )
21 3 20 syl3an1 ⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝐷 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) = ( 𝐵 𝐺 𝐶 ) )
22 21 3adant3r1 ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝐷 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) = ( 𝐵 𝐺 𝐶 ) )
23 22 oveq2d ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 ( 𝐵 𝐷 ( ( inv ‘ 𝐺 ) ‘ 𝐶 ) ) ) = ( 𝐴 𝐷 ( 𝐵 𝐺 𝐶 ) ) )
24 11 19 23 3eqtr2d ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) 𝐷 𝐶 ) = ( 𝐴 𝐷 ( 𝐵 𝐺 𝐶 ) ) )