Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. 2
β’
(0gβπ) = (0gβπ) |
2 | | dihp.n |
. 2
β’ π = (LSpanβπ) |
3 | | eqid 2737 |
. 2
β’
(LSAtomsβπ) =
(LSAtomsβπ) |
4 | | dihp.h |
. . 3
β’ π» = (LHypβπΎ) |
5 | | dihp.u |
. . 3
β’ π = ((DVecHβπΎ)βπ) |
6 | | dihp.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
7 | 4, 5, 6 | dvhlvec 39575 |
. 2
β’ (π β π β LVec) |
8 | | dihp.p |
. . 3
β’ π = ((ocβπΎ)βπ) |
9 | | dihp.i |
. . 3
β’ πΌ = ((DIsoHβπΎ)βπ) |
10 | 4, 8, 9, 5, 3, 6 | dihat 39801 |
. 2
β’ (π β (πΌβπ) β (LSAtomsβπ)) |
11 | | eqid 2737 |
. . . . . . . 8
β’
(leβπΎ) =
(leβπΎ) |
12 | | eqid 2737 |
. . . . . . . 8
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
13 | 11, 12, 4, 8 | lhpocnel2 38485 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) |
14 | | dihp.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
15 | | dihp.t |
. . . . . . . 8
β’ π = ((LTrnβπΎ)βπ) |
16 | | eqid 2737 |
. . . . . . . 8
β’
(β©π
β π (πβπ) = π) = (β©π β π (πβπ) = π) |
17 | 14, 11, 12, 4, 15, 16 | ltrniotaidvalN 39049 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (β©π β π (πβπ) = π) = ( I βΎ π΅)) |
18 | 6, 13, 17 | syl2anc2 586 |
. . . . . 6
β’ (π β (β©π β π (πβπ) = π) = ( I βΎ π΅)) |
19 | 18 | fveq2d 6847 |
. . . . 5
β’ (π β (πβ(β©π β π (πβπ) = π)) = (πβ( I βΎ π΅))) |
20 | | dihp.s |
. . . . . . 7
β’ (π β (π β πΈ β§ π β π)) |
21 | 20 | simpld 496 |
. . . . . 6
β’ (π β π β πΈ) |
22 | | dihp.e |
. . . . . . 7
β’ πΈ = ((TEndoβπΎ)βπ) |
23 | 14, 4, 22 | tendoid 39239 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πβ( I βΎ π΅)) = ( I βΎ π΅)) |
24 | 6, 21, 23 | syl2anc 585 |
. . . . 5
β’ (π β (πβ( I βΎ π΅)) = ( I βΎ π΅)) |
25 | 19, 24 | eqtr2d 2778 |
. . . 4
β’ (π β ( I βΎ π΅) = (πβ(β©π β π (πβπ) = π))) |
26 | 14 | fvexi 6857 |
. . . . . 6
β’ π΅ β V |
27 | | resiexg 7852 |
. . . . . 6
β’ (π΅ β V β ( I βΎ
π΅) β
V) |
28 | 26, 27 | mp1i 13 |
. . . . 5
β’ (π β ( I βΎ π΅) β V) |
29 | | eqeq1 2741 |
. . . . . . 7
β’ (π = ( I βΎ π΅) β (π = (π β(β©π β π (πβπ) = π)) β ( I βΎ π΅) = (π β(β©π β π (πβπ) = π)))) |
30 | 29 | anbi1d 631 |
. . . . . 6
β’ (π = ( I βΎ π΅) β ((π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ) β (( I βΎ π΅) = (π β(β©π β π (πβπ) = π)) β§ π β πΈ))) |
31 | | fveq1 6842 |
. . . . . . . 8
β’ (π = π β (π β(β©π β π (πβπ) = π)) = (πβ(β©π β π (πβπ) = π))) |
32 | 31 | eqeq2d 2748 |
. . . . . . 7
β’ (π = π β (( I βΎ π΅) = (π β(β©π β π (πβπ) = π)) β ( I βΎ π΅) = (πβ(β©π β π (πβπ) = π)))) |
33 | | eleq1 2826 |
. . . . . . 7
β’ (π = π β (π β πΈ β π β πΈ)) |
34 | 32, 33 | anbi12d 632 |
. . . . . 6
β’ (π = π β ((( I βΎ π΅) = (π β(β©π β π (πβπ) = π)) β§ π β πΈ) β (( I βΎ π΅) = (πβ(β©π β π (πβπ) = π)) β§ π β πΈ))) |
35 | 30, 34 | opelopabg 5496 |
. . . . 5
β’ ((( I
βΎ π΅) β V β§
π β πΈ) β (β¨( I βΎ π΅), πβ© β {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)} β (( I βΎ π΅) = (πβ(β©π β π (πβπ) = π)) β§ π β πΈ))) |
36 | 28, 21, 35 | syl2anc 585 |
. . . 4
β’ (π β (β¨( I βΎ π΅), πβ© β {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)} β (( I βΎ π΅) = (πβ(β©π β π (πβπ) = π)) β§ π β πΈ))) |
37 | 25, 21, 36 | mpbir2and 712 |
. . 3
β’ (π β β¨( I βΎ π΅), πβ© β {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)}) |
38 | | eqid 2737 |
. . . . . 6
β’
((DIsoCβπΎ)βπ) = ((DIsoCβπΎ)βπ) |
39 | 11, 12, 4, 38, 9 | dihvalcqat 39705 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (πΌβπ) = (((DIsoCβπΎ)βπ)βπ)) |
40 | 6, 13, 39 | syl2anc2 586 |
. . . 4
β’ (π β (πΌβπ) = (((DIsoCβπΎ)βπ)βπ)) |
41 | 11, 12, 4, 8, 15, 22, 38 | dicval 39642 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (((DIsoCβπΎ)βπ)βπ) = {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)}) |
42 | 6, 13, 41 | syl2anc2 586 |
. . . 4
β’ (π β (((DIsoCβπΎ)βπ)βπ) = {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)}) |
43 | 40, 42 | eqtr2d 2778 |
. . 3
β’ (π β {β¨π, π β© β£ (π = (π β(β©π β π (πβπ) = π)) β§ π β πΈ)} = (πΌβπ)) |
44 | 37, 43 | eleqtrd 2840 |
. 2
β’ (π β β¨( I βΎ π΅), πβ© β (πΌβπ)) |
45 | 20 | simprd 497 |
. . 3
β’ (π β π β π) |
46 | | dihp.o |
. . . . . . . 8
β’ π = (π β π β¦ ( I βΎ π΅)) |
47 | 14, 4, 15, 5, 1, 46 | dvh0g 39577 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β (0gβπ) = β¨( I βΎ π΅), πβ©) |
48 | 6, 47 | syl 17 |
. . . . . 6
β’ (π β (0gβπ) = β¨( I βΎ π΅), πβ©) |
49 | 48 | eqeq2d 2748 |
. . . . 5
β’ (π β (β¨( I βΎ π΅), πβ© = (0gβπ) β β¨( I βΎ π΅), πβ© = β¨( I βΎ π΅), πβ©)) |
50 | 26, 27 | ax-mp 5 |
. . . . . . 7
β’ ( I
βΎ π΅) β
V |
51 | 15 | fvexi 6857 |
. . . . . . . . 9
β’ π β V |
52 | 51 | mptex 7174 |
. . . . . . . 8
β’ (π β π β¦ ( I βΎ π΅)) β V |
53 | 46, 52 | eqeltri 2834 |
. . . . . . 7
β’ π β V |
54 | 50, 53 | opth2 5438 |
. . . . . 6
β’ (β¨(
I βΎ π΅), πβ© = β¨( I βΎ π΅), πβ© β (( I βΎ π΅) = ( I βΎ π΅) β§ π = π)) |
55 | 54 | simprbi 498 |
. . . . 5
β’ (β¨(
I βΎ π΅), πβ© = β¨( I βΎ π΅), πβ© β π = π) |
56 | 49, 55 | syl6bi 253 |
. . . 4
β’ (π β (β¨( I βΎ π΅), πβ© = (0gβπ) β π = π)) |
57 | 56 | necon3d 2965 |
. . 3
β’ (π β (π β π β β¨( I βΎ π΅), πβ© β (0gβπ))) |
58 | 45, 57 | mpd 15 |
. 2
β’ (π β β¨( I βΎ π΅), πβ© β (0gβπ)) |
59 | 1, 2, 3, 7, 10, 44, 58 | lsatel 37470 |
1
β’ (π β (πΌβπ) = (πβ{β¨( I βΎ π΅), πβ©})) |