Step | Hyp | Ref
| Expression |
1 | | asclpropd.5 |
. . . . . 6
β’ (π β (1rβπΎ) β π) |
2 | | asclpropd.3 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯( Β·π
βπΎ)π¦) = (π₯( Β·π
βπΏ)π¦)) |
3 | 2 | oveqrspc2v 7385 |
. . . . . . 7
β’ ((π β§ (π§ β π β§ (1rβπΎ) β π)) β (π§( Β·π
βπΎ)(1rβπΎ)) = (π§( Β·π
βπΏ)(1rβπΎ))) |
4 | 3 | anassrs 469 |
. . . . . 6
β’ (((π β§ π§ β π) β§ (1rβπΎ) β π) β (π§( Β·π
βπΎ)(1rβπΎ)) = (π§( Β·π
βπΏ)(1rβπΎ))) |
5 | 1, 4 | mpidan 688 |
. . . . 5
β’ ((π β§ π§ β π) β (π§( Β·π
βπΎ)(1rβπΎ)) = (π§( Β·π
βπΏ)(1rβπΎ))) |
6 | | asclpropd.4 |
. . . . . . 7
β’ (π β (1rβπΎ) = (1rβπΏ)) |
7 | 6 | oveq2d 7374 |
. . . . . 6
β’ (π β (π§( Β·π
βπΏ)(1rβπΎ)) = (π§( Β·π
βπΏ)(1rβπΏ))) |
8 | 7 | adantr 482 |
. . . . 5
β’ ((π β§ π§ β π) β (π§( Β·π
βπΏ)(1rβπΎ)) = (π§( Β·π
βπΏ)(1rβπΏ))) |
9 | 5, 8 | eqtrd 2773 |
. . . 4
β’ ((π β§ π§ β π) β (π§( Β·π
βπΎ)(1rβπΎ)) = (π§( Β·π
βπΏ)(1rβπΏ))) |
10 | 9 | mpteq2dva 5206 |
. . 3
β’ (π β (π§ β π β¦ (π§( Β·π
βπΎ)(1rβπΎ))) = (π§ β π β¦ (π§( Β·π
βπΏ)(1rβπΏ)))) |
11 | | asclpropd.1 |
. . . 4
β’ (π β π = (BaseβπΉ)) |
12 | 11 | mpteq1d 5201 |
. . 3
β’ (π β (π§ β π β¦ (π§( Β·π
βπΎ)(1rβπΎ))) = (π§ β (BaseβπΉ) β¦ (π§( Β·π
βπΎ)(1rβπΎ)))) |
13 | | asclpropd.2 |
. . . 4
β’ (π β π = (BaseβπΊ)) |
14 | 13 | mpteq1d 5201 |
. . 3
β’ (π β (π§ β π β¦ (π§( Β·π
βπΏ)(1rβπΏ))) = (π§ β (BaseβπΊ) β¦ (π§( Β·π
βπΏ)(1rβπΏ)))) |
15 | 10, 12, 14 | 3eqtr3d 2781 |
. 2
β’ (π β (π§ β (BaseβπΉ) β¦ (π§( Β·π
βπΎ)(1rβπΎ))) = (π§ β (BaseβπΊ) β¦ (π§( Β·π
βπΏ)(1rβπΏ)))) |
16 | | eqid 2733 |
. . 3
β’
(algScβπΎ) =
(algScβπΎ) |
17 | | asclpropd.f |
. . 3
β’ πΉ = (ScalarβπΎ) |
18 | | eqid 2733 |
. . 3
β’
(BaseβπΉ) =
(BaseβπΉ) |
19 | | eqid 2733 |
. . 3
β’ (
Β·π βπΎ) = ( Β·π
βπΎ) |
20 | | eqid 2733 |
. . 3
β’
(1rβπΎ) = (1rβπΎ) |
21 | 16, 17, 18, 19, 20 | asclfval 21298 |
. 2
β’
(algScβπΎ) =
(π§ β (BaseβπΉ) β¦ (π§( Β·π
βπΎ)(1rβπΎ))) |
22 | | eqid 2733 |
. . 3
β’
(algScβπΏ) =
(algScβπΏ) |
23 | | asclpropd.g |
. . 3
β’ πΊ = (ScalarβπΏ) |
24 | | eqid 2733 |
. . 3
β’
(BaseβπΊ) =
(BaseβπΊ) |
25 | | eqid 2733 |
. . 3
β’ (
Β·π βπΏ) = ( Β·π
βπΏ) |
26 | | eqid 2733 |
. . 3
β’
(1rβπΏ) = (1rβπΏ) |
27 | 22, 23, 24, 25, 26 | asclfval 21298 |
. 2
β’
(algScβπΏ) =
(π§ β (BaseβπΊ) β¦ (π§( Β·π
βπΏ)(1rβπΏ))) |
28 | 15, 21, 27 | 3eqtr4g 2798 |
1
β’ (π β (algScβπΎ) = (algScβπΏ)) |