Step | Hyp | Ref
| Expression |
1 | | simprr 772 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β π β πΈ) |
2 | | dvhop.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
3 | | dvhop.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
4 | | dvhop.t |
. . . . . . 7
β’ π = ((LTrnβπΎ)βπ) |
5 | 2, 3, 4 | idltrn 38616 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β ( I βΎ π΅) β π) |
6 | 5 | adantr 482 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β ( I βΎ π΅) β π) |
7 | | dvhop.e |
. . . . . . 7
β’ πΈ = ((TEndoβπΎ)βπ) |
8 | 3, 4, 7 | tendoidcl 39235 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β πΈ) |
9 | 8 | adantr 482 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β ( I βΎ π) β πΈ) |
10 | | dvhop.s |
. . . . . 6
β’ π = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) |
11 | 10 | dvhopspN 39581 |
. . . . 5
β’ ((π β πΈ β§ (( I βΎ π΅) β π β§ ( I βΎ π) β πΈ)) β (ππβ¨( I βΎ π΅), ( I βΎ π)β©) = β¨(πβ( I βΎ π΅)), (π β ( I βΎ π))β©) |
12 | 1, 6, 9, 11 | syl12anc 836 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β (ππβ¨( I βΎ π΅), ( I βΎ π)β©) = β¨(πβ( I βΎ π΅)), (π β ( I βΎ π))β©) |
13 | 2, 3, 7 | tendoid 39239 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πβ( I βΎ π΅)) = ( I βΎ π΅)) |
14 | 13 | adantrl 715 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β (πβ( I βΎ π΅)) = ( I βΎ π΅)) |
15 | 3, 4, 7 | tendo1mulr 39237 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π β ( I βΎ π)) = π) |
16 | 15 | adantrl 715 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β (π β ( I βΎ π)) = π) |
17 | 14, 16 | opeq12d 4839 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β β¨(πβ( I βΎ π΅)), (π β ( I βΎ π))β© = β¨( I βΎ π΅), πβ©) |
18 | 12, 17 | eqtrd 2777 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β (ππβ¨( I βΎ π΅), ( I βΎ π)β©) = β¨( I βΎ π΅), πβ©) |
19 | 18 | oveq2d 7374 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β (β¨πΉ, πβ©π΄(ππβ¨( I βΎ π΅), ( I βΎ π)β©)) = (β¨πΉ, πβ©π΄β¨( I βΎ π΅), πβ©)) |
20 | | simprl 770 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β πΉ β π) |
21 | | dvhop.o |
. . . . 5
β’ π = (π β π β¦ ( I βΎ π΅)) |
22 | 2, 3, 4, 7, 21 | tendo0cl 39256 |
. . . 4
β’ ((πΎ β HL β§ π β π») β π β πΈ) |
23 | 22 | adantr 482 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β π β πΈ) |
24 | | dvhop.a |
. . . 4
β’ π΄ = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st
βπ) β
(1st βπ)),
((2nd βπ)π(2nd βπ))β©) |
25 | 24 | dvhopaddN 39580 |
. . 3
β’ (((πΉ β π β§ π β πΈ) β§ (( I βΎ π΅) β π β§ π β πΈ)) β (β¨πΉ, πβ©π΄β¨( I βΎ π΅), πβ©) = β¨(πΉ β ( I βΎ π΅)), (πππ)β©) |
26 | 20, 23, 6, 1, 25 | syl22anc 838 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β (β¨πΉ, πβ©π΄β¨( I βΎ π΅), πβ©) = β¨(πΉ β ( I βΎ π΅)), (πππ)β©) |
27 | 2, 3, 4 | ltrn1o 38590 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ:π΅β1-1-ontoβπ΅) |
28 | 27 | adantrr 716 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β πΉ:π΅β1-1-ontoβπ΅) |
29 | | f1of 6785 |
. . . 4
β’ (πΉ:π΅β1-1-ontoβπ΅ β πΉ:π΅βΆπ΅) |
30 | | fcoi1 6717 |
. . . 4
β’ (πΉ:π΅βΆπ΅ β (πΉ β ( I βΎ π΅)) = πΉ) |
31 | 28, 29, 30 | 3syl 18 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β (πΉ β ( I βΎ π΅)) = πΉ) |
32 | | dvhop.p |
. . . . 5
β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) |
33 | 2, 3, 4, 7, 21, 32 | tendo0pl 39257 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πππ) = π) |
34 | 33 | adantrl 715 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β (πππ) = π) |
35 | 31, 34 | opeq12d 4839 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β β¨(πΉ β ( I βΎ π΅)), (πππ)β© = β¨πΉ, πβ©) |
36 | 19, 26, 35 | 3eqtrrd 2782 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β β¨πΉ, πβ© = (β¨πΉ, πβ©π΄(ππβ¨( I βΎ π΅), ( I βΎ π)β©))) |