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