Step | Hyp | Ref
| Expression |
1 | | diblsmopel.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
2 | | diblsmopel.x |
. . . 4
β’ (π β (π β π΅ β§ π β€ π)) |
3 | | diblsmopel.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
4 | | diblsmopel.l |
. . . . 5
β’ β€ =
(leβπΎ) |
5 | | diblsmopel.h |
. . . . 5
β’ π» = (LHypβπΎ) |
6 | | diblsmopel.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
7 | | diblsmopel.i |
. . . . 5
β’ πΌ = ((DIsoBβπΎ)βπ) |
8 | | eqid 2733 |
. . . . 5
β’
(LSubSpβπ) =
(LSubSpβπ) |
9 | 3, 4, 5, 6, 7, 8 | diblss 39683 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) β (LSubSpβπ)) |
10 | 1, 2, 9 | syl2anc 585 |
. . 3
β’ (π β (πΌβπ) β (LSubSpβπ)) |
11 | | diblsmopel.y |
. . . 4
β’ (π β (π β π΅ β§ π β€ π)) |
12 | 3, 4, 5, 6, 7, 8 | diblss 39683 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) β (LSubSpβπ)) |
13 | 1, 11, 12 | syl2anc 585 |
. . 3
β’ (π β (πΌβπ) β (LSubSpβπ)) |
14 | | eqid 2733 |
. . . 4
β’
(+gβπ) = (+gβπ) |
15 | | diblsmopel.p |
. . . 4
β’ β =
(LSSumβπ) |
16 | 5, 6, 14, 8, 15 | dvhopellsm 39630 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΌβπ) β (LSubSpβπ) β§ (πΌβπ) β (LSubSpβπ)) β (β¨πΉ, πβ© β ((πΌβπ) β (πΌβπ)) β βπ₯βπ¦βπ§βπ€((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)))) |
17 | 1, 10, 13, 16 | syl3anc 1372 |
. 2
β’ (π β (β¨πΉ, πβ© β ((πΌβπ) β (πΌβπ)) β βπ₯βπ¦βπ§βπ€((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)))) |
18 | | excom 2163 |
. . . 4
β’
(βπ¦βπ§βπ€((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)) β βπ§βπ¦βπ€((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©))) |
19 | | diblsmopel.t |
. . . . . . . . . . . . 13
β’ π = ((LTrnβπΎ)βπ) |
20 | | diblsmopel.o |
. . . . . . . . . . . . 13
β’ π = (π β π β¦ ( I βΎ π΅)) |
21 | | diblsmopel.j |
. . . . . . . . . . . . 13
β’ π½ = ((DIsoAβπΎ)βπ) |
22 | 3, 4, 5, 19, 20, 21, 7 | dibopelval2 39658 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (β¨π₯, π¦β© β (πΌβπ) β (π₯ β (π½βπ) β§ π¦ = π))) |
23 | 1, 2, 22 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (β¨π₯, π¦β© β (πΌβπ) β (π₯ β (π½βπ) β§ π¦ = π))) |
24 | 3, 4, 5, 19, 20, 21, 7 | dibopelval2 39658 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (β¨π§, π€β© β (πΌβπ) β (π§ β (π½βπ) β§ π€ = π))) |
25 | 1, 11, 24 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (β¨π§, π€β© β (πΌβπ) β (π§ β (π½βπ) β§ π€ = π))) |
26 | 23, 25 | anbi12d 632 |
. . . . . . . . . 10
β’ (π β ((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β ((π₯ β (π½βπ) β§ π¦ = π) β§ (π§ β (π½βπ) β§ π€ = π)))) |
27 | | an4 655 |
. . . . . . . . . . 11
β’ (((π₯ β (π½βπ) β§ π¦ = π) β§ (π§ β (π½βπ) β§ π€ = π)) β ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (π¦ = π β§ π€ = π))) |
28 | | ancom 462 |
. . . . . . . . . . 11
β’ (((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (π¦ = π β§ π€ = π)) β ((π¦ = π β§ π€ = π) β§ (π₯ β (π½βπ) β§ π§ β (π½βπ)))) |
29 | 27, 28 | bitri 275 |
. . . . . . . . . 10
β’ (((π₯ β (π½βπ) β§ π¦ = π) β§ (π§ β (π½βπ) β§ π€ = π)) β ((π¦ = π β§ π€ = π) β§ (π₯ β (π½βπ) β§ π§ β (π½βπ)))) |
30 | 26, 29 | bitrdi 287 |
. . . . . . . . 9
β’ (π β ((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β ((π¦ = π β§ π€ = π) β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))))) |
31 | 30 | anbi1d 631 |
. . . . . . . 8
β’ (π β (((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)) β (((π¦ = π β§ π€ = π) β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)))) |
32 | | anass 470 |
. . . . . . . . 9
β’ ((((π¦ = π β§ π€ = π) β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)) β ((π¦ = π β§ π€ = π) β§ ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)))) |
33 | | df-3an 1090 |
. . . . . . . . 9
β’ ((π¦ = π β§ π€ = π β§ ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©))) β ((π¦ = π β§ π€ = π) β§ ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)))) |
34 | 32, 33 | bitr4i 278 |
. . . . . . . 8
β’ ((((π¦ = π β§ π€ = π) β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)) β (π¦ = π β§ π€ = π β§ ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)))) |
35 | 31, 34 | bitrdi 287 |
. . . . . . 7
β’ (π β (((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)) β (π¦ = π β§ π€ = π β§ ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©))))) |
36 | 35 | 2exbidv 1928 |
. . . . . 6
β’ (π β (βπ¦βπ€((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)) β βπ¦βπ€(π¦ = π β§ π€ = π β§ ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©))))) |
37 | 19 | fvexi 6860 |
. . . . . . . . . 10
β’ π β V |
38 | 37 | mptex 7177 |
. . . . . . . . 9
β’ (π β π β¦ ( I βΎ π΅)) β V |
39 | 20, 38 | eqeltri 2830 |
. . . . . . . 8
β’ π β V |
40 | | opeq2 4835 |
. . . . . . . . . . 11
β’ (π¦ = π β β¨π₯, π¦β© = β¨π₯, πβ©) |
41 | 40 | oveq1d 7376 |
. . . . . . . . . 10
β’ (π¦ = π β (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©) = (β¨π₯, πβ©(+gβπ)β¨π§, π€β©)) |
42 | 41 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π¦ = π β (β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©) β β¨πΉ, πβ© = (β¨π₯, πβ©(+gβπ)β¨π§, π€β©))) |
43 | 42 | anbi2d 630 |
. . . . . . . 8
β’ (π¦ = π β (((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)) β ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, πβ©(+gβπ)β¨π§, π€β©)))) |
44 | | opeq2 4835 |
. . . . . . . . . . 11
β’ (π€ = π β β¨π§, π€β© = β¨π§, πβ©) |
45 | 44 | oveq2d 7377 |
. . . . . . . . . 10
β’ (π€ = π β (β¨π₯, πβ©(+gβπ)β¨π§, π€β©) = (β¨π₯, πβ©(+gβπ)β¨π§, πβ©)) |
46 | 45 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π€ = π β (β¨πΉ, πβ© = (β¨π₯, πβ©(+gβπ)β¨π§, π€β©) β β¨πΉ, πβ© = (β¨π₯, πβ©(+gβπ)β¨π§, πβ©))) |
47 | 46 | anbi2d 630 |
. . . . . . . 8
β’ (π€ = π β (((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, πβ©(+gβπ)β¨π§, π€β©)) β ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, πβ©(+gβπ)β¨π§, πβ©)))) |
48 | 39, 39, 43, 47 | ceqsex2v 3501 |
. . . . . . 7
β’
(βπ¦βπ€(π¦ = π β§ π€ = π β§ ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©))) β ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, πβ©(+gβπ)β¨π§, πβ©))) |
49 | 1 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (πΎ β HL β§ π β π»)) |
50 | 2 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (π β π΅ β§ π β€ π)) |
51 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β π₯ β (π½βπ)) |
52 | 3, 4, 5, 19, 21 | diael 39556 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ π₯ β (π½βπ)) β π₯ β π) |
53 | 49, 50, 51, 52 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β π₯ β π) |
54 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
((TEndoβπΎ)βπ) = ((TEndoβπΎ)βπ) |
55 | 3, 5, 19, 54, 20 | tendo0cl 39303 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π») β π β ((TEndoβπΎ)βπ)) |
56 | 49, 55 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β π β ((TEndoβπΎ)βπ)) |
57 | 11 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (π β π΅ β§ π β€ π)) |
58 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β π§ β (π½βπ)) |
59 | 3, 4, 5, 19, 21 | diael 39556 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ π§ β (π½βπ)) β π§ β π) |
60 | 49, 57, 58, 59 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β π§ β π) |
61 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Scalarβπ) =
(Scalarβπ) |
62 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
63 | 5, 19, 54, 6, 61, 14, 62 | dvhopvadd 39606 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (π₯ β π β§ π β ((TEndoβπΎ)βπ)) β§ (π§ β π β§ π β ((TEndoβπΎ)βπ))) β (β¨π₯, πβ©(+gβπ)β¨π§, πβ©) = β¨(π₯ β π§), (π(+gβ(Scalarβπ))π)β©) |
64 | 49, 53, 56, 60, 56, 63 | syl122anc 1380 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (β¨π₯, πβ©(+gβπ)β¨π§, πβ©) = β¨(π₯ β π§), (π(+gβ(Scalarβπ))π)β©) |
65 | 64 | eqeq2d 2744 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (β¨πΉ, πβ© = (β¨π₯, πβ©(+gβπ)β¨π§, πβ©) β β¨πΉ, πβ© = β¨(π₯ β π§), (π(+gβ(Scalarβπ))π)β©)) |
66 | | vex 3451 |
. . . . . . . . . . . 12
β’ π₯ β V |
67 | | vex 3451 |
. . . . . . . . . . . 12
β’ π§ β V |
68 | 66, 67 | coex 7871 |
. . . . . . . . . . 11
β’ (π₯ β π§) β V |
69 | | ovex 7394 |
. . . . . . . . . . 11
β’ (π(+gβ(Scalarβπ))π) β V |
70 | 68, 69 | opth2 5441 |
. . . . . . . . . 10
β’
(β¨πΉ, πβ© = β¨(π₯ β π§), (π(+gβ(Scalarβπ))π)β© β (πΉ = (π₯ β π§) β§ π = (π(+gβ(Scalarβπ))π))) |
71 | | diblsmopel.v |
. . . . . . . . . . . . . . 15
β’ π = ((DVecAβπΎ)βπ) |
72 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(+gβπ) = (+gβπ) |
73 | 5, 19, 71, 72 | dvavadd 39528 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ (π₯ β π β§ π§ β π)) β (π₯(+gβπ)π§) = (π₯ β π§)) |
74 | 49, 53, 60, 73 | syl12anc 836 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (π₯(+gβπ)π§) = (π₯ β π§)) |
75 | 74 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (πΉ = (π₯(+gβπ)π§) β πΉ = (π₯ β π§))) |
76 | 75 | bicomd 222 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (πΉ = (π₯ β π§) β πΉ = (π₯(+gβπ)π§))) |
77 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) = (π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) |
78 | 5, 19, 54, 6, 61, 77, 62 | dvhfplusr 39597 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β HL β§ π β π») β
(+gβ(Scalarβπ)) = (π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) |
79 | 49, 78 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β
(+gβ(Scalarβπ)) = (π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) |
80 | 79 | oveqd 7378 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (π(+gβ(Scalarβπ))π) = (π(π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ))))π)) |
81 | 3, 5, 19, 54, 20, 77 | tendo0pl 39304 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ π β ((TEndoβπΎ)βπ)) β (π(π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ))))π) = π) |
82 | 49, 56, 81 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (π(π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ))))π) = π) |
83 | 80, 82 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (π(+gβ(Scalarβπ))π) = π) |
84 | 83 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (π = (π(+gβ(Scalarβπ))π) β π = π)) |
85 | 76, 84 | anbi12d 632 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β ((πΉ = (π₯ β π§) β§ π = (π(+gβ(Scalarβπ))π)) β (πΉ = (π₯(+gβπ)π§) β§ π = π))) |
86 | 70, 85 | bitrid 283 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (β¨πΉ, πβ© = β¨(π₯ β π§), (π(+gβ(Scalarβπ))π)β© β (πΉ = (π₯(+gβπ)π§) β§ π = π))) |
87 | 65, 86 | bitrd 279 |
. . . . . . . 8
β’ ((π β§ (π₯ β (π½βπ) β§ π§ β (π½βπ))) β (β¨πΉ, πβ© = (β¨π₯, πβ©(+gβπ)β¨π§, πβ©) β (πΉ = (π₯(+gβπ)π§) β§ π = π))) |
88 | 87 | pm5.32da 580 |
. . . . . . 7
β’ (π β (((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, πβ©(+gβπ)β¨π§, πβ©)) β ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (πΉ = (π₯(+gβπ)π§) β§ π = π)))) |
89 | 48, 88 | bitrid 283 |
. . . . . 6
β’ (π β (βπ¦βπ€(π¦ = π β§ π€ = π β§ ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©))) β ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (πΉ = (π₯(+gβπ)π§) β§ π = π)))) |
90 | 36, 89 | bitrd 279 |
. . . . 5
β’ (π β (βπ¦βπ€((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)) β ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (πΉ = (π₯(+gβπ)π§) β§ π = π)))) |
91 | 90 | exbidv 1925 |
. . . 4
β’ (π β (βπ§βπ¦βπ€((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)) β βπ§((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (πΉ = (π₯(+gβπ)π§) β§ π = π)))) |
92 | 18, 91 | bitrid 283 |
. . 3
β’ (π β (βπ¦βπ§βπ€((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)) β βπ§((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (πΉ = (π₯(+gβπ)π§) β§ π = π)))) |
93 | 92 | exbidv 1925 |
. 2
β’ (π β (βπ₯βπ¦βπ§βπ€((β¨π₯, π¦β© β (πΌβπ) β§ β¨π§, π€β© β (πΌβπ)) β§ β¨πΉ, πβ© = (β¨π₯, π¦β©(+gβπ)β¨π§, π€β©)) β βπ₯βπ§((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (πΉ = (π₯(+gβπ)π§) β§ π = π)))) |
94 | | anass 470 |
. . . . . 6
β’ ((((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ πΉ = (π₯(+gβπ)π§)) β§ π = π) β ((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (πΉ = (π₯(+gβπ)π§) β§ π = π))) |
95 | 94 | bicomi 223 |
. . . . 5
β’ (((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (πΉ = (π₯(+gβπ)π§) β§ π = π)) β (((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ πΉ = (π₯(+gβπ)π§)) β§ π = π)) |
96 | 95 | 2exbii 1852 |
. . . 4
β’
(βπ₯βπ§((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (πΉ = (π₯(+gβπ)π§) β§ π = π)) β βπ₯βπ§(((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ πΉ = (π₯(+gβπ)π§)) β§ π = π)) |
97 | | 19.41vv 1955 |
. . . 4
β’
(βπ₯βπ§(((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ πΉ = (π₯(+gβπ)π§)) β§ π = π) β (βπ₯βπ§((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ πΉ = (π₯(+gβπ)π§)) β§ π = π)) |
98 | 96, 97 | bitri 275 |
. . 3
β’
(βπ₯βπ§((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (πΉ = (π₯(+gβπ)π§) β§ π = π)) β (βπ₯βπ§((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ πΉ = (π₯(+gβπ)π§)) β§ π = π)) |
99 | 5, 71 | dvalvec 39539 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β π β LVec) |
100 | | lveclmod 20611 |
. . . . . . . . 9
β’ (π β LVec β π β LMod) |
101 | | eqid 2733 |
. . . . . . . . . 10
β’
(LSubSpβπ) =
(LSubSpβπ) |
102 | 101 | lsssssubg 20463 |
. . . . . . . . 9
β’ (π β LMod β
(LSubSpβπ) β
(SubGrpβπ)) |
103 | 1, 99, 100, 102 | 4syl 19 |
. . . . . . . 8
β’ (π β (LSubSpβπ) β (SubGrpβπ)) |
104 | 3, 4, 5, 71, 21, 101 | dialss 39559 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (π½βπ) β (LSubSpβπ)) |
105 | 1, 2, 104 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π½βπ) β (LSubSpβπ)) |
106 | 103, 105 | sseldd 3949 |
. . . . . . 7
β’ (π β (π½βπ) β (SubGrpβπ)) |
107 | 3, 4, 5, 71, 21, 101 | dialss 39559 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (π½βπ) β (LSubSpβπ)) |
108 | 1, 11, 107 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π½βπ) β (LSubSpβπ)) |
109 | 103, 108 | sseldd 3949 |
. . . . . . 7
β’ (π β (π½βπ) β (SubGrpβπ)) |
110 | | diblsmopel.q |
. . . . . . . 8
β’ β =
(LSSumβπ) |
111 | 72, 110 | lsmelval 19439 |
. . . . . . 7
β’ (((π½βπ) β (SubGrpβπ) β§ (π½βπ) β (SubGrpβπ)) β (πΉ β ((π½βπ) β (π½βπ)) β βπ₯ β (π½βπ)βπ§ β (π½βπ)πΉ = (π₯(+gβπ)π§))) |
112 | 106, 109,
111 | syl2anc 585 |
. . . . . 6
β’ (π β (πΉ β ((π½βπ) β (π½βπ)) β βπ₯ β (π½βπ)βπ§ β (π½βπ)πΉ = (π₯(+gβπ)π§))) |
113 | | r2ex 3189 |
. . . . . 6
β’
(βπ₯ β
(π½βπ)βπ§ β (π½βπ)πΉ = (π₯(+gβπ)π§) β βπ₯βπ§((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ πΉ = (π₯(+gβπ)π§))) |
114 | 112, 113 | bitrdi 287 |
. . . . 5
β’ (π β (πΉ β ((π½βπ) β (π½βπ)) β βπ₯βπ§((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ πΉ = (π₯(+gβπ)π§)))) |
115 | 114 | anbi1d 631 |
. . . 4
β’ (π β ((πΉ β ((π½βπ) β (π½βπ)) β§ π = π) β (βπ₯βπ§((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ πΉ = (π₯(+gβπ)π§)) β§ π = π))) |
116 | 115 | bicomd 222 |
. . 3
β’ (π β ((βπ₯βπ§((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ πΉ = (π₯(+gβπ)π§)) β§ π = π) β (πΉ β ((π½βπ) β (π½βπ)) β§ π = π))) |
117 | 98, 116 | bitrid 283 |
. 2
β’ (π β (βπ₯βπ§((π₯ β (π½βπ) β§ π§ β (π½βπ)) β§ (πΉ = (π₯(+gβπ)π§) β§ π = π)) β (πΉ β ((π½βπ) β (π½βπ)) β§ π = π))) |
118 | 17, 93, 117 | 3bitrd 305 |
1
β’ (π β (β¨πΉ, πβ© β ((πΌβπ) β (πΌβπ)) β (πΉ β ((π½βπ) β (π½βπ)) β§ π = π))) |