Step | Hyp | Ref
| Expression |
1 | | ringsubdi.1 |
. . . . 5
β’ πΊ = (1st βπ
) |
2 | | ringsubdi.3 |
. . . . 5
β’ π = ran πΊ |
3 | | eqid 2733 |
. . . . 5
β’
(invβπΊ) =
(invβπΊ) |
4 | | ringsubdi.4 |
. . . . 5
β’ π· = ( /π
βπΊ) |
5 | 1, 2, 3, 4 | rngosub 36439 |
. . . 4
β’ ((π
β RingOps β§ π΅ β π β§ πΆ β π) β (π΅π·πΆ) = (π΅πΊ((invβπΊ)βπΆ))) |
6 | 5 | 3adant3r1 1183 |
. . 3
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΅π·πΆ) = (π΅πΊ((invβπΊ)βπΆ))) |
7 | 6 | oveq2d 7377 |
. 2
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π»(π΅π·πΆ)) = (π΄π»(π΅πΊ((invβπΊ)βπΆ)))) |
8 | | ringsubdi.2 |
. . . . . . 7
β’ π» = (2nd βπ
) |
9 | 1, 8, 2 | rngocl 36410 |
. . . . . 6
β’ ((π
β RingOps β§ π΄ β π β§ π΅ β π) β (π΄π»π΅) β π) |
10 | 9 | 3adant3r3 1185 |
. . . . 5
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π»π΅) β π) |
11 | 1, 8, 2 | rngocl 36410 |
. . . . . 6
β’ ((π
β RingOps β§ π΄ β π β§ πΆ β π) β (π΄π»πΆ) β π) |
12 | 11 | 3adant3r2 1184 |
. . . . 5
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π»πΆ) β π) |
13 | 10, 12 | jca 513 |
. . . 4
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π»π΅) β π β§ (π΄π»πΆ) β π)) |
14 | 1, 2, 3, 4 | rngosub 36439 |
. . . . 5
β’ ((π
β RingOps β§ (π΄π»π΅) β π β§ (π΄π»πΆ) β π) β ((π΄π»π΅)π·(π΄π»πΆ)) = ((π΄π»π΅)πΊ((invβπΊ)β(π΄π»πΆ)))) |
15 | 14 | 3expb 1121 |
. . . 4
β’ ((π
β RingOps β§ ((π΄π»π΅) β π β§ (π΄π»πΆ) β π)) β ((π΄π»π΅)π·(π΄π»πΆ)) = ((π΄π»π΅)πΊ((invβπΊ)β(π΄π»πΆ)))) |
16 | 13, 15 | syldan 592 |
. . 3
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π»π΅)π·(π΄π»πΆ)) = ((π΄π»π΅)πΊ((invβπΊ)β(π΄π»πΆ)))) |
17 | | idd 24 |
. . . . . . 7
β’ (π
β RingOps β (π΄ β π β π΄ β π)) |
18 | | idd 24 |
. . . . . . 7
β’ (π
β RingOps β (π΅ β π β π΅ β π)) |
19 | 1, 2, 3 | rngonegcl 36436 |
. . . . . . . 8
β’ ((π
β RingOps β§ πΆ β π) β ((invβπΊ)βπΆ) β π) |
20 | 19 | ex 414 |
. . . . . . 7
β’ (π
β RingOps β (πΆ β π β ((invβπΊ)βπΆ) β π)) |
21 | 17, 18, 20 | 3anim123d 1444 |
. . . . . 6
β’ (π
β RingOps β ((π΄ β π β§ π΅ β π β§ πΆ β π) β (π΄ β π β§ π΅ β π β§ ((invβπΊ)βπΆ) β π))) |
22 | 21 | imp 408 |
. . . . 5
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄ β π β§ π΅ β π β§ ((invβπΊ)βπΆ) β π)) |
23 | 1, 8, 2 | rngodi 36413 |
. . . . 5
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ ((invβπΊ)βπΆ) β π)) β (π΄π»(π΅πΊ((invβπΊ)βπΆ))) = ((π΄π»π΅)πΊ(π΄π»((invβπΊ)βπΆ)))) |
24 | 22, 23 | syldan 592 |
. . . 4
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π»(π΅πΊ((invβπΊ)βπΆ))) = ((π΄π»π΅)πΊ(π΄π»((invβπΊ)βπΆ)))) |
25 | 1, 8, 2, 3 | rngonegrmul 36453 |
. . . . . 6
β’ ((π
β RingOps β§ π΄ β π β§ πΆ β π) β ((invβπΊ)β(π΄π»πΆ)) = (π΄π»((invβπΊ)βπΆ))) |
26 | 25 | 3adant3r2 1184 |
. . . . 5
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((invβπΊ)β(π΄π»πΆ)) = (π΄π»((invβπΊ)βπΆ))) |
27 | 26 | oveq2d 7377 |
. . . 4
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π»π΅)πΊ((invβπΊ)β(π΄π»πΆ))) = ((π΄π»π΅)πΊ(π΄π»((invβπΊ)βπΆ)))) |
28 | 24, 27 | eqtr4d 2776 |
. . 3
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π»(π΅πΊ((invβπΊ)βπΆ))) = ((π΄π»π΅)πΊ((invβπΊ)β(π΄π»πΆ)))) |
29 | 16, 28 | eqtr4d 2776 |
. 2
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π»π΅)π·(π΄π»πΆ)) = (π΄π»(π΅πΊ((invβπΊ)βπΆ)))) |
30 | 7, 29 | eqtr4d 2776 |
1
β’ ((π
β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π»(π΅π·πΆ)) = ((π΄π»π΅)π·(π΄π»πΆ))) |