Step | Hyp | Ref
| Expression |
1 | | trlcoat.h |
. . . . . . . 8
β’ π» = (LHypβπΎ) |
2 | | trlcoat.t |
. . . . . . . 8
β’ π = ((LTrnβπΎ)βπ) |
3 | 1, 2 | ltrnco 39211 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (πΉ β πΊ) β π) |
4 | 3 | 3expb 1121 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β (πΉ β πΊ) β π) |
5 | | eqid 2737 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
6 | | eqid 2737 |
. . . . . . 7
β’
(0.βπΎ) =
(0.βπΎ) |
7 | | trlcoat.r |
. . . . . . 7
β’ π
= ((trLβπΎ)βπ) |
8 | 5, 6, 1, 2, 7 | trlid0b 38670 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β πΊ) β π) β ((πΉ β πΊ) = ( I βΎ (BaseβπΎ)) β (π
β(πΉ β πΊ)) = (0.βπΎ))) |
9 | 4, 8 | syldan 592 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β ((πΉ β πΊ) = ( I βΎ (BaseβπΎ)) β (π
β(πΉ β πΊ)) = (0.βπΎ))) |
10 | | coass 6222 |
. . . . . . . . . 10
β’ ((β‘πΉ β πΉ) β πΊ) = (β‘πΉ β (πΉ β πΊ)) |
11 | | simpll 766 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β (πΎ β HL β§ π β π»)) |
12 | | simplrl 776 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β πΉ β π) |
13 | 5, 1, 2 | ltrn1o 38616 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
14 | 11, 12, 13 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
15 | | f1ococnv1 6818 |
. . . . . . . . . . . 12
β’ (πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β (β‘πΉ β πΉ) = ( I βΎ (BaseβπΎ))) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β (β‘πΉ β πΉ) = ( I βΎ (BaseβπΎ))) |
17 | 16 | coeq1d 5822 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β ((β‘πΉ β πΉ) β πΊ) = (( I βΎ (BaseβπΎ)) β πΊ)) |
18 | | coeq2 5819 |
. . . . . . . . . . 11
β’ ((πΉ β πΊ) = ( I βΎ (BaseβπΎ)) β (β‘πΉ β (πΉ β πΊ)) = (β‘πΉ β ( I βΎ (BaseβπΎ)))) |
19 | 18 | adantl 483 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β (β‘πΉ β (πΉ β πΊ)) = (β‘πΉ β ( I βΎ (BaseβπΎ)))) |
20 | 10, 17, 19 | 3eqtr3a 2801 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β (( I βΎ
(BaseβπΎ)) β
πΊ) = (β‘πΉ β ( I βΎ (BaseβπΎ)))) |
21 | | simplrr 777 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β πΊ β π) |
22 | 5, 1, 2 | ltrn1o 38616 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β πΊ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
23 | 11, 21, 22 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β πΊ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
24 | | f1of 6789 |
. . . . . . . . . 10
β’ (πΊ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β πΊ:(BaseβπΎ)βΆ(BaseβπΎ)) |
25 | | fcoi2 6722 |
. . . . . . . . . 10
β’ (πΊ:(BaseβπΎ)βΆ(BaseβπΎ) β (( I βΎ (BaseβπΎ)) β πΊ) = πΊ) |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β (( I βΎ
(BaseβπΎ)) β
πΊ) = πΊ) |
27 | 1, 2 | ltrncnv 38638 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β π) |
28 | 11, 12, 27 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β β‘πΉ β π) |
29 | 5, 1, 2 | ltrn1o 38616 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ β‘πΉ β π) β β‘πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
30 | 11, 28, 29 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β β‘πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
31 | | f1of 6789 |
. . . . . . . . . 10
β’ (β‘πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β β‘πΉ:(BaseβπΎ)βΆ(BaseβπΎ)) |
32 | | fcoi1 6721 |
. . . . . . . . . 10
β’ (β‘πΉ:(BaseβπΎ)βΆ(BaseβπΎ) β (β‘πΉ β ( I βΎ (BaseβπΎ))) = β‘πΉ) |
33 | 30, 31, 32 | 3syl 18 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β (β‘πΉ β ( I βΎ (BaseβπΎ))) = β‘πΉ) |
34 | 20, 26, 33 | 3eqtr3d 2785 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β πΊ = β‘πΉ) |
35 | 34 | fveq2d 6851 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β (π
βπΊ) = (π
ββ‘πΉ)) |
36 | 1, 2, 7 | trlcnv 38657 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
ββ‘πΉ) = (π
βπΉ)) |
37 | 11, 12, 36 | syl2anc 585 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β (π
ββ‘πΉ) = (π
βπΉ)) |
38 | 35, 37 | eqtr2d 2778 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β πΊ) = ( I βΎ (BaseβπΎ))) β (π
βπΉ) = (π
βπΊ)) |
39 | 38 | ex 414 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β ((πΉ β πΊ) = ( I βΎ (BaseβπΎ)) β (π
βπΉ) = (π
βπΊ))) |
40 | 9, 39 | sylbird 260 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β ((π
β(πΉ β πΊ)) = (0.βπΎ) β (π
βπΉ) = (π
βπΊ))) |
41 | 40 | necon3d 2965 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β ((π
βπΉ) β (π
βπΊ) β (π
β(πΉ β πΊ)) β (0.βπΎ))) |
42 | | trlcoat.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
43 | 6, 42, 1, 2, 7 | trlatn0 38664 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β πΊ) β π) β ((π
β(πΉ β πΊ)) β π΄ β (π
β(πΉ β πΊ)) β (0.βπΎ))) |
44 | 4, 43 | syldan 592 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β ((π
β(πΉ β πΊ)) β π΄ β (π
β(πΉ β πΊ)) β (0.βπΎ))) |
45 | 41, 44 | sylibrd 259 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β ((π
βπΉ) β (π
βπΊ) β (π
β(πΉ β πΊ)) β π΄)) |
46 | 45 | 3impia 1118 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π
βπΉ) β (π
βπΊ)) β (π
β(πΉ β πΊ)) β π΄) |