Step | Hyp | Ref
| Expression |
1 | | idlnegcl.1 |
. . . 4
β’ πΊ = (1st βπ
) |
2 | | eqid 2737 |
. . . 4
β’ ran πΊ = ran πΊ |
3 | 1, 2 | idlss 36478 |
. . 3
β’ ((π
β RingOps β§ πΌ β (Idlβπ
)) β πΌ β ran πΊ) |
4 | | ssel2 3940 |
. . . . 5
β’ ((πΌ β ran πΊ β§ π΄ β πΌ) β π΄ β ran πΊ) |
5 | | eqid 2737 |
. . . . . 6
β’
(2nd βπ
) = (2nd βπ
) |
6 | | idlnegcl.2 |
. . . . . 6
β’ π = (invβπΊ) |
7 | | eqid 2737 |
. . . . . 6
β’
(GIdβ(2nd βπ
)) = (GIdβ(2nd βπ
)) |
8 | 1, 5, 2, 6, 7 | rngonegmn1l 36403 |
. . . . 5
β’ ((π
β RingOps β§ π΄ β ran πΊ) β (πβπ΄) = ((πβ(GIdβ(2nd
βπ
)))(2nd
βπ
)π΄)) |
9 | 4, 8 | sylan2 594 |
. . . 4
β’ ((π
β RingOps β§ (πΌ β ran πΊ β§ π΄ β πΌ)) β (πβπ΄) = ((πβ(GIdβ(2nd
βπ
)))(2nd
βπ
)π΄)) |
10 | 9 | anassrs 469 |
. . 3
β’ (((π
β RingOps β§ πΌ β ran πΊ) β§ π΄ β πΌ) β (πβπ΄) = ((πβ(GIdβ(2nd
βπ
)))(2nd
βπ
)π΄)) |
11 | 3, 10 | syldanl 603 |
. 2
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ π΄ β πΌ) β (πβπ΄) = ((πβ(GIdβ(2nd
βπ
)))(2nd
βπ
)π΄)) |
12 | 1 | rneqi 5893 |
. . . . . 6
β’ ran πΊ = ran (1st
βπ
) |
13 | 12, 5, 7 | rngo1cl 36401 |
. . . . 5
β’ (π
β RingOps β
(GIdβ(2nd βπ
)) β ran πΊ) |
14 | 1, 2, 6 | rngonegcl 36389 |
. . . . 5
β’ ((π
β RingOps β§
(GIdβ(2nd βπ
)) β ran πΊ) β (πβ(GIdβ(2nd
βπ
))) β ran
πΊ) |
15 | 13, 14 | mpdan 686 |
. . . 4
β’ (π
β RingOps β (πβ(GIdβ(2nd
βπ
))) β ran
πΊ) |
16 | 15 | ad2antrr 725 |
. . 3
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ π΄ β πΌ) β (πβ(GIdβ(2nd
βπ
))) β ran
πΊ) |
17 | 1, 5, 2 | idllmulcl 36482 |
. . . 4
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ (π΄ β πΌ β§ (πβ(GIdβ(2nd
βπ
))) β ran
πΊ)) β ((πβ(GIdβ(2nd
βπ
)))(2nd
βπ
)π΄) β πΌ) |
18 | 17 | anassrs 469 |
. . 3
β’ ((((π
β RingOps β§ πΌ β (Idlβπ
)) β§ π΄ β πΌ) β§ (πβ(GIdβ(2nd
βπ
))) β ran
πΊ) β ((πβ(GIdβ(2nd
βπ
)))(2nd
βπ
)π΄) β πΌ) |
19 | 16, 18 | mpdan 686 |
. 2
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ π΄ β πΌ) β ((πβ(GIdβ(2nd
βπ
)))(2nd
βπ
)π΄) β πΌ) |
20 | 11, 19 | eqeltrd 2838 |
1
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ π΄ β πΌ) β (πβπ΄) β πΌ) |