Proof of Theorem ablodivdiv4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ablogrpo 30566 | . . 3
⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp) | 
| 2 |  | simpl 482 | . . . 4
⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → 𝐺 ∈ GrpOp) | 
| 3 |  | abldiv.1 | . . . . . 6
⊢ 𝑋 = ran 𝐺 | 
| 4 |  | abldiv.3 | . . . . . 6
⊢ 𝐷 = ( /𝑔
‘𝐺) | 
| 5 | 3, 4 | grpodivcl 30558 | . . . . 5
⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ 𝑋) | 
| 6 | 5 | 3adant3r3 1185 | . . . 4
⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ∈ 𝑋) | 
| 7 |  | simpr3 1197 | . . . 4
⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → 𝐶 ∈ 𝑋) | 
| 8 |  | eqid 2737 | . . . . 5
⊢
(inv‘𝐺) =
(inv‘𝐺) | 
| 9 | 3, 8, 4 | grpodivval 30554 | . . . 4
⊢ ((𝐺 ∈ GrpOp ∧ (𝐴𝐷𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐷𝐵)𝐷𝐶) = ((𝐴𝐷𝐵)𝐺((inv‘𝐺)‘𝐶))) | 
| 10 | 2, 6, 7, 9 | syl3anc 1373 | . . 3
⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷𝐶) = ((𝐴𝐷𝐵)𝐺((inv‘𝐺)‘𝐶))) | 
| 11 | 1, 10 | sylan 580 | . 2
⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷𝐶) = ((𝐴𝐷𝐵)𝐺((inv‘𝐺)‘𝐶))) | 
| 12 |  | simpr1 1195 | . . . 4
⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → 𝐴 ∈ 𝑋) | 
| 13 |  | simpr2 1196 | . . . 4
⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → 𝐵 ∈ 𝑋) | 
| 14 |  | simp3 1139 | . . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) | 
| 15 | 3, 8 | grpoinvcl 30543 | . . . . 5
⊢ ((𝐺 ∈ GrpOp ∧ 𝐶 ∈ 𝑋) → ((inv‘𝐺)‘𝐶) ∈ 𝑋) | 
| 16 | 1, 14, 15 | syl2an 596 | . . . 4
⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((inv‘𝐺)‘𝐶) ∈ 𝑋) | 
| 17 | 12, 13, 16 | 3jca 1129 | . . 3
⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((inv‘𝐺)‘𝐶) ∈ 𝑋)) | 
| 18 | 3, 4 | ablodivdiv 30572 | . . 3
⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((inv‘𝐺)‘𝐶) ∈ 𝑋)) → (𝐴𝐷(𝐵𝐷((inv‘𝐺)‘𝐶))) = ((𝐴𝐷𝐵)𝐺((inv‘𝐺)‘𝐶))) | 
| 19 | 17, 18 | syldan 591 | . 2
⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷(𝐵𝐷((inv‘𝐺)‘𝐶))) = ((𝐴𝐷𝐵)𝐺((inv‘𝐺)‘𝐶))) | 
| 20 | 3, 8, 4 | grpodivinv 30555 | . . . . 5
⊢ ((𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐵𝐷((inv‘𝐺)‘𝐶)) = (𝐵𝐺𝐶)) | 
| 21 | 1, 20 | syl3an1 1164 | . . . 4
⊢ ((𝐺 ∈ AbelOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐵𝐷((inv‘𝐺)‘𝐶)) = (𝐵𝐺𝐶)) | 
| 22 | 21 | 3adant3r1 1183 | . . 3
⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵𝐷((inv‘𝐺)‘𝐶)) = (𝐵𝐺𝐶)) | 
| 23 | 22 | oveq2d 7447 | . 2
⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷(𝐵𝐷((inv‘𝐺)‘𝐶))) = (𝐴𝐷(𝐵𝐺𝐶))) | 
| 24 | 11, 19, 23 | 3eqtr2d 2783 | 1
⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷𝐶) = (𝐴𝐷(𝐵𝐺𝐶))) |