Theorem ablmuldiv 8115

Description: Law for group multiplication and division.

Hypotheses

Ref	Expression
abldiv.1	⊢ X = ran G
abldiv.3	⊢ D = ( /g ‘G)

Assertion

Ref	Expression
ablmuldiv	⊢ ((G ∈ Abel ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((AGB)DC) = ((ADC)GB))

Proof of Theorem ablmuldiv

Step	Hyp	Ref	Expression
1		abldiv.1	. . . . 5 ⊢ X = ran G
2	1	ablcom 8111	. . . 4 ⊢ ((G ∈ Abel ⋀ A ∈ X ⋀ B ∈ X) → (AGB) = (BGA))
3	2	3adant3r3 848	. . 3 ⊢ ((G ∈ Abel ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → (AGB) = (BGA))
4	3	opreq1d 3989	. 2 ⊢ ((G ∈ Abel ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((AGB)DC) = ((BGA)DC))
5		abldiv.3	. . . . 5 ⊢ D = ( /g ‘G)
6	1, 5	grpmuldivass 8096	. . . 4 ⊢ ((G ∈ Grp ⋀ (B ∈ X ⋀ A ∈ X ⋀ C ∈ X)) → ((BGA)DC) = (BG(ADC)))
7		ablgrp 8110	. . . 4 ⊢ (G ∈ Abel → G ∈ Grp)
8	6, 7	sylan 451	. . 3 ⊢ ((G ∈ Abel ⋀ (B ∈ X ⋀ A ∈ X ⋀ C ∈ X)) → ((BGA)DC) = (BG(ADC)))
9		3ancoma 786	. . 3 ⊢ ((A ∈ X ⋀ B ∈ X ⋀ C ∈ X) ↔ (B ∈ X ⋀ A ∈ X ⋀ C ∈ X))
10	8, 9	sylan2b 455	. 2 ⊢ ((G ∈ Abel ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((BGA)DC) = (BG(ADC)))
11		3simp2 793	. . . . 5 ⊢ ((A ∈ X ⋀ B ∈ X ⋀ C ∈ X) → B ∈ X)
12	11	adantl 390	. . . 4 ⊢ ((G ∈ Abel ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → B ∈ X)
13	1, 5	grpdivcl 8094	. . . . . 6 ⊢ ((G ∈ Grp ⋀ A ∈ X ⋀ C ∈ X) → (ADC) ∈ X)
14	13, 7	syl3an1 863	. . . . 5 ⊢ ((G ∈ Abel ⋀ A ∈ X ⋀ C ∈ X) → (ADC) ∈ X)
15	14	3adant3r2 847	. . . 4 ⊢ ((G ∈ Abel ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → (ADC) ∈ X)
16	12, 15	jca 288	. . 3 ⊢ ((G ∈ Abel ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → (B ∈ X ⋀ (ADC) ∈ X))
17	1	ablcom 8111	. . . 4 ⊢ ((G ∈ Abel ⋀ B ∈ X ⋀ (ADC) ∈ X) → (BG(ADC)) = ((ADC)GB))
18	17	3expb 838	. . 3 ⊢ ((G ∈ Abel ⋀ (B ∈ X ⋀ (ADC) ∈ X)) → (BG(ADC)) = ((ADC)GB))
19	16, 18	syldan 470	. 2 ⊢ ((G ∈ Abel ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → (BG(ADC)) = ((ADC)GB))
20	4, 10, 19	3eqtrd 1518	1 ⊢ ((G ∈ Abel ⋀ (A ∈ X ⋀ B ∈ X ⋀ C ∈ X)) → ((AGB)DC) = ((ADC)GB))

Syntax hints:   → wi 3   ⋀ wa 223   ⋀ w3a 779   = wceq 960   ∈ wcel 962  ran crn 3185   ‘cfv 3196  (class class class)co 3977  Grpcgr 8042   /_g cgs 8045  Abelcabl 8107

This theorem is referenced by:  abldivdiv 8116  nvaddsub 8287

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466  ax-rep 2706  ax-sep 2716  ax-nul 2723  ax-pow 2756  ax-pr 2793  ax-un 2880

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 781  df-ex 985  df-sb 1178  df-eu 1388  df-mo 1389  df-clab 1471  df-cleq 1476  df-clel 1479  df-ne 1594  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-csb 2010  df-dif 2058  df-un 2059  df-in 2060  df-ss 2062  df-nul 2290  df-pw 2412  df-sn 2422  df-pr 2423  df-op 2426  df-uni 2516  df-br 2633  df-opab 2680  df-id 2849  df-xp 3198  df-rel 3199  df-cnv 3200  df-co 3201  df-dm 3202  df-rn 3203  df-res 3204  df-ima 3205  df-fun 3206  df-fn 3207  df-f 3208  df-fo 3210  df-fv 3212  df-opr 3979  df-oprab 3980  df-1st 4093  df-2nd 4094  df-grp 8046  df-gid 8047  df-ginv 8048  df-gdiv 8049  df-abl 8108

Copyright terms: Public domain