Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (πΎ β HL β§ π β π»)) |
2 | | dvh0g.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | dvh0g.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | | dvh0g.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
5 | 2, 3, 4 | idltrn 38616 |
. . . 4
β’ ((πΎ β HL β§ π β π») β ( I βΎ π΅) β π) |
6 | | eqid 2737 |
. . . . 5
β’
((TEndoβπΎ)βπ) = ((TEndoβπΎ)βπ) |
7 | | dvh0g.o |
. . . . 5
β’ π = (π β π β¦ ( I βΎ π΅)) |
8 | 2, 3, 4, 6, 7 | tendo0cl 39256 |
. . . 4
β’ ((πΎ β HL β§ π β π») β π β ((TEndoβπΎ)βπ)) |
9 | | dvh0g.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
10 | | eqid 2737 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
11 | | eqid 2737 |
. . . . 5
β’
(+gβπ) = (+gβπ) |
12 | | eqid 2737 |
. . . . 5
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
13 | 3, 4, 6, 9, 10, 11, 12 | dvhopvadd 39559 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (( I βΎ π΅) β π β§ π β ((TEndoβπΎ)βπ)) β§ (( I βΎ π΅) β π β§ π β ((TEndoβπΎ)βπ))) β (β¨( I βΎ π΅), πβ©(+gβπ)β¨( I βΎ π΅), πβ©) = β¨(( I βΎ π΅) β ( I βΎ π΅)), (π(+gβ(Scalarβπ))π)β©) |
14 | 1, 5, 8, 5, 8, 13 | syl122anc 1380 |
. . 3
β’ ((πΎ β HL β§ π β π») β (β¨( I βΎ π΅), πβ©(+gβπ)β¨( I βΎ π΅), πβ©) = β¨(( I βΎ π΅) β ( I βΎ π΅)), (π(+gβ(Scalarβπ))π)β©) |
15 | | f1oi 6823 |
. . . . . 6
β’ ( I
βΎ π΅):π΅β1-1-ontoβπ΅ |
16 | | f1of 6785 |
. . . . . 6
β’ (( I
βΎ π΅):π΅β1-1-ontoβπ΅ β ( I βΎ π΅):π΅βΆπ΅) |
17 | | fcoi2 6718 |
. . . . . 6
β’ (( I
βΎ π΅):π΅βΆπ΅ β (( I βΎ π΅) β ( I βΎ π΅)) = ( I βΎ π΅)) |
18 | 15, 16, 17 | mp2b 10 |
. . . . 5
β’ (( I
βΎ π΅) β ( I
βΎ π΅)) = ( I βΎ
π΅) |
19 | 18 | a1i 11 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (( I βΎ π΅) β ( I βΎ π΅)) = ( I βΎ π΅)) |
20 | | eqid 2737 |
. . . . . . 7
β’ (π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) = (π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) |
21 | 3, 4, 6, 9, 10, 20, 12 | dvhfplusr 39550 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β
(+gβ(Scalarβπ)) = (π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) |
22 | 21 | oveqd 7375 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (π(+gβ(Scalarβπ))π) = (π(π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ))))π)) |
23 | 2, 3, 4, 6, 7, 20 | tendo0pl 39257 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β ((TEndoβπΎ)βπ)) β (π(π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ))))π) = π) |
24 | 8, 23 | mpdan 686 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (π(π β ((TEndoβπΎ)βπ), π‘ β ((TEndoβπΎ)βπ) β¦ (π β π β¦ ((π βπ) β (π‘βπ))))π) = π) |
25 | 22, 24 | eqtrd 2777 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (π(+gβ(Scalarβπ))π) = π) |
26 | 19, 25 | opeq12d 4839 |
. . 3
β’ ((πΎ β HL β§ π β π») β β¨(( I βΎ π΅) β ( I βΎ π΅)), (π(+gβ(Scalarβπ))π)β© = β¨( I βΎ π΅), πβ©) |
27 | 14, 26 | eqtrd 2777 |
. 2
β’ ((πΎ β HL β§ π β π») β (β¨( I βΎ π΅), πβ©(+gβπ)β¨( I βΎ π΅), πβ©) = β¨( I βΎ π΅), πβ©) |
28 | 3, 9, 1 | dvhlmod 39576 |
. . 3
β’ ((πΎ β HL β§ π β π») β π β LMod) |
29 | | eqid 2737 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
30 | 3, 4, 6, 9, 29 | dvhelvbasei 39554 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (( I βΎ π΅) β π β§ π β ((TEndoβπΎ)βπ))) β β¨( I βΎ π΅), πβ© β (Baseβπ)) |
31 | 1, 5, 8, 30 | syl12anc 836 |
. . 3
β’ ((πΎ β HL β§ π β π») β β¨( I βΎ π΅), πβ© β (Baseβπ)) |
32 | | dvh0g.z |
. . . 4
β’ 0 =
(0gβπ) |
33 | 29, 11, 32 | lmod0vid 20357 |
. . 3
β’ ((π β LMod β§ β¨( I
βΎ π΅), πβ© β (Baseβπ)) β ((β¨( I βΎ
π΅), πβ©(+gβπ)β¨( I βΎ π΅), πβ©) = β¨( I βΎ π΅), πβ© β 0 = β¨( I βΎ π΅), πβ©)) |
34 | 28, 31, 33 | syl2anc 585 |
. 2
β’ ((πΎ β HL β§ π β π») β ((β¨( I βΎ π΅), πβ©(+gβπ)β¨( I βΎ π΅), πβ©) = β¨( I βΎ π΅), πβ© β 0 = β¨( I βΎ π΅), πβ©)) |
35 | 27, 34 | mpbid 231 |
1
β’ ((πΎ β HL β§ π β π») β 0 = β¨( I βΎ π΅), πβ©) |