Step | Hyp | Ref
| Expression |
1 | | rngcsectALTV.b |
. . 3
β’ π΅ = (BaseβπΆ) |
2 | | rngcinvALTV.n |
. . 3
β’ π = (InvβπΆ) |
3 | | rngcsectALTV.u |
. . . 4
β’ (π β π β π) |
4 | | rngcsectALTV.c |
. . . . 5
β’ πΆ = (RngCatALTVβπ) |
5 | 4 | rngccatALTV 46362 |
. . . 4
β’ (π β π β πΆ β Cat) |
6 | 3, 5 | syl 17 |
. . 3
β’ (π β πΆ β Cat) |
7 | | rngcsectALTV.x |
. . 3
β’ (π β π β π΅) |
8 | | rngcsectALTV.y |
. . 3
β’ (π β π β π΅) |
9 | | eqid 2737 |
. . 3
β’
(SectβπΆ) =
(SectβπΆ) |
10 | 1, 2, 6, 7, 8, 9 | isinv 17650 |
. 2
β’ (π β (πΉ(πππ)πΊ β (πΉ(π(SectβπΆ)π)πΊ β§ πΊ(π(SectβπΆ)π)πΉ))) |
11 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
12 | 4, 1, 3, 7, 8, 11,
9 | rngcsectALTV 46364 |
. . . . 5
β’ (π β (πΉ(π(SectβπΆ)π)πΊ β (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))))) |
13 | | df-3an 1090 |
. . . . 5
β’ ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ)))) |
14 | 12, 13 | bitrdi 287 |
. . . 4
β’ (π β (πΉ(π(SectβπΆ)π)πΊ β ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))))) |
15 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
16 | 4, 1, 3, 8, 7, 15,
9 | rngcsectALTV 46364 |
. . . . 5
β’ (π β (πΊ(π(SectβπΆ)π)πΉ β (πΊ β (π RngHomo π) β§ πΉ β (π RngHomo π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) |
17 | | 3ancoma 1099 |
. . . . . 6
β’ ((πΊ β (π RngHomo π) β§ πΉ β (π RngHomo π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))) β (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) |
18 | | df-3an 1090 |
. . . . . 6
β’ ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))) β ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) |
19 | 17, 18 | bitri 275 |
. . . . 5
β’ ((πΊ β (π RngHomo π) β§ πΉ β (π RngHomo π) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))) β ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) |
20 | 16, 19 | bitrdi 287 |
. . . 4
β’ (π β (πΊ(π(SectβπΆ)π)πΉ β ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) |
21 | 14, 20 | anbi12d 632 |
. . 3
β’ (π β ((πΉ(π(SectβπΆ)π)πΊ β§ πΊ(π(SectβπΆ)π)πΉ) β (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))))) |
22 | | anandi 675 |
. . 3
β’ ((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β ((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) |
23 | 21, 22 | bitrdi 287 |
. 2
β’ (π β ((πΉ(π(SectβπΆ)π)πΊ β§ πΊ(π(SectβπΆ)π)πΉ) β ((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))))) |
24 | | simplrl 776 |
. . . . . 6
β’
(((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β πΉ β (π RngHomo π)) |
25 | 24 | adantl 483 |
. . . . 5
β’ ((π β§ ((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β πΉ β (π RngHomo π)) |
26 | 11, 15 | rnghmf 46271 |
. . . . . . . . . 10
β’ (πΉ β (π RngHomo π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
27 | 15, 11 | rnghmf 46271 |
. . . . . . . . . 10
β’ (πΊ β (π RngHomo π) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
28 | 26, 27 | anim12i 614 |
. . . . . . . . 9
β’ ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β (πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ))) |
29 | 28 | ad2antlr 726 |
. . . . . . . 8
β’
(((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β (πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ))) |
30 | | simpr 486 |
. . . . . . . . 9
β’ ((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))) β (πΉ β πΊ) = ( I βΎ (Baseβπ))) |
31 | 30 | adantl 483 |
. . . . . . . 8
β’
(((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β (πΉ β πΊ) = ( I βΎ (Baseβπ))) |
32 | | simpr 486 |
. . . . . . . . 9
β’ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β (πΊ β πΉ) = ( I βΎ (Baseβπ))) |
33 | 32 | ad2antrl 727 |
. . . . . . . 8
β’
(((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β (πΊ β πΉ) = ( I βΎ (Baseβπ))) |
34 | 29, 31, 33 | jca32 517 |
. . . . . . 7
β’
(((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β ((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((πΉ β πΊ) = ( I βΎ (Baseβπ)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))))) |
35 | 34 | adantl 483 |
. . . . . 6
β’ ((π β§ ((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β ((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((πΉ β πΊ) = ( I βΎ (Baseβπ)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))))) |
36 | | fcof1o 7247 |
. . . . . . 7
β’ (((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((πΉ β πΊ) = ( I βΎ (Baseβπ)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ)))) β (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ β‘πΉ = πΊ)) |
37 | | eqcom 2744 |
. . . . . . . 8
β’ (β‘πΉ = πΊ β πΊ = β‘πΉ) |
38 | 37 | anbi2i 624 |
. . . . . . 7
β’ ((πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ β‘πΉ = πΊ) β (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ πΊ = β‘πΉ)) |
39 | 36, 38 | sylib 217 |
. . . . . 6
β’ (((πΉ:(Baseβπ)βΆ(Baseβπ) β§ πΊ:(Baseβπ)βΆ(Baseβπ)) β§ ((πΉ β πΊ) = ( I βΎ (Baseβπ)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ)))) β (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ πΊ = β‘πΉ)) |
40 | 35, 39 | syl 17 |
. . . . 5
β’ ((π β§ ((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ πΊ = β‘πΉ)) |
41 | | anass 470 |
. . . . 5
β’ (((πΉ β (π RngHomo π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) β§ πΊ = β‘πΉ) β (πΉ β (π RngHomo π) β§ (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ πΊ = β‘πΉ))) |
42 | 25, 40, 41 | sylanbrc 584 |
. . . 4
β’ ((π β§ ((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β ((πΉ β (π RngHomo π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) β§ πΊ = β‘πΉ)) |
43 | 11, 15 | isrngim 46276 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅) β (πΉ β (π RngIsom π) β (πΉ β (π RngHomo π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)))) |
44 | 7, 8, 43 | syl2anc 585 |
. . . . . 6
β’ (π β (πΉ β (π RngIsom π) β (πΉ β (π RngHomo π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)))) |
45 | 44 | anbi1d 631 |
. . . . 5
β’ (π β ((πΉ β (π RngIsom π) β§ πΊ = β‘πΉ) β ((πΉ β (π RngHomo π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) β§ πΊ = β‘πΉ))) |
46 | 45 | adantr 482 |
. . . 4
β’ ((π β§ ((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β ((πΉ β (π RngIsom π) β§ πΊ = β‘πΉ) β ((πΉ β (π RngHomo π) β§ πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) β§ πΊ = β‘πΉ))) |
47 | 42, 46 | mpbird 257 |
. . 3
β’ ((π β§ ((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) β (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) |
48 | 11, 15 | rngimrnghm 46278 |
. . . . . 6
β’ (πΉ β (π RngIsom π) β πΉ β (π RngHomo π)) |
49 | 48 | ad2antrl 727 |
. . . . 5
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β πΉ β (π RngHomo π)) |
50 | | isrngisom 46268 |
. . . . . . . . . . 11
β’ ((π β π΅ β§ π β π΅) β (πΉ β (π RngIsom π) β (πΉ β (π RngHomo π) β§ β‘πΉ β (π RngHomo π)))) |
51 | 7, 8, 50 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (πΉ β (π RngIsom π) β (πΉ β (π RngHomo π) β§ β‘πΉ β (π RngHomo π)))) |
52 | | eleq1 2826 |
. . . . . . . . . . . 12
β’ (β‘πΉ = πΊ β (β‘πΉ β (π RngHomo π) β πΊ β (π RngHomo π))) |
53 | 52 | eqcoms 2745 |
. . . . . . . . . . 11
β’ (πΊ = β‘πΉ β (β‘πΉ β (π RngHomo π) β πΊ β (π RngHomo π))) |
54 | 53 | anbi2d 630 |
. . . . . . . . . 10
β’ (πΊ = β‘πΉ β ((πΉ β (π RngHomo π) β§ β‘πΉ β (π RngHomo π)) β (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)))) |
55 | 51, 54 | sylan9bbr 512 |
. . . . . . . . 9
β’ ((πΊ = β‘πΉ β§ π) β (πΉ β (π RngIsom π) β (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)))) |
56 | | simpr 486 |
. . . . . . . . 9
β’ ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β πΊ β (π RngHomo π)) |
57 | 55, 56 | syl6bi 253 |
. . . . . . . 8
β’ ((πΊ = β‘πΉ β§ π) β (πΉ β (π RngIsom π) β πΊ β (π RngHomo π))) |
58 | 57 | com12 32 |
. . . . . . 7
β’ (πΉ β (π RngIsom π) β ((πΊ = β‘πΉ β§ π) β πΊ β (π RngHomo π))) |
59 | 58 | expdimp 454 |
. . . . . 6
β’ ((πΉ β (π RngIsom π) β§ πΊ = β‘πΉ) β (π β πΊ β (π RngHomo π))) |
60 | 59 | impcom 409 |
. . . . 5
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β πΊ β (π RngHomo π)) |
61 | | coeq1 5818 |
. . . . . . 7
β’ (πΊ = β‘πΉ β (πΊ β πΉ) = (β‘πΉ β πΉ)) |
62 | 61 | ad2antll 728 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β (πΊ β πΉ) = (β‘πΉ β πΉ)) |
63 | 11, 15 | rngimf1o 46277 |
. . . . . . . 8
β’ (πΉ β (π RngIsom π) β πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) |
64 | 63 | ad2antrl 727 |
. . . . . . 7
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ)) |
65 | | f1ococnv1 6818 |
. . . . . . 7
β’ (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β (β‘πΉ β πΉ) = ( I βΎ (Baseβπ))) |
66 | 64, 65 | syl 17 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β (β‘πΉ β πΉ) = ( I βΎ (Baseβπ))) |
67 | 62, 66 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β (πΊ β πΉ) = ( I βΎ (Baseβπ))) |
68 | 49, 60, 67 | jca31 516 |
. . . 4
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ)))) |
69 | 51 | biimpcd 249 |
. . . . . . 7
β’ (πΉ β (π RngIsom π) β (π β (πΉ β (π RngHomo π) β§ β‘πΉ β (π RngHomo π)))) |
70 | 69 | adantr 482 |
. . . . . 6
β’ ((πΉ β (π RngIsom π) β§ πΊ = β‘πΉ) β (π β (πΉ β (π RngHomo π) β§ β‘πΉ β (π RngHomo π)))) |
71 | 70 | impcom 409 |
. . . . 5
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β (πΉ β (π RngHomo π) β§ β‘πΉ β (π RngHomo π))) |
72 | | eleq1 2826 |
. . . . . . 7
β’ (πΊ = β‘πΉ β (πΊ β (π RngHomo π) β β‘πΉ β (π RngHomo π))) |
73 | 72 | ad2antll 728 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β (πΊ β (π RngHomo π) β β‘πΉ β (π RngHomo π))) |
74 | 73 | anbi2d 630 |
. . . . 5
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β ((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β (πΉ β (π RngHomo π) β§ β‘πΉ β (π RngHomo π)))) |
75 | 71, 74 | mpbird 257 |
. . . 4
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) |
76 | | coeq2 5819 |
. . . . . . 7
β’ (πΊ = β‘πΉ β (πΉ β πΊ) = (πΉ β β‘πΉ)) |
77 | 76 | ad2antll 728 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β (πΉ β πΊ) = (πΉ β β‘πΉ)) |
78 | | f1ococnv2 6816 |
. . . . . . 7
β’ (πΉ:(Baseβπ)β1-1-ontoβ(Baseβπ) β (πΉ β β‘πΉ) = ( I βΎ (Baseβπ))) |
79 | 64, 78 | syl 17 |
. . . . . 6
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β (πΉ β β‘πΉ) = ( I βΎ (Baseβπ))) |
80 | 77, 79 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β (πΉ β πΊ) = ( I βΎ (Baseβπ))) |
81 | 75, 67, 80 | jca31 516 |
. . . 4
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) |
82 | 68, 75, 81 | jca31 516 |
. . 3
β’ ((π β§ (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ)) β ((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ))))) |
83 | 47, 82 | impbida 800 |
. 2
β’ (π β (((((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π))) β§ (((πΉ β (π RngHomo π) β§ πΊ β (π RngHomo π)) β§ (πΊ β πΉ) = ( I βΎ (Baseβπ))) β§ (πΉ β πΊ) = ( I βΎ (Baseβπ)))) β (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ))) |
84 | 10, 23, 83 | 3bitrd 305 |
1
β’ (π β (πΉ(πππ)πΊ β (πΉ β (π RngIsom π) β§ πΊ = β‘πΉ))) |