Step | Hyp | Ref
| Expression |
1 | | hlhilphl.h |
. . 3
β’ π» = (LHypβπΎ) |
2 | | hlhilphllem.u |
. . 3
β’ π = ((HLHilβπΎ)βπ) |
3 | | hlhilphl.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
4 | | hlhilphllem.l |
. . 3
β’ πΏ = ((DVecHβπΎ)βπ) |
5 | | hlhilphllem.v |
. . 3
β’ π = (BaseβπΏ) |
6 | 1, 2, 3, 4, 5 | hlhilbase 40899 |
. 2
β’ (π β π = (Baseβπ)) |
7 | | hlhilphllem.a |
. . 3
β’ + =
(+gβπΏ) |
8 | 1, 2, 3, 4, 7 | hlhilplus 40900 |
. 2
β’ (π β + =
(+gβπ)) |
9 | | hlhilphllem.s |
. . 3
β’ Β· = (
Β·π βπΏ) |
10 | 1, 4, 9, 2, 3 | hlhilvsca 40914 |
. 2
β’ (π β Β· = (
Β·π βπ)) |
11 | | hlhilphllem.i |
. . 3
β’ , =
(Β·πβπ) |
12 | 11 | a1i 11 |
. 2
β’ (π β , =
(Β·πβπ)) |
13 | | hlhilphllem.z |
. . 3
β’ 0 =
(0gβπΏ) |
14 | 1, 4, 2, 3, 13 | hlhil0 40922 |
. 2
β’ (π β 0 =
(0gβπ)) |
15 | | hlhilphllem.f |
. . 3
β’ πΉ = (Scalarβπ) |
16 | 15 | a1i 11 |
. 2
β’ (π β πΉ = (Scalarβπ)) |
17 | | hlhilphllem.r |
. . 3
β’ π
= (ScalarβπΏ) |
18 | | hlhilphllem.b |
. . 3
β’ π΅ = (Baseβπ
) |
19 | 1, 4, 17, 2, 15, 3, 18 | hlhilsbase2 40909 |
. 2
β’ (π β π΅ = (BaseβπΉ)) |
20 | | hlhilphllem.p |
. . 3
⒠⨣ =
(+gβπ
) |
21 | 1, 4, 17, 2, 15, 3, 20 | hlhilsplus2 40910 |
. 2
β’ (π β ⨣ =
(+gβπΉ)) |
22 | | hlhilphllem.t |
. . 3
β’ Γ =
(.rβπ
) |
23 | 1, 4, 17, 2, 15, 3, 22 | hlhilsmul2 40911 |
. 2
β’ (π β Γ =
(.rβπΉ)) |
24 | | hlhilphllem.g |
. . 3
β’ πΊ = ((HGMapβπΎ)βπ) |
25 | 1, 2, 15, 24, 3 | hlhilnvl 40917 |
. 2
β’ (π β πΊ = (*πβπΉ)) |
26 | | hlhilphllem.q |
. . 3
β’ π = (0gβπ
) |
27 | 1, 4, 17, 2, 15, 3, 26 | hlhils0 40912 |
. 2
β’ (π β π = (0gβπΉ)) |
28 | 1, 2, 3 | hlhillvec 40918 |
. 2
β’ (π β π β LVec) |
29 | 1, 2, 3, 15 | hlhilsrng 40921 |
. 2
β’ (π β πΉ β *-Ring) |
30 | | hlhilphllem.j |
. . . 4
β’ π½ = ((HDMapβπΎ)βπ) |
31 | 3 | 3ad2ant1 1133 |
. . . 4
β’ ((π β§ π β π β§ π β π) β (πΎ β HL β§ π β π»)) |
32 | | simp2 1137 |
. . . 4
β’ ((π β§ π β π β§ π β π) β π β π) |
33 | | simp3 1138 |
. . . 4
β’ ((π β§ π β π β§ π β π) β π β π) |
34 | 1, 4, 5, 30, 2, 31, 11, 32, 33 | hlhilipval 40916 |
. . 3
β’ ((π β§ π β π β§ π β π) β (π , π) = ((π½βπ)βπ)) |
35 | 1, 4, 5, 17, 18, 30, 31, 32, 33 | hdmapipcl 40868 |
. . 3
β’ ((π β§ π β π β§ π β π) β ((π½βπ)βπ) β π΅) |
36 | 34, 35 | eqeltrd 2833 |
. 2
β’ ((π β§ π β π β§ π β π) β (π , π) β π΅) |
37 | 3 | 3ad2ant1 1133 |
. . . 4
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β (πΎ β HL β§ π β π»)) |
38 | | simp31 1209 |
. . . 4
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β π β π) |
39 | | simp32 1210 |
. . . 4
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β π β π) |
40 | | simp33 1211 |
. . . 4
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β π β π) |
41 | | simp2 1137 |
. . . 4
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β π β π΅) |
42 | 1, 4, 5, 7, 9, 17,
18, 20, 22, 30, 37, 38, 39, 40, 41 | hdmapln1 40869 |
. . 3
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β ((π½βπ)β((π Β· π) + π)) = ((π Γ ((π½βπ)βπ)) ⨣ ((π½βπ)βπ))) |
43 | 1, 4, 3 | dvhlmod 40073 |
. . . . . 6
β’ (π β πΏ β LMod) |
44 | 43 | 3ad2ant1 1133 |
. . . . 5
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β πΏ β LMod) |
45 | 5, 17, 9, 18 | lmodvscl 20493 |
. . . . . 6
β’ ((πΏ β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
46 | 44, 41, 38, 45 | syl3anc 1371 |
. . . . 5
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β (π Β· π) β π) |
47 | 5, 7 | lmodvacl 20490 |
. . . . 5
β’ ((πΏ β LMod β§ (π Β· π) β π β§ π β π) β ((π Β· π) + π) β π) |
48 | 44, 46, 39, 47 | syl3anc 1371 |
. . . 4
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β ((π Β· π) + π) β π) |
49 | 1, 4, 5, 30, 2, 37, 11, 48, 40 | hlhilipval 40916 |
. . 3
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β (((π Β· π) + π) , π) = ((π½βπ)β((π Β· π) + π))) |
50 | 1, 4, 5, 30, 2, 37, 11, 38, 40 | hlhilipval 40916 |
. . . . 5
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β (π , π) = ((π½βπ)βπ)) |
51 | 50 | oveq2d 7427 |
. . . 4
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β (π Γ (π , π)) = (π Γ ((π½βπ)βπ))) |
52 | 1, 4, 5, 30, 2, 37, 11, 39, 40 | hlhilipval 40916 |
. . . 4
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β (π , π) = ((π½βπ)βπ)) |
53 | 51, 52 | oveq12d 7429 |
. . 3
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β ((π Γ (π , π)) ⨣ (π , π)) = ((π Γ ((π½βπ)βπ)) ⨣ ((π½βπ)βπ))) |
54 | 42, 49, 53 | 3eqtr4d 2782 |
. 2
β’ ((π β§ π β π΅ β§ (π β π β§ π β π β§ π β π)) β (((π Β· π) + π) , π) = ((π Γ (π , π)) ⨣ (π , π))) |
55 | 3 | adantr 481 |
. . . . . 6
β’ ((π β§ π β π) β (πΎ β HL β§ π β π»)) |
56 | | simpr 485 |
. . . . . 6
β’ ((π β§ π β π) β π β π) |
57 | 1, 4, 5, 30, 2, 55, 11, 56, 56 | hlhilipval 40916 |
. . . . 5
β’ ((π β§ π β π) β (π , π) = ((π½βπ)βπ)) |
58 | 57 | eqeq1d 2734 |
. . . 4
β’ ((π β§ π β π) β ((π , π) = π β ((π½βπ)βπ) = π)) |
59 | 1, 4, 5, 13, 17, 26, 30, 55, 56 | hdmapip0 40878 |
. . . 4
β’ ((π β§ π β π) β (((π½βπ)βπ) = π β π = 0 )) |
60 | 58, 59 | bitrd 278 |
. . 3
β’ ((π β§ π β π) β ((π , π) = π β π = 0 )) |
61 | 60 | biimp3a 1469 |
. 2
β’ ((π β§ π β π β§ (π , π) = π) β π = 0 ) |
62 | 1, 4, 5, 30, 24, 31, 32, 33 | hdmapg 40893 |
. . 3
β’ ((π β§ π β π β§ π β π) β (πΊβ((π½βπ)βπ)) = ((π½βπ)βπ)) |
63 | 34 | fveq2d 6895 |
. . 3
β’ ((π β§ π β π β§ π β π) β (πΊβ(π , π)) = (πΊβ((π½βπ)βπ))) |
64 | 1, 4, 5, 30, 2, 31, 11, 33, 32 | hlhilipval 40916 |
. . 3
β’ ((π β§ π β π β§ π β π) β (π , π) = ((π½βπ)βπ)) |
65 | 62, 63, 64 | 3eqtr4d 2782 |
. 2
β’ ((π β§ π β π β§ π β π) β (πΊβ(π , π)) = (π , π)) |
66 | 6, 8, 10, 12, 14, 16, 19, 21, 23, 25, 27, 28, 29, 36, 54, 61, 65 | isphld 21213 |
1
β’ (π β π β PreHil) |