Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | ernggrp.h-r |
. . 3
β’ π» = (LHypβπΎ) |
3 | | eqid 2733 |
. . 3
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
4 | 1, 2, 3 | cdlemftr0 39081 |
. 2
β’ ((πΎ β HL β§ π β π») β βπ β ((LTrnβπΎ)βπ)π β ( I βΎ (BaseβπΎ))) |
5 | | ernggrp.d-r |
. . 3
β’ π· =
((EDRingRβπΎ)βπ) |
6 | | eqid 2733 |
. . 3
β’
((TEndoβπΎ)βπ) = ((TEndoβπΎ)βπ) |
7 | | eqid 2733 |
. . 3
β’ (π β ((TEndoβπΎ)βπ), π β ((TEndoβπΎ)βπ) β¦ (π β ((LTrnβπΎ)βπ) β¦ ((πβπ) β (πβπ)))) = (π β ((TEndoβπΎ)βπ), π β ((TEndoβπΎ)βπ) β¦ (π β ((LTrnβπΎ)βπ) β¦ ((πβπ) β (πβπ)))) |
8 | | eqid 2733 |
. . 3
β’ (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))) = (π β ((LTrnβπΎ)βπ) β¦ ( I βΎ (BaseβπΎ))) |
9 | | eqid 2733 |
. . 3
β’ (π β ((TEndoβπΎ)βπ) β¦ (π β ((LTrnβπΎ)βπ) β¦ β‘(πβπ))) = (π β ((TEndoβπΎ)βπ) β¦ (π β ((LTrnβπΎ)βπ) β¦ β‘(πβπ))) |
10 | | eqid 2733 |
. . 3
β’ (π β ((TEndoβπΎ)βπ), π β ((TEndoβπΎ)βπ) β¦ (π β π)) = (π β ((TEndoβπΎ)βπ), π β ((TEndoβπΎ)βπ) β¦ (π β π)) |
11 | | eqid 2733 |
. . 3
β’
(joinβπΎ) =
(joinβπΎ) |
12 | | eqid 2733 |
. . 3
β’
(meetβπΎ) =
(meetβπΎ) |
13 | | eqid 2733 |
. . 3
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
14 | | eqid 2733 |
. . 3
β’
((ocβπΎ)βπ) = ((ocβπΎ)βπ) |
15 | | eqid 2733 |
. . 3
β’
((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘(π βπ))))) = ((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘(π βπ))))) |
16 | | eqid 2733 |
. . 3
β’
((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘(π βπ)))))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘π)))) = ((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘(π βπ)))))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘π)))) |
17 | | eqid 2733 |
. . 3
β’
(β©π§
β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)((π β ( I βΎ (BaseβπΎ)) β§ (((trLβπΎ)βπ)βπ) β (((trLβπΎ)βπ)β(π βπ)) β§ (((trLβπΎ)βπ)βπ) β (((trLβπΎ)βπ)βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘(π βπ)))))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘π)))))) = (β©π§ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)((π β ( I βΎ (BaseβπΎ)) β§ (((trLβπΎ)βπ)βπ) β (((trLβπΎ)βπ)β(π βπ)) β§ (((trLβπΎ)βπ)βπ) β (((trLβπΎ)βπ)βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘(π βπ)))))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘π)))))) |
18 | | eqid 2733 |
. . 3
β’ (π β ((LTrnβπΎ)βπ) β¦ if((π βπ) = π, π, (β©π§ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)((π β ( I βΎ (BaseβπΎ)) β§ (((trLβπΎ)βπ)βπ) β (((trLβπΎ)βπ)β(π βπ)) β§ (((trLβπΎ)βπ)βπ) β (((trLβπΎ)βπ)βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘(π βπ)))))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘π)))))))) = (π β ((LTrnβπΎ)βπ) β¦ if((π βπ) = π, π, (β©π§ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)((π β ( I βΎ (BaseβπΎ)) β§ (((trLβπΎ)βπ)βπ) β (((trLβπΎ)βπ)β(π βπ)) β§ (((trLβπΎ)βπ)βπ) β (((trLβπΎ)βπ)βπ)) β (π§β((ocβπΎ)βπ)) = ((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)(((((ocβπΎ)βπ)(joinβπΎ)(((trLβπΎ)βπ)βπ))(meetβπΎ)((πβ((ocβπΎ)βπ))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘(π βπ)))))(joinβπΎ)(((trLβπΎ)βπ)β(π β β‘π)))))))) |
19 | 2, 5, 1, 3, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18 | erngdvlem4-rN 39512 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β ((LTrnβπΎ)βπ) β§ π β ( I βΎ (BaseβπΎ)))) β π· β DivRing) |
20 | 4, 19 | rexlimddv 3155 |
1
β’ ((πΎ β HL β§ π β π») β π· β DivRing) |