Step | Hyp | Ref
| Expression |
1 | | ernggrp.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | erngdv.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
3 | | erngdv.e |
. . . 4
β’ πΈ = ((TEndoβπΎ)βπ) |
4 | | ernggrp.d |
. . . 4
β’ π· = ((EDRingβπΎ)βπ) |
5 | | eqid 2733 |
. . . 4
β’
(Baseβπ·) =
(Baseβπ·) |
6 | 1, 2, 3, 4, 5 | erngbase 39314 |
. . 3
β’ ((πΎ β HL β§ π β π») β (Baseβπ·) = πΈ) |
7 | 6 | eqcomd 2739 |
. 2
β’ ((πΎ β HL β§ π β π») β πΈ = (Baseβπ·)) |
8 | | erngdv.p |
. . 3
β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) |
9 | | eqid 2733 |
. . . 4
β’
(+gβπ·) = (+gβπ·) |
10 | 1, 2, 3, 4, 9 | erngfplus 39315 |
. . 3
β’ ((πΎ β HL β§ π β π») β (+gβπ·) = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))) |
11 | 8, 10 | eqtr4id 2792 |
. 2
β’ ((πΎ β HL β§ π β π») β π = (+gβπ·)) |
12 | | erngrnglem.m |
. . 3
β’ + = (π β πΈ, π β πΈ β¦ (π β π)) |
13 | | eqid 2733 |
. . . 4
β’
(.rβπ·) = (.rβπ·) |
14 | 1, 2, 3, 4, 13 | erngfmul 39318 |
. . 3
β’ ((πΎ β HL β§ π β π») β (.rβπ·) = (π β πΈ, π β πΈ β¦ (π β π))) |
15 | 12, 14 | eqtr4id 2792 |
. 2
β’ ((πΎ β HL β§ π β π») β + =
(.rβπ·)) |
16 | | erngdv.b |
. . 3
β’ π΅ = (BaseβπΎ) |
17 | | erngdv.o |
. . 3
β’ 0 = (π β π β¦ ( I βΎ π΅)) |
18 | | erngdv.i |
. . 3
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) |
19 | 1, 4, 16, 2, 3, 8,
17, 18 | erngdvlem1 39501 |
. 2
β’ ((πΎ β HL β§ π β π») β π· β Grp) |
20 | 15 | oveqd 7378 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (π + π‘) = (π (.rβπ·)π‘)) |
21 | 20 | 3ad2ant1 1134 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β πΈ) β (π + π‘) = (π (.rβπ·)π‘)) |
22 | 1, 2, 3, 4, 13 | erngmul 39319 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ)) β (π (.rβπ·)π‘) = (π β π‘)) |
23 | 22 | 3impb 1116 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β πΈ) β (π (.rβπ·)π‘) = (π β π‘)) |
24 | 21, 23 | eqtrd 2773 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β πΈ) β (π + π‘) = (π β π‘)) |
25 | 1, 3 | tendococl 39285 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β πΈ) β (π β π‘) β πΈ) |
26 | 24, 25 | eqeltrd 2834 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β πΈ) β (π + π‘) β πΈ) |
27 | | coass 6221 |
. . 3
β’ ((π β π‘) β π’) = (π β (π‘ β π’)) |
28 | 15 | oveqd 7378 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β ((π + π‘) + π’) = ((π + π‘)(.rβπ·)π’)) |
29 | 28 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β ((π + π‘) + π’) = ((π + π‘)(.rβπ·)π’)) |
30 | | simpl 484 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (πΎ β HL β§ π β π»)) |
31 | 26 | 3adant3r3 1185 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π + π‘) β πΈ) |
32 | | simpr3 1197 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β π’ β πΈ) |
33 | 1, 2, 3, 4, 13 | erngmul 39319 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π + π‘) β πΈ β§ π’ β πΈ)) β ((π + π‘)(.rβπ·)π’) = ((π + π‘) β π’)) |
34 | 30, 31, 32, 33 | syl12anc 836 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β ((π + π‘)(.rβπ·)π’) = ((π + π‘) β π’)) |
35 | 15 | oveqdr 7389 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π + π‘) = (π (.rβπ·)π‘)) |
36 | 22 | 3adantr3 1172 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π (.rβπ·)π‘) = (π β π‘)) |
37 | 35, 36 | eqtrd 2773 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π + π‘) = (π β π‘)) |
38 | 37 | coeq1d 5821 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β ((π + π‘) β π’) = ((π β π‘) β π’)) |
39 | 29, 34, 38 | 3eqtrd 2777 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β ((π + π‘) + π’) = ((π β π‘) β π’)) |
40 | 15 | oveqd 7378 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (π + (π‘ + π’)) = (π (.rβπ·)(π‘ + π’))) |
41 | 40 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π + (π‘ + π’)) = (π (.rβπ·)(π‘ + π’))) |
42 | | simpr1 1195 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β π β πΈ) |
43 | 15 | oveqdr 7389 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π‘ + π’) = (π‘(.rβπ·)π’)) |
44 | 1, 2, 3, 4, 13 | erngmul 39319 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π‘ β πΈ β§ π’ β πΈ)) β (π‘(.rβπ·)π’) = (π‘ β π’)) |
45 | 44 | 3adantr1 1170 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π‘(.rβπ·)π’) = (π‘ β π’)) |
46 | 43, 45 | eqtrd 2773 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π‘ + π’) = (π‘ β π’)) |
47 | 1, 3 | tendococl 39285 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π‘ β πΈ β§ π’ β πΈ) β (π‘ β π’) β πΈ) |
48 | 47 | 3adant3r1 1183 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π‘ β π’) β πΈ) |
49 | 46, 48 | eqeltrd 2834 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π‘ + π’) β πΈ) |
50 | 1, 2, 3, 4, 13 | erngmul 39319 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ (π‘ + π’) β πΈ)) β (π (.rβπ·)(π‘ + π’)) = (π β (π‘ + π’))) |
51 | 30, 42, 49, 50 | syl12anc 836 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π (.rβπ·)(π‘ + π’)) = (π β (π‘ + π’))) |
52 | 46 | coeq2d 5822 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π β (π‘ + π’)) = (π β (π‘ β π’))) |
53 | 41, 51, 52 | 3eqtrd 2777 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π + (π‘ + π’)) = (π β (π‘ β π’))) |
54 | 27, 39, 53 | 3eqtr4a 2799 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β ((π + π‘) + π’) = (π + (π‘ + π’))) |
55 | 1, 2, 3, 8 | tendodi1 39297 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π β (π‘ππ’)) = ((π β π‘)π(π β π’))) |
56 | 15 | oveqd 7378 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (π + (π‘ππ’)) = (π (.rβπ·)(π‘ππ’))) |
57 | 56 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π + (π‘ππ’)) = (π (.rβπ·)(π‘ππ’))) |
58 | 1, 2, 3, 8 | tendoplcl 39294 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π‘ β πΈ β§ π’ β πΈ) β (π‘ππ’) β πΈ) |
59 | 58 | 3adant3r1 1183 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π‘ππ’) β πΈ) |
60 | 1, 2, 3, 4, 13 | erngmul 39319 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ (π‘ππ’) β πΈ)) β (π (.rβπ·)(π‘ππ’)) = (π β (π‘ππ’))) |
61 | 30, 42, 59, 60 | syl12anc 836 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π (.rβπ·)(π‘ππ’)) = (π β (π‘ππ’))) |
62 | 57, 61 | eqtrd 2773 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π + (π‘ππ’)) = (π β (π‘ππ’))) |
63 | 15 | oveqdr 7389 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π + π’) = (π (.rβπ·)π’)) |
64 | 1, 2, 3, 4, 13 | erngmul 39319 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π’ β πΈ)) β (π (.rβπ·)π’) = (π β π’)) |
65 | 64 | 3adantr2 1171 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π (.rβπ·)π’) = (π β π’)) |
66 | 63, 65 | eqtrd 2773 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π + π’) = (π β π’)) |
67 | 37, 66 | oveq12d 7379 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β ((π + π‘)π(π + π’)) = ((π β π‘)π(π β π’))) |
68 | 55, 62, 67 | 3eqtr4d 2783 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π + (π‘ππ’)) = ((π + π‘)π(π + π’))) |
69 | 1, 2, 3, 8 | tendodi2 39298 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β ((π ππ‘) β π’) = ((π β π’)π(π‘ β π’))) |
70 | 15 | oveqd 7378 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β ((π ππ‘) + π’) = ((π ππ‘)(.rβπ·)π’)) |
71 | 70 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β ((π ππ‘) + π’) = ((π ππ‘)(.rβπ·)π’)) |
72 | 1, 2, 3, 8 | tendoplcl 39294 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β πΈ) β (π ππ‘) β πΈ) |
73 | 72 | 3adant3r3 1185 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β (π ππ‘) β πΈ) |
74 | 1, 2, 3, 4, 13 | erngmul 39319 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π ππ‘) β πΈ β§ π’ β πΈ)) β ((π ππ‘)(.rβπ·)π’) = ((π ππ‘) β π’)) |
75 | 30, 73, 32, 74 | syl12anc 836 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β ((π ππ‘)(.rβπ·)π’) = ((π ππ‘) β π’)) |
76 | 71, 75 | eqtrd 2773 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β ((π ππ‘) + π’) = ((π ππ‘) β π’)) |
77 | 66, 46 | oveq12d 7379 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β ((π + π’)π(π‘ + π’)) = ((π β π’)π(π‘ β π’))) |
78 | 69, 76, 77 | 3eqtr4d 2783 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π’ β πΈ)) β ((π ππ‘) + π’) = ((π + π’)π(π‘ + π’))) |
79 | 1, 2, 3 | tendoidcl 39282 |
. 2
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β πΈ) |
80 | 15 | oveqd 7378 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (( I βΎ π) + π ) = (( I βΎ π)(.rβπ·)π )) |
81 | 80 | adantr 482 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (( I βΎ π) + π ) = (( I βΎ π)(.rβπ·)π )) |
82 | | simpl 484 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πΎ β HL β§ π β π»)) |
83 | 79 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β ( I βΎ π) β πΈ) |
84 | | simpr 486 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β π β πΈ) |
85 | 1, 2, 3, 4, 13 | erngmul 39319 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (( I βΎ π) β πΈ β§ π β πΈ)) β (( I βΎ π)(.rβπ·)π ) = (( I βΎ π) β π )) |
86 | 82, 83, 84, 85 | syl12anc 836 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (( I βΎ π)(.rβπ·)π ) = (( I βΎ π) β π )) |
87 | 1, 2, 3 | tendo1mul 39283 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (( I βΎ π) β π ) = π ) |
88 | 81, 86, 87 | 3eqtrd 2777 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (( I βΎ π) + π ) = π ) |
89 | 15 | oveqd 7378 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (π + ( I βΎ π)) = (π (.rβπ·)( I βΎ π))) |
90 | 89 | adantr 482 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π + ( I βΎ π)) = (π (.rβπ·)( I βΎ π))) |
91 | 1, 2, 3, 4, 13 | erngmul 39319 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ ( I βΎ π) β πΈ)) β (π (.rβπ·)( I βΎ π)) = (π β ( I βΎ π))) |
92 | 82, 84, 83, 91 | syl12anc 836 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π (.rβπ·)( I βΎ π)) = (π β ( I βΎ π))) |
93 | 1, 2, 3 | tendo1mulr 39284 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π β ( I βΎ π)) = π ) |
94 | 90, 92, 93 | 3eqtrd 2777 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π + ( I βΎ π)) = π ) |
95 | 7, 11, 15, 19, 26, 54, 68, 78, 79, 88, 94 | isringd 20017 |
1
β’ ((πΎ β HL β§ π β π») β π· β Ring) |