Step | Hyp | Ref
| Expression |
1 | | cdlemn8.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | cdlemn8.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | cdlemn8.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
4 | | cdlemn8.h |
. . . 4
β’ π» = (LHypβπΎ) |
5 | | cdlemn8.p |
. . . 4
β’ π = ((ocβπΎ)βπ) |
6 | | cdlemn8.o |
. . . 4
β’ π = (β β π β¦ ( I βΎ π΅)) |
7 | | cdlemn8.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
8 | | cdlemn8.e |
. . . 4
β’ πΈ = ((TEndoβπΎ)βπ) |
9 | | cdlemn8.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
10 | | cdlemn8.s |
. . . 4
β’ + =
(+gβπ) |
11 | | cdlemn8.f |
. . . 4
β’ πΉ = (β©β β π (ββπ) = π) |
12 | | cdlemn8.g |
. . . 4
β’ πΊ = (β©β β π (ββπ) = π
) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | cdlemn8 40587 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β π = (πΊ β β‘πΉ)) |
14 | 13 | fveq1d 6886 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β (πβπ) = ((πΊ β β‘πΉ)βπ)) |
15 | | simp1 1133 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β (πΎ β HL β§ π β π»)) |
16 | 2, 3, 4, 5 | lhpocnel2 39402 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β (π β π΄ β§ Β¬ π β€ π)) |
17 | 16 | 3ad2ant1 1130 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β (π β π΄ β§ Β¬ π β€ π)) |
18 | | simp2l 1196 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β (π β π΄ β§ Β¬ π β€ π)) |
19 | 2, 3, 4, 7, 11 | ltrniotacl 39962 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) |
20 | 15, 17, 18, 19 | syl3anc 1368 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β πΉ β π) |
21 | 1, 4, 7 | ltrn1o 39507 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ:π΅β1-1-ontoβπ΅) |
22 | 15, 20, 21 | syl2anc 583 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β πΉ:π΅β1-1-ontoβπ΅) |
23 | | f1ocnv 6838 |
. . . 4
β’ (πΉ:π΅β1-1-ontoβπ΅ β β‘πΉ:π΅β1-1-ontoβπ΅) |
24 | | f1of 6826 |
. . . 4
β’ (β‘πΉ:π΅β1-1-ontoβπ΅ β β‘πΉ:π΅βΆπ΅) |
25 | 22, 23, 24 | 3syl 18 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β β‘πΉ:π΅βΆπ΅) |
26 | | simp2ll 1237 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β π β π΄) |
27 | 1, 3 | atbase 38671 |
. . . 4
β’ (π β π΄ β π β π΅) |
28 | 26, 27 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β π β π΅) |
29 | | fvco3 6983 |
. . 3
β’ ((β‘πΉ:π΅βΆπ΅ β§ π β π΅) β ((πΊ β β‘πΉ)βπ) = (πΊβ(β‘πΉβπ))) |
30 | 25, 28, 29 | syl2anc 583 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β ((πΊ β β‘πΉ)βπ) = (πΊβ(β‘πΉβπ))) |
31 | 2, 3, 4, 7, 11 | ltrniotacnvval 39965 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (β‘πΉβπ) = π) |
32 | 15, 17, 18, 31 | syl3anc 1368 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β (β‘πΉβπ) = π) |
33 | 32 | fveq2d 6888 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β (πΊβ(β‘πΉβπ)) = (πΊβπ)) |
34 | | simp2r 1197 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β (π
β π΄ β§ Β¬ π
β€ π)) |
35 | 2, 3, 4, 7, 12 | ltrniotaval 39964 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (πΊβπ) = π
) |
36 | 15, 17, 34, 35 | syl3anc 1368 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β (πΊβπ) = π
) |
37 | 33, 36 | eqtrd 2766 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β (πΊβ(β‘πΉβπ)) = π
) |
38 | 14, 30, 37 | 3eqtrd 2770 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π β§ β¨πΊ, ( I βΎ π)β© = (β¨(π βπΉ), π β© + β¨π, πβ©))) β (πβπ) = π
) |