Step | Hyp | Ref
| Expression |
1 | | ernggrp.h |
. . . . 5
β’ π» = (LHypβπΎ) |
2 | | erngdv.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
3 | | erngdv.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
4 | | ernggrp.d |
. . . . 5
β’ π· = ((EDRingβπΎ)βπ) |
5 | | eqid 2733 |
. . . . 5
β’
(Baseβπ·) =
(Baseβπ·) |
6 | 1, 2, 3, 4, 5 | erngbase 39314 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (Baseβπ·) = πΈ) |
7 | 6 | eqcomd 2739 |
. . 3
β’ ((πΎ β HL β§ π β π») β πΈ = (Baseβπ·)) |
8 | 7 | adantr 482 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β πΈ = (Baseβπ·)) |
9 | | erngrnglem.m |
. . . 4
β’ + = (π β πΈ, π β πΈ β¦ (π β π)) |
10 | | eqid 2733 |
. . . . 5
β’
(.rβπ·) = (.rβπ·) |
11 | 1, 2, 3, 4, 10 | erngfmul 39318 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (.rβπ·) = (π β πΈ, π β πΈ β¦ (π β π))) |
12 | 9, 11 | eqtr4id 2792 |
. . 3
β’ ((πΎ β HL β§ π β π») β + =
(.rβπ·)) |
13 | 12 | adantr 482 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β + =
(.rβπ·)) |
14 | | erngdv.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
15 | | erngdv.o |
. . . . . . 7
β’ 0 = (π β π β¦ ( I βΎ π΅)) |
16 | 14, 1, 2, 3, 15 | tendo0cl 39303 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β 0 β πΈ) |
17 | 16, 6 | eleqtrrd 2837 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β 0 β (Baseβπ·)) |
18 | | erngdv.p |
. . . . . . . 8
β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) |
19 | | eqid 2733 |
. . . . . . . . 9
β’
(+gβπ·) = (+gβπ·) |
20 | 1, 2, 3, 4, 19 | erngfplus 39315 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (+gβπ·) = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))) |
21 | 18, 20 | eqtr4id 2792 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β π = (+gβπ·)) |
22 | 21 | oveqd 7378 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β ( 0 π 0 ) = ( 0 (+gβπ·) 0 )) |
23 | 14, 1, 2, 3, 15, 18 | tendo0pl 39304 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ 0 β πΈ) β ( 0 π 0 ) = 0 ) |
24 | 16, 23 | mpdan 686 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β ( 0 π 0 ) = 0 ) |
25 | 22, 24 | eqtr3d 2775 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β ( 0 (+gβπ·) 0 ) = 0 ) |
26 | | erngdv.i |
. . . . . . 7
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) |
27 | 1, 4, 14, 2, 3, 18, 15, 26 | erngdvlem1 39501 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β π· β Grp) |
28 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ·) = (0gβπ·) |
29 | 5, 19, 28 | isgrpid2 18795 |
. . . . . 6
β’ (π· β Grp β (( 0 β
(Baseβπ·) β§ (
0
(+gβπ·)
0 ) =
0 )
β (0gβπ·) = 0 )) |
30 | 27, 29 | syl 17 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (( 0 β (Baseβπ·) β§ ( 0 (+gβπ·) 0 ) = 0 ) β
(0gβπ·) =
0
)) |
31 | 17, 25, 30 | mpbi2and 711 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (0gβπ·) = 0 ) |
32 | 31 | eqcomd 2739 |
. . 3
β’ ((πΎ β HL β§ π β π») β 0 =
(0gβπ·)) |
33 | 32 | adantr 482 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β 0 =
(0gβπ·)) |
34 | 1, 4, 14, 2, 3, 18, 15, 26, 9 | erngdvlem3 39503 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β π· β Ring) |
35 | 1, 2, 3, 4, 34 | erng1lem 39500 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (1rβπ·) = ( I βΎ π)) |
36 | 35 | eqcomd 2739 |
. . 3
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) = (1rβπ·)) |
37 | 36 | adantr 482 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β ( I βΎ π) = (1rβπ·)) |
38 | 34 | adantr 482 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β π· β Ring) |
39 | | simp1l 1198 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 ) β§ (π‘ β πΈ β§ π‘ β 0 )) β (πΎ β HL β§ π β π»)) |
40 | 12 | oveqd 7378 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (π + π‘) = (π (.rβπ·)π‘)) |
41 | 39, 40 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 ) β§ (π‘ β πΈ β§ π‘ β 0 )) β (π + π‘) = (π (.rβπ·)π‘)) |
42 | | simp2l 1200 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 ) β§ (π‘ β πΈ β§ π‘ β 0 )) β π β πΈ) |
43 | | simp3l 1202 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 ) β§ (π‘ β πΈ β§ π‘ β 0 )) β π‘ β πΈ) |
44 | 1, 2, 3, 4, 10 | erngmul 39319 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ)) β (π (.rβπ·)π‘) = (π β π‘)) |
45 | 39, 42, 43, 44 | syl12anc 836 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 ) β§ (π‘ β πΈ β§ π‘ β 0 )) β (π (.rβπ·)π‘) = (π β π‘)) |
46 | 41, 45 | eqtrd 2773 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 ) β§ (π‘ β πΈ β§ π‘ β 0 )) β (π + π‘) = (π β π‘)) |
47 | 14, 1, 2, 3, 15 | tendoconid 39342 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β 0 ) β§ (π‘ β πΈ β§ π‘ β 0 )) β (π β π‘) β 0 ) |
48 | 47 | 3adant1r 1178 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 ) β§ (π‘ β πΈ β§ π‘ β 0 )) β (π β π‘) β 0 ) |
49 | 46, 48 | eqnetrd 3008 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 ) β§ (π‘ β πΈ β§ π‘ β 0 )) β (π + π‘) β 0 ) |
50 | 14, 1, 2, 3, 15 | tendo1ne0 39341 |
. . 3
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β 0 ) |
51 | 50 | adantr 482 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β ( I βΎ π) β 0 ) |
52 | | simpll 766 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 )) β (πΎ β HL β§ π β π»)) |
53 | | simplrl 776 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 )) β β β π) |
54 | | simpr 486 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 )) β (π β πΈ β§ π β 0 )) |
55 | | edlemk6.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
56 | | edlemk6.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
57 | | edlemk6.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
58 | | edlemk6.p |
. . . . 5
β’ π = ((ocβπΎ)βπ) |
59 | | edlemk6.z |
. . . . 5
β’ π = ((π β¨ (π
βπ)) β§ ((ββπ) β¨ (π
β(π β β‘(π ββ))))) |
60 | | edlemk6.y |
. . . . 5
β’ π = ((π β¨ (π
βπ)) β§ (π β¨ (π
β(π β β‘π)))) |
61 | | edlemk6.x |
. . . . 5
β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
β(π ββ)) β§ (π
βπ) β (π
βπ)) β (π§βπ) = π)) |
62 | | edlemk6.u |
. . . . 5
β’ π = (π β π β¦ if((π ββ) = β, π, π)) |
63 | 14, 55, 56, 1, 2, 57, 58, 59, 60, 61, 62, 3, 15 | cdleml6 39494 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ β β π β§ (π β πΈ β§ π β 0 )) β (π β πΈ β§ (πβ(π ββ)) = β)) |
64 | 63 | simpld 496 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ β β π β§ (π β πΈ β§ π β 0 )) β π β πΈ) |
65 | 52, 53, 54, 64 | syl3anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 )) β π β πΈ) |
66 | 12 | oveqd 7378 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (π + π ) = (π(.rβπ·)π )) |
67 | 66 | ad2antrr 725 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 )) β (π + π ) = (π(.rβπ·)π )) |
68 | | simprl 770 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 )) β π β πΈ) |
69 | 1, 2, 3, 4, 10 | erngmul 39319 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π(.rβπ·)π ) = (π β π )) |
70 | 52, 65, 68, 69 | syl12anc 836 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 )) β (π(.rβπ·)π ) = (π β π )) |
71 | 14, 55, 56, 1, 2, 57, 58, 59, 60, 61, 62, 3, 15 | cdleml8 39496 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β (π β π ) = ( I βΎ π)) |
72 | 71 | 3expa 1119 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 )) β (π β π ) = ( I βΎ π)) |
73 | 67, 70, 72 | 3eqtrd 2777 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β§ (π β πΈ β§ π β 0 )) β (π + π ) = ( I βΎ π)) |
74 | 8, 13, 33, 37, 38, 49, 51, 65, 73 | isdrngd 20249 |
1
β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β π· β DivRing) |