Proof of Theorem rngosubdir
| Step | Hyp | Ref
| Expression |
| 1 | | ringsubdi.1 |
. . . . 5
⊢ 𝐺 = (1st ‘𝑅) |
| 2 | | ringsubdi.3 |
. . . . 5
⊢ 𝑋 = ran 𝐺 |
| 3 | | eqid 2737 |
. . . . 5
⊢
(inv‘𝐺) =
(inv‘𝐺) |
| 4 | | ringsubdi.4 |
. . . . 5
⊢ 𝐷 = ( /𝑔
‘𝐺) |
| 5 | 1, 2, 3, 4 | rngosub 37937 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐴𝐺((inv‘𝐺)‘𝐵))) |
| 6 | 5 | 3adant3r3 1185 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) = (𝐴𝐺((inv‘𝐺)‘𝐵))) |
| 7 | 6 | oveq1d 7446 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐻𝐶) = ((𝐴𝐺((inv‘𝐺)‘𝐵))𝐻𝐶)) |
| 8 | | ringsubdi.2 |
. . . . . . 7
⊢ 𝐻 = (2nd ‘𝑅) |
| 9 | 1, 8, 2 | rngocl 37908 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝐻𝐶) ∈ 𝑋) |
| 10 | 9 | 3adant3r2 1184 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻𝐶) ∈ 𝑋) |
| 11 | 1, 8, 2 | rngocl 37908 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐵𝐻𝐶) ∈ 𝑋) |
| 12 | 11 | 3adant3r1 1183 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵𝐻𝐶) ∈ 𝑋) |
| 13 | 10, 12 | jca 511 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐶) ∈ 𝑋 ∧ (𝐵𝐻𝐶) ∈ 𝑋)) |
| 14 | 1, 2, 3, 4 | rngosub 37937 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ (𝐴𝐻𝐶) ∈ 𝑋 ∧ (𝐵𝐻𝐶) ∈ 𝑋) → ((𝐴𝐻𝐶)𝐷(𝐵𝐻𝐶)) = ((𝐴𝐻𝐶)𝐺((inv‘𝐺)‘(𝐵𝐻𝐶)))) |
| 15 | 14 | 3expb 1121 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ ((𝐴𝐻𝐶) ∈ 𝑋 ∧ (𝐵𝐻𝐶) ∈ 𝑋)) → ((𝐴𝐻𝐶)𝐷(𝐵𝐻𝐶)) = ((𝐴𝐻𝐶)𝐺((inv‘𝐺)‘(𝐵𝐻𝐶)))) |
| 16 | 13, 15 | syldan 591 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐶)𝐷(𝐵𝐻𝐶)) = ((𝐴𝐻𝐶)𝐺((inv‘𝐺)‘(𝐵𝐻𝐶)))) |
| 17 | | idd 24 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps → (𝐴 ∈ 𝑋 → 𝐴 ∈ 𝑋)) |
| 18 | 1, 2, 3 | rngonegcl 37934 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝐵 ∈ 𝑋) → ((inv‘𝐺)‘𝐵) ∈ 𝑋) |
| 19 | 18 | ex 412 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps → (𝐵 ∈ 𝑋 → ((inv‘𝐺)‘𝐵) ∈ 𝑋)) |
| 20 | | idd 24 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps → (𝐶 ∈ 𝑋 → 𝐶 ∈ 𝑋)) |
| 21 | 17, 19, 20 | 3anim123d 1445 |
. . . . . 6
⊢ (𝑅 ∈ RingOps → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴 ∈ 𝑋 ∧ ((inv‘𝐺)‘𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋))) |
| 22 | 21 | imp 406 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴 ∈ 𝑋 ∧ ((inv‘𝐺)‘𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) |
| 23 | 1, 8, 2 | rngodir 37912 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ ((inv‘𝐺)‘𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺((inv‘𝐺)‘𝐵))𝐻𝐶) = ((𝐴𝐻𝐶)𝐺(((inv‘𝐺)‘𝐵)𝐻𝐶))) |
| 24 | 22, 23 | syldan 591 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺((inv‘𝐺)‘𝐵))𝐻𝐶) = ((𝐴𝐻𝐶)𝐺(((inv‘𝐺)‘𝐵)𝐻𝐶))) |
| 25 | 1, 8, 2, 3 | rngoneglmul 37950 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((inv‘𝐺)‘(𝐵𝐻𝐶)) = (((inv‘𝐺)‘𝐵)𝐻𝐶)) |
| 26 | 25 | 3adant3r1 1183 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((inv‘𝐺)‘(𝐵𝐻𝐶)) = (((inv‘𝐺)‘𝐵)𝐻𝐶)) |
| 27 | 26 | oveq2d 7447 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐶)𝐺((inv‘𝐺)‘(𝐵𝐻𝐶))) = ((𝐴𝐻𝐶)𝐺(((inv‘𝐺)‘𝐵)𝐻𝐶))) |
| 28 | 24, 27 | eqtr4d 2780 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺((inv‘𝐺)‘𝐵))𝐻𝐶) = ((𝐴𝐻𝐶)𝐺((inv‘𝐺)‘(𝐵𝐻𝐶)))) |
| 29 | 16, 28 | eqtr4d 2780 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐶)𝐷(𝐵𝐻𝐶)) = ((𝐴𝐺((inv‘𝐺)‘𝐵))𝐻𝐶)) |
| 30 | 7, 29 | eqtr4d 2780 |
1
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐷(𝐵𝐻𝐶))) |