Proof of Theorem rngosubdi
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 35825 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐵𝐷𝐶) = (𝐵𝐺((inv‘𝐺)‘𝐶))) |
6 | 5 | 3adant3r1 1184 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵𝐷𝐶) = (𝐵𝐺((inv‘𝐺)‘𝐶))) |
7 | 6 | oveq2d 7229 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵𝐷𝐶)) = (𝐴𝐻(𝐵𝐺((inv‘𝐺)‘𝐶)))) |
8 | | ringsubdi.2 |
. . . . . . 7
⊢ 𝐻 = (2nd ‘𝑅) |
9 | 1, 8, 2 | rngocl 35796 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐻𝐵) ∈ 𝑋) |
10 | 9 | 3adant3r3 1186 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻𝐵) ∈ 𝑋) |
11 | 1, 8, 2 | rngocl 35796 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝐻𝐶) ∈ 𝑋) |
12 | 11 | 3adant3r2 1185 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻𝐶) ∈ 𝑋) |
13 | 10, 12 | jca 515 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵) ∈ 𝑋 ∧ (𝐴𝐻𝐶) ∈ 𝑋)) |
14 | 1, 2, 3, 4 | rngosub 35825 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ (𝐴𝐻𝐵) ∈ 𝑋 ∧ (𝐴𝐻𝐶) ∈ 𝑋) → ((𝐴𝐻𝐵)𝐷(𝐴𝐻𝐶)) = ((𝐴𝐻𝐵)𝐺((inv‘𝐺)‘(𝐴𝐻𝐶)))) |
15 | 14 | 3expb 1122 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ ((𝐴𝐻𝐵) ∈ 𝑋 ∧ (𝐴𝐻𝐶) ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐷(𝐴𝐻𝐶)) = ((𝐴𝐻𝐵)𝐺((inv‘𝐺)‘(𝐴𝐻𝐶)))) |
16 | 13, 15 | syldan 594 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐷(𝐴𝐻𝐶)) = ((𝐴𝐻𝐵)𝐺((inv‘𝐺)‘(𝐴𝐻𝐶)))) |
17 | | idd 24 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps → (𝐴 ∈ 𝑋 → 𝐴 ∈ 𝑋)) |
18 | | idd 24 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps → (𝐵 ∈ 𝑋 → 𝐵 ∈ 𝑋)) |
19 | 1, 2, 3 | rngonegcl 35822 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ∈ 𝑋) → ((inv‘𝐺)‘𝐶) ∈ 𝑋) |
20 | 19 | ex 416 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps → (𝐶 ∈ 𝑋 → ((inv‘𝐺)‘𝐶) ∈ 𝑋)) |
21 | 17, 18, 20 | 3anim123d 1445 |
. . . . . 6
⊢ (𝑅 ∈ RingOps → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((inv‘𝐺)‘𝐶) ∈ 𝑋))) |
22 | 21 | imp 410 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((inv‘𝐺)‘𝐶) ∈ 𝑋)) |
23 | 1, 8, 2 | rngodi 35799 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((inv‘𝐺)‘𝐶) ∈ 𝑋)) → (𝐴𝐻(𝐵𝐺((inv‘𝐺)‘𝐶))) = ((𝐴𝐻𝐵)𝐺(𝐴𝐻((inv‘𝐺)‘𝐶)))) |
24 | 22, 23 | syldan 594 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵𝐺((inv‘𝐺)‘𝐶))) = ((𝐴𝐻𝐵)𝐺(𝐴𝐻((inv‘𝐺)‘𝐶)))) |
25 | 1, 8, 2, 3 | rngonegrmul 35839 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((inv‘𝐺)‘(𝐴𝐻𝐶)) = (𝐴𝐻((inv‘𝐺)‘𝐶))) |
26 | 25 | 3adant3r2 1185 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((inv‘𝐺)‘(𝐴𝐻𝐶)) = (𝐴𝐻((inv‘𝐺)‘𝐶))) |
27 | 26 | oveq2d 7229 |
. . . 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 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵𝐷𝐶)) = ((𝐴𝐻𝐵)𝐷(𝐴𝐻𝐶))) |