Step | Hyp | Ref
| Expression |
1 | | xihopellsm.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
2 | | xihopellsm.x |
. . . 4
β’ (π β π β π΅) |
3 | | xihopellsm.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
4 | | xihopellsm.h |
. . . . 5
β’ π» = (LHypβπΎ) |
5 | | xihopellsm.i |
. . . . 5
β’ πΌ = ((DIsoHβπΎ)βπ) |
6 | | xihopellsm.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
7 | | eqid 2733 |
. . . . 5
β’
(LSubSpβπ) =
(LSubSpβπ) |
8 | 3, 4, 5, 6, 7 | dihlss 39763 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβπ) β (LSubSpβπ)) |
9 | 1, 2, 8 | syl2anc 585 |
. . 3
β’ (π β (πΌβπ) β (LSubSpβπ)) |
10 | | xihopellsm.y |
. . . 4
β’ (π β π β π΅) |
11 | 3, 4, 5, 6, 7 | dihlss 39763 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβπ) β (LSubSpβπ)) |
12 | 1, 10, 11 | syl2anc 585 |
. . 3
β’ (π β (πΌβπ) β (LSubSpβπ)) |
13 | | eqid 2733 |
. . . 4
β’
(+gβπ) = (+gβπ) |
14 | | xihopellsm.p |
. . . 4
β’ β =
(LSSumβπ) |
15 | 4, 6, 13, 7, 14 | dvhopellsm 39630 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΌβπ) β (LSubSpβπ) β§ (πΌβπ) β (LSubSpβπ)) β (β¨πΉ, πβ© β ((πΌβπ) β (πΌβπ)) β βπβπ‘βββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π, π‘β©(+gβπ)β¨β, π’β©)))) |
16 | 1, 9, 12, 15 | syl3anc 1372 |
. 2
β’ (π β (β¨πΉ, πβ© β ((πΌβπ) β (πΌβπ)) β βπβπ‘βββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π, π‘β©(+gβπ)β¨β, π’β©)))) |
17 | | xihopellsm.t |
. . . . . . 7
β’ π = ((LTrnβπΎ)βπ) |
18 | | xihopellsm.e |
. . . . . . 7
β’ πΈ = ((TEndoβπΎ)βπ) |
19 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ β¨π, π‘β© β (πΌβπ)) β (πΎ β HL β§ π β π»)) |
20 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ β¨π, π‘β© β (πΌβπ)) β π β π΅) |
21 | | simpr 486 |
. . . . . . 7
β’ ((π β§ β¨π, π‘β© β (πΌβπ)) β β¨π, π‘β© β (πΌβπ)) |
22 | 3, 4, 17, 18, 5, 19, 20, 21 | dihopcl 39766 |
. . . . . 6
β’ ((π β§ β¨π, π‘β© β (πΌβπ)) β (π β π β§ π‘ β πΈ)) |
23 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ β¨β, π’β© β (πΌβπ)) β (πΎ β HL β§ π β π»)) |
24 | 10 | adantr 482 |
. . . . . . 7
β’ ((π β§ β¨β, π’β© β (πΌβπ)) β π β π΅) |
25 | | simpr 486 |
. . . . . . 7
β’ ((π β§ β¨β, π’β© β (πΌβπ)) β β¨β, π’β© β (πΌβπ)) |
26 | 3, 4, 17, 18, 5, 23, 24, 25 | dihopcl 39766 |
. . . . . 6
β’ ((π β§ β¨β, π’β© β (πΌβπ)) β (β β π β§ π’ β πΈ)) |
27 | 22, 26 | anim12dan 620 |
. . . . 5
β’ ((π β§ (β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ))) β ((π β π β§ π‘ β πΈ) β§ (β β π β§ π’ β πΈ))) |
28 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((π β π β§ π‘ β πΈ) β§ (β β π β§ π’ β πΈ))) β (πΎ β HL β§ π β π»)) |
29 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ ((π β π β§ π‘ β πΈ) β§ (β β π β§ π’ β πΈ))) β (π β π β§ π‘ β πΈ)) |
30 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ ((π β π β§ π‘ β πΈ) β§ (β β π β§ π’ β πΈ))) β (β β π β§ π’ β πΈ)) |
31 | | xihopellsm.a |
. . . . . . . . 9
β’ π΄ = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) |
32 | 4, 17, 18, 31, 6, 13 | dvhopvadd2 39607 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π‘ β πΈ) β§ (β β π β§ π’ β πΈ)) β (β¨π, π‘β©(+gβπ)β¨β, π’β©) = β¨(π β β), (π‘π΄π’)β©) |
33 | 28, 29, 30, 32 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ ((π β π β§ π‘ β πΈ) β§ (β β π β§ π’ β πΈ))) β (β¨π, π‘β©(+gβπ)β¨β, π’β©) = β¨(π β β), (π‘π΄π’)β©) |
34 | 33 | eqeq2d 2744 |
. . . . . 6
β’ ((π β§ ((π β π β§ π‘ β πΈ) β§ (β β π β§ π’ β πΈ))) β (β¨πΉ, πβ© = (β¨π, π‘β©(+gβπ)β¨β, π’β©) β β¨πΉ, πβ© = β¨(π β β), (π‘π΄π’)β©)) |
35 | | vex 3451 |
. . . . . . . 8
β’ π β V |
36 | | vex 3451 |
. . . . . . . 8
β’ β β V |
37 | 35, 36 | coex 7871 |
. . . . . . 7
β’ (π β β) β V |
38 | | ovex 7394 |
. . . . . . 7
β’ (π‘π΄π’) β V |
39 | 37, 38 | opth2 5441 |
. . . . . 6
β’
(β¨πΉ, πβ© = β¨(π β β), (π‘π΄π’)β© β (πΉ = (π β β) β§ π = (π‘π΄π’))) |
40 | 34, 39 | bitrdi 287 |
. . . . 5
β’ ((π β§ ((π β π β§ π‘ β πΈ) β§ (β β π β§ π’ β πΈ))) β (β¨πΉ, πβ© = (β¨π, π‘β©(+gβπ)β¨β, π’β©) β (πΉ = (π β β) β§ π = (π‘π΄π’)))) |
41 | 27, 40 | syldan 592 |
. . . 4
β’ ((π β§ (β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ))) β (β¨πΉ, πβ© = (β¨π, π‘β©(+gβπ)β¨β, π’β©) β (πΉ = (π β β) β§ π = (π‘π΄π’)))) |
42 | 41 | pm5.32da 580 |
. . 3
β’ (π β (((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π, π‘β©(+gβπ)β¨β, π’β©)) β ((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (πΉ = (π β β) β§ π = (π‘π΄π’))))) |
43 | 42 | 4exbidv 1930 |
. 2
β’ (π β (βπβπ‘βββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π, π‘β©(+gβπ)β¨β, π’β©)) β βπβπ‘βββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (πΉ = (π β β) β§ π = (π‘π΄π’))))) |
44 | 16, 43 | bitrd 279 |
1
β’ (π β (β¨πΉ, πβ© β ((πΌβπ) β (πΌβπ)) β βπβπ‘βββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (πΉ = (π β β) β§ π = (π‘π΄π’))))) |