Step | Hyp | Ref
| Expression |
1 | | idlsubcl.1 |
. . . . 5
β’ πΊ = (1st βπ
) |
2 | | eqid 2737 |
. . . . 5
β’ ran πΊ = ran πΊ |
3 | 1, 2 | idlcl 36479 |
. . . 4
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ π΄ β πΌ) β π΄ β ran πΊ) |
4 | 1, 2 | idlcl 36479 |
. . . 4
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ π΅ β πΌ) β π΅ β ran πΊ) |
5 | 3, 4 | anim12dan 620 |
. . 3
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ (π΄ β πΌ β§ π΅ β πΌ)) β (π΄ β ran πΊ β§ π΅ β ran πΊ)) |
6 | | eqid 2737 |
. . . . . 6
β’
(invβπΊ) =
(invβπΊ) |
7 | | idlsubcl.2 |
. . . . . 6
β’ π· = ( /π
βπΊ) |
8 | 1, 2, 6, 7 | rngosub 36392 |
. . . . 5
β’ ((π
β RingOps β§ π΄ β ran πΊ β§ π΅ β ran πΊ) β (π΄π·π΅) = (π΄πΊ((invβπΊ)βπ΅))) |
9 | 8 | 3expb 1121 |
. . . 4
β’ ((π
β RingOps β§ (π΄ β ran πΊ β§ π΅ β ran πΊ)) β (π΄π·π΅) = (π΄πΊ((invβπΊ)βπ΅))) |
10 | 9 | adantlr 714 |
. . 3
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ (π΄ β ran πΊ β§ π΅ β ran πΊ)) β (π΄π·π΅) = (π΄πΊ((invβπΊ)βπ΅))) |
11 | 5, 10 | syldan 592 |
. 2
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ (π΄ β πΌ β§ π΅ β πΌ)) β (π΄π·π΅) = (π΄πΊ((invβπΊ)βπ΅))) |
12 | | simprl 770 |
. . . 4
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ (π΄ β πΌ β§ π΅ β πΌ)) β π΄ β πΌ) |
13 | 1, 6 | idlnegcl 36484 |
. . . . 5
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ π΅ β πΌ) β ((invβπΊ)βπ΅) β πΌ) |
14 | 13 | adantrl 715 |
. . . 4
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ (π΄ β πΌ β§ π΅ β πΌ)) β ((invβπΊ)βπ΅) β πΌ) |
15 | 12, 14 | jca 513 |
. . 3
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ (π΄ β πΌ β§ π΅ β πΌ)) β (π΄ β πΌ β§ ((invβπΊ)βπ΅) β πΌ)) |
16 | 1 | idladdcl 36481 |
. . 3
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ (π΄ β πΌ β§ ((invβπΊ)βπ΅) β πΌ)) β (π΄πΊ((invβπΊ)βπ΅)) β πΌ) |
17 | 15, 16 | syldan 592 |
. 2
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ (π΄ β πΌ β§ π΅ β πΌ)) β (π΄πΊ((invβπΊ)βπ΅)) β πΌ) |
18 | 11, 17 | eqeltrd 2838 |
1
β’ (((π
β RingOps β§ πΌ β (Idlβπ
)) β§ (π΄ β πΌ β§ π΅ β πΌ)) β (π΄π·π΅) β πΌ) |