Step | Hyp | Ref
| Expression |
1 | | eqidd 2734 |
. 2
β’ ((π β PreHil β§ π β π) β (Baseβπ) = (Baseβπ)) |
2 | | eqidd 2734 |
. 2
β’ ((π β PreHil β§ π β π) β (+gβπ) = (+gβπ)) |
3 | | eqidd 2734 |
. 2
β’ ((π β PreHil β§ π β π) β (
Β·π βπ) = ( Β·π
βπ)) |
4 | | eqidd 2734 |
. 2
β’ ((π β PreHil β§ π β π) β
(Β·πβπ) =
(Β·πβπ)) |
5 | | phllmod 21057 |
. . . 4
β’ (π β PreHil β π β LMod) |
6 | | phlssphl.x |
. . . . 5
β’ π = (π βΎs π) |
7 | | eqid 2733 |
. . . . 5
β’
(0gβπ) = (0gβπ) |
8 | | eqid 2733 |
. . . . 5
β’
(0gβπ) = (0gβπ) |
9 | | phlssphl.s |
. . . . 5
β’ π = (LSubSpβπ) |
10 | 6, 7, 8, 9 | lss0v 20521 |
. . . 4
β’ ((π β LMod β§ π β π) β (0gβπ) = (0gβπ)) |
11 | 5, 10 | sylan 581 |
. . 3
β’ ((π β PreHil β§ π β π) β (0gβπ) = (0gβπ)) |
12 | 11 | eqcomd 2739 |
. 2
β’ ((π β PreHil β§ π β π) β (0gβπ) = (0gβπ)) |
13 | | eqidd 2734 |
. 2
β’ ((π β PreHil β§ π β π) β (Scalarβπ) = (Scalarβπ)) |
14 | | eqidd 2734 |
. 2
β’ ((π β PreHil β§ π β π) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
15 | | eqidd 2734 |
. 2
β’ ((π β PreHil β§ π β π) β
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ))) |
16 | | eqidd 2734 |
. 2
β’ ((π β PreHil β§ π β π) β
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ))) |
17 | | eqidd 2734 |
. 2
β’ ((π β PreHil β§ π β π) β
(*πβ(Scalarβπ)) =
(*πβ(Scalarβπ))) |
18 | | eqidd 2734 |
. 2
β’ ((π β PreHil β§ π β π) β
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ))) |
19 | | phllvec 21056 |
. . 3
β’ (π β PreHil β π β LVec) |
20 | 6, 9 | lsslvec 20613 |
. . 3
β’ ((π β LVec β§ π β π) β π β LVec) |
21 | 19, 20 | sylan 581 |
. 2
β’ ((π β PreHil β§ π β π) β π β LVec) |
22 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
23 | 6, 22 | resssca 17232 |
. . . . 5
β’ (π β π β (Scalarβπ) = (Scalarβπ)) |
24 | 23 | eqcomd 2739 |
. . . 4
β’ (π β π β (Scalarβπ) = (Scalarβπ)) |
25 | 24 | adantl 483 |
. . 3
β’ ((π β PreHil β§ π β π) β (Scalarβπ) = (Scalarβπ)) |
26 | 22 | phlsrng 21058 |
. . . 4
β’ (π β PreHil β
(Scalarβπ) β
*-Ring) |
27 | 26 | adantr 482 |
. . 3
β’ ((π β PreHil β§ π β π) β (Scalarβπ) β *-Ring) |
28 | 25, 27 | eqeltrd 2834 |
. 2
β’ ((π β PreHil β§ π β π) β (Scalarβπ) β *-Ring) |
29 | | simpl 484 |
. . . . 5
β’ ((π β PreHil β§ π β π) β π β PreHil) |
30 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
31 | 6, 30 | ressbasss 17129 |
. . . . . 6
β’
(Baseβπ)
β (Baseβπ) |
32 | 31 | sseli 3944 |
. . . . 5
β’ (π₯ β (Baseβπ) β π₯ β (Baseβπ)) |
33 | 31 | sseli 3944 |
. . . . 5
β’ (π¦ β (Baseβπ) β π¦ β (Baseβπ)) |
34 | | eqid 2733 |
. . . . . 6
β’
(Β·πβπ) =
(Β·πβπ) |
35 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
36 | 22, 34, 30, 35 | ipcl 21060 |
. . . . 5
β’ ((π β PreHil β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ))) |
37 | 29, 32, 33, 36 | syl3an 1161 |
. . . 4
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ))) |
38 | 24 | fveq2d 6850 |
. . . . . . 7
β’ (π β π β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
39 | 38 | eleq2d 2820 |
. . . . . 6
β’ (π β π β ((π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ)) β (π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ)))) |
40 | 39 | adantl 483 |
. . . . 5
β’ ((π β PreHil β§ π β π) β ((π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ)) β (π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ)))) |
41 | 40 | 3ad2ant1 1134 |
. . . 4
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β ((π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ)) β (π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ)))) |
42 | 37, 41 | mpbird 257 |
. . 3
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ))) |
43 | | eqid 2733 |
. . . . . . . 8
β’
(Β·πβπ) =
(Β·πβπ) |
44 | 6, 34, 43 | ssipeq 21083 |
. . . . . . 7
β’ (π β π β
(Β·πβπ) =
(Β·πβπ)) |
45 | 44 | oveqd 7378 |
. . . . . 6
β’ (π β π β (π₯(Β·πβπ)π¦) = (π₯(Β·πβπ)π¦)) |
46 | 45 | eleq1d 2819 |
. . . . 5
β’ (π β π β ((π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ)) β (π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ)))) |
47 | 46 | adantl 483 |
. . . 4
β’ ((π β PreHil β§ π β π) β ((π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ)) β (π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ)))) |
48 | 47 | 3ad2ant1 1134 |
. . 3
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β ((π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ)) β (π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ)))) |
49 | 42, 48 | mpbird 257 |
. 2
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(Β·πβπ)π¦) β (Baseβ(Scalarβπ))) |
50 | 29 | 3ad2ant1 1134 |
. . . . 5
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π β PreHil) |
51 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β PreHil β§ π β π) β π β LMod) |
52 | 51 | 3ad2ant1 1134 |
. . . . . 6
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π β LMod) |
53 | 25 | fveq2d 6850 |
. . . . . . . . 9
β’ ((π β PreHil β§ π β π) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβπ))) |
54 | 53 | eleq2d 2820 |
. . . . . . . 8
β’ ((π β PreHil β§ π β π) β (π β (Baseβ(Scalarβπ)) β π β (Baseβ(Scalarβπ)))) |
55 | 54 | biimpa 478 |
. . . . . . 7
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ))) β π β (Baseβ(Scalarβπ))) |
56 | 55 | 3adant3 1133 |
. . . . . 6
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π β (Baseβ(Scalarβπ))) |
57 | 32 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ)) β π₯ β (Baseβπ)) |
58 | 57 | 3ad2ant3 1136 |
. . . . . 6
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π₯ β (Baseβπ)) |
59 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
60 | 30, 22, 59, 35 | lmodvscl 20383 |
. . . . . 6
β’ ((π β LMod β§ π β
(Baseβ(Scalarβπ)) β§ π₯ β (Baseβπ)) β (π( Β·π
βπ)π₯) β (Baseβπ)) |
61 | 52, 56, 58, 60 | syl3anc 1372 |
. . . . 5
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π( Β·π
βπ)π₯) β (Baseβπ)) |
62 | 33 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ)) β π¦ β (Baseβπ)) |
63 | 62 | 3ad2ant3 1136 |
. . . . 5
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π¦ β (Baseβπ)) |
64 | 31 | sseli 3944 |
. . . . . . 7
β’ (π§ β (Baseβπ) β π§ β (Baseβπ)) |
65 | 64 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ)) β π§ β (Baseβπ)) |
66 | 65 | 3ad2ant3 1136 |
. . . . 5
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π§ β (Baseβπ)) |
67 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
68 | | eqid 2733 |
. . . . . 6
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
69 | 22, 34, 30, 67, 68 | ipdir 21066 |
. . . . 5
β’ ((π β PreHil β§ ((π(
Β·π βπ)π₯) β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (((π( Β·π
βπ)π₯)(+gβπ)π¦)(Β·πβπ)π§) = (((π( Β·π
βπ)π₯)(Β·πβπ)π§)(+gβ(Scalarβπ))(π¦(Β·πβπ)π§))) |
70 | 50, 61, 63, 66, 69 | syl13anc 1373 |
. . . 4
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (((π( Β·π
βπ)π₯)(+gβπ)π¦)(Β·πβπ)π§) = (((π( Β·π
βπ)π₯)(Β·πβπ)π§)(+gβ(Scalarβπ))(π¦(Β·πβπ)π§))) |
71 | | eqid 2733 |
. . . . . . 7
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
72 | 22, 34, 30, 35, 59, 71 | ipass 21072 |
. . . . . 6
β’ ((π β PreHil β§ (π β
(Baseβ(Scalarβπ)) β§ π₯ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π( Β·π
βπ)π₯)(Β·πβπ)π§) = (π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))) |
73 | 50, 56, 58, 66, 72 | syl13anc 1373 |
. . . . 5
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((π( Β·π
βπ)π₯)(Β·πβπ)π§) = (π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))) |
74 | 73 | oveq1d 7376 |
. . . 4
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (((π( Β·π
βπ)π₯)(Β·πβπ)π§)(+gβ(Scalarβπ))(π¦(Β·πβπ)π§)) = ((π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))(+gβ(Scalarβπ))(π¦(Β·πβπ)π§))) |
75 | 70, 74 | eqtrd 2773 |
. . 3
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (((π( Β·π
βπ)π₯)(+gβπ)π¦)(Β·πβπ)π§) = ((π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))(+gβ(Scalarβπ))(π¦(Β·πβπ)π§))) |
76 | 6, 67 | ressplusg 17179 |
. . . . . . . . 9
β’ (π β π β (+gβπ) = (+gβπ)) |
77 | 76 | eqcomd 2739 |
. . . . . . . 8
β’ (π β π β (+gβπ) = (+gβπ)) |
78 | 6, 59 | ressvsca 17233 |
. . . . . . . . . 10
β’ (π β π β (
Β·π βπ) = ( Β·π
βπ)) |
79 | 78 | eqcomd 2739 |
. . . . . . . . 9
β’ (π β π β (
Β·π βπ) = ( Β·π
βπ)) |
80 | 79 | oveqd 7378 |
. . . . . . . 8
β’ (π β π β (π( Β·π
βπ)π₯) = (π( Β·π
βπ)π₯)) |
81 | | eqidd 2734 |
. . . . . . . 8
β’ (π β π β π¦ = π¦) |
82 | 77, 80, 81 | oveq123d 7382 |
. . . . . . 7
β’ (π β π β ((π( Β·π
βπ)π₯)(+gβπ)π¦) = ((π( Β·π
βπ)π₯)(+gβπ)π¦)) |
83 | | eqidd 2734 |
. . . . . . 7
β’ (π β π β π§ = π§) |
84 | 44, 82, 83 | oveq123d 7382 |
. . . . . 6
β’ (π β π β (((π( Β·π
βπ)π₯)(+gβπ)π¦)(Β·πβπ)π§) = (((π( Β·π
βπ)π₯)(+gβπ)π¦)(Β·πβπ)π§)) |
85 | 24 | fveq2d 6850 |
. . . . . . 7
β’ (π β π β
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ))) |
86 | 24 | fveq2d 6850 |
. . . . . . . 8
β’ (π β π β
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ))) |
87 | | eqidd 2734 |
. . . . . . . 8
β’ (π β π β π = π) |
88 | 44 | oveqd 7378 |
. . . . . . . 8
β’ (π β π β (π₯(Β·πβπ)π§) = (π₯(Β·πβπ)π§)) |
89 | 86, 87, 88 | oveq123d 7382 |
. . . . . . 7
β’ (π β π β (π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§)) = (π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))) |
90 | 44 | oveqd 7378 |
. . . . . . 7
β’ (π β π β (π¦(Β·πβπ)π§) = (π¦(Β·πβπ)π§)) |
91 | 85, 89, 90 | oveq123d 7382 |
. . . . . 6
β’ (π β π β ((π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))(+gβ(Scalarβπ))(π¦(Β·πβπ)π§)) = ((π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))(+gβ(Scalarβπ))(π¦(Β·πβπ)π§))) |
92 | 84, 91 | eqeq12d 2749 |
. . . . 5
β’ (π β π β ((((π( Β·π
βπ)π₯)(+gβπ)π¦)(Β·πβπ)π§) = ((π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))(+gβ(Scalarβπ))(π¦(Β·πβπ)π§)) β (((π( Β·π
βπ)π₯)(+gβπ)π¦)(Β·πβπ)π§) = ((π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))(+gβ(Scalarβπ))(π¦(Β·πβπ)π§)))) |
93 | 92 | adantl 483 |
. . . 4
β’ ((π β PreHil β§ π β π) β ((((π( Β·π
βπ)π₯)(+gβπ)π¦)(Β·πβπ)π§) = ((π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))(+gβ(Scalarβπ))(π¦(Β·πβπ)π§)) β (((π( Β·π
βπ)π₯)(+gβπ)π¦)(Β·πβπ)π§) = ((π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))(+gβ(Scalarβπ))(π¦(Β·πβπ)π§)))) |
94 | 93 | 3ad2ant1 1134 |
. . 3
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((((π( Β·π
βπ)π₯)(+gβπ)π¦)(Β·πβπ)π§) = ((π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))(+gβ(Scalarβπ))(π¦(Β·πβπ)π§)) β (((π( Β·π
βπ)π₯)(+gβπ)π¦)(Β·πβπ)π§) = ((π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))(+gβ(Scalarβπ))(π¦(Β·πβπ)π§)))) |
95 | 75, 94 | mpbird 257 |
. 2
β’ (((π β PreHil β§ π β π) β§ π β (Baseβ(Scalarβπ)) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (((π( Β·π
βπ)π₯)(+gβπ)π¦)(Β·πβπ)π§) = ((π(.rβ(Scalarβπ))(π₯(Β·πβπ)π§))(+gβ(Scalarβπ))(π¦(Β·πβπ)π§))) |
96 | 44 | adantl 483 |
. . . . . 6
β’ ((π β PreHil β§ π β π) β
(Β·πβπ) =
(Β·πβπ)) |
97 | 96 | oveqdr 7389 |
. . . . 5
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ)) β (π₯(Β·πβπ)π₯) = (π₯(Β·πβπ)π₯)) |
98 | 24 | fveq2d 6850 |
. . . . . . 7
β’ (π β π β
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ))) |
99 | 98 | adantl 483 |
. . . . . 6
β’ ((π β PreHil β§ π β π) β
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ))) |
100 | 99 | adantr 482 |
. . . . 5
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ)) β
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ))) |
101 | 97, 100 | eqeq12d 2749 |
. . . 4
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ)) β ((π₯(Β·πβπ)π₯) = (0gβ(Scalarβπ)) β (π₯(Β·πβπ)π₯) = (0gβ(Scalarβπ)))) |
102 | | eqid 2733 |
. . . . . . 7
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
103 | 22, 34, 30, 102, 7 | ipeq0 21065 |
. . . . . 6
β’ ((π β PreHil β§ π₯ β (Baseβπ)) β ((π₯(Β·πβπ)π₯) = (0gβ(Scalarβπ)) β π₯ = (0gβπ))) |
104 | 29, 32, 103 | syl2an 597 |
. . . . 5
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ)) β ((π₯(Β·πβπ)π₯) = (0gβ(Scalarβπ)) β π₯ = (0gβπ))) |
105 | 104 | biimpd 228 |
. . . 4
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ)) β ((π₯(Β·πβπ)π₯) = (0gβ(Scalarβπ)) β π₯ = (0gβπ))) |
106 | 101, 105 | sylbid 239 |
. . 3
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ)) β ((π₯(Β·πβπ)π₯) = (0gβ(Scalarβπ)) β π₯ = (0gβπ))) |
107 | 106 | 3impia 1118 |
. 2
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ) β§ (π₯(Β·πβπ)π₯) = (0gβ(Scalarβπ))) β π₯ = (0gβπ)) |
108 | 24 | fveq2d 6850 |
. . . . . . 7
β’ (π β π β
(*πβ(Scalarβπ)) =
(*πβ(Scalarβπ))) |
109 | 108 | fveq1d 6848 |
. . . . . 6
β’ (π β π β
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) =
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦))) |
110 | 109 | adantl 483 |
. . . . 5
β’ ((π β PreHil β§ π β π) β
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) =
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦))) |
111 | 110 | 3ad2ant1 1134 |
. . . 4
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) =
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦))) |
112 | | eqid 2733 |
. . . . . 6
β’
(*πβ(Scalarβπ)) =
(*πβ(Scalarβπ)) |
113 | 22, 34, 30, 112 | ipcj 21061 |
. . . . 5
β’ ((π β PreHil β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) = (π¦(Β·πβπ)π₯)) |
114 | 29, 32, 33, 113 | syl3an 1161 |
. . . 4
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) = (π¦(Β·πβπ)π₯)) |
115 | 111, 114 | eqtrd 2773 |
. . 3
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) = (π¦(Β·πβπ)π₯)) |
116 | 45 | fveq2d 6850 |
. . . . . 6
β’ (π β π β
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) =
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦))) |
117 | 44 | oveqd 7378 |
. . . . . 6
β’ (π β π β (π¦(Β·πβπ)π₯) = (π¦(Β·πβπ)π₯)) |
118 | 116, 117 | eqeq12d 2749 |
. . . . 5
β’ (π β π β
(((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) = (π¦(Β·πβπ)π₯) β
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) = (π¦(Β·πβπ)π₯))) |
119 | 118 | adantl 483 |
. . . 4
β’ ((π β PreHil β§ π β π) β
(((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) = (π¦(Β·πβπ)π₯) β
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) = (π¦(Β·πβπ)π₯))) |
120 | 119 | 3ad2ant1 1134 |
. . 3
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β
(((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) = (π¦(Β·πβπ)π₯) β
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) = (π¦(Β·πβπ)π₯))) |
121 | 115, 120 | mpbird 257 |
. 2
β’ (((π β PreHil β§ π β π) β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β
((*πβ(Scalarβπ))β(π₯(Β·πβπ)π¦)) = (π¦(Β·πβπ)π₯)) |
122 | 1, 2, 3, 4, 12, 13, 14, 15, 16, 17, 18, 21, 28, 49, 95, 107, 121 | isphld 21081 |
1
β’ ((π β PreHil β§ π β π) β π β PreHil) |