Step | Hyp | Ref
| Expression |
1 | | lflset.v |
. . . . 5
β’ π = (Baseβπ) |
2 | | lflset.a |
. . . . 5
β’ + =
(+gβπ) |
3 | | lflset.d |
. . . . 5
β’ π· = (Scalarβπ) |
4 | | lflset.s |
. . . . 5
β’ Β· = (
Β·π βπ) |
5 | | lflset.k |
. . . . 5
β’ πΎ = (Baseβπ·) |
6 | | lflset.p |
. . . . 5
⒠⨣ =
(+gβπ·) |
7 | | lflset.t |
. . . . 5
β’ Γ =
(.rβπ·) |
8 | | lflset.f |
. . . . 5
β’ πΉ = (LFnlβπ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | islfl 37551 |
. . . 4
β’ (π β π β (πΊ β πΉ β (πΊ:πβΆπΎ β§ βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦))))) |
10 | 9 | simplbda 501 |
. . 3
β’ ((π β π β§ πΊ β πΉ) β βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦))) |
11 | 10 | 3adant3 1133 |
. 2
β’ ((π β π β§ πΊ β πΉ β§ (π
β πΎ β§ π β π β§ π β π)) β βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦))) |
12 | | oveq1 7369 |
. . . . . 6
β’ (π = π
β (π Β· π₯) = (π
Β· π₯)) |
13 | 12 | fvoveq1d 7384 |
. . . . 5
β’ (π = π
β (πΊβ((π Β· π₯) + π¦)) = (πΊβ((π
Β· π₯) + π¦))) |
14 | | oveq1 7369 |
. . . . . 6
β’ (π = π
β (π Γ (πΊβπ₯)) = (π
Γ (πΊβπ₯))) |
15 | 14 | oveq1d 7377 |
. . . . 5
β’ (π = π
β ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)) = ((π
Γ (πΊβπ₯)) ⨣ (πΊβπ¦))) |
16 | 13, 15 | eqeq12d 2753 |
. . . 4
β’ (π = π
β ((πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)) β (πΊβ((π
Β· π₯) + π¦)) = ((π
Γ (πΊβπ₯)) ⨣ (πΊβπ¦)))) |
17 | | oveq2 7370 |
. . . . . 6
β’ (π₯ = π β (π
Β· π₯) = (π
Β· π)) |
18 | 17 | fvoveq1d 7384 |
. . . . 5
β’ (π₯ = π β (πΊβ((π
Β· π₯) + π¦)) = (πΊβ((π
Β· π) + π¦))) |
19 | | fveq2 6847 |
. . . . . . 7
β’ (π₯ = π β (πΊβπ₯) = (πΊβπ)) |
20 | 19 | oveq2d 7378 |
. . . . . 6
β’ (π₯ = π β (π
Γ (πΊβπ₯)) = (π
Γ (πΊβπ))) |
21 | 20 | oveq1d 7377 |
. . . . 5
β’ (π₯ = π β ((π
Γ (πΊβπ₯)) ⨣ (πΊβπ¦)) = ((π
Γ (πΊβπ)) ⨣ (πΊβπ¦))) |
22 | 18, 21 | eqeq12d 2753 |
. . . 4
β’ (π₯ = π β ((πΊβ((π
Β· π₯) + π¦)) = ((π
Γ (πΊβπ₯)) ⨣ (πΊβπ¦)) β (πΊβ((π
Β· π) + π¦)) = ((π
Γ (πΊβπ)) ⨣ (πΊβπ¦)))) |
23 | | oveq2 7370 |
. . . . . 6
β’ (π¦ = π β ((π
Β· π) + π¦) = ((π
Β· π) + π)) |
24 | 23 | fveq2d 6851 |
. . . . 5
β’ (π¦ = π β (πΊβ((π
Β· π) + π¦)) = (πΊβ((π
Β· π) + π))) |
25 | | fveq2 6847 |
. . . . . 6
β’ (π¦ = π β (πΊβπ¦) = (πΊβπ)) |
26 | 25 | oveq2d 7378 |
. . . . 5
β’ (π¦ = π β ((π
Γ (πΊβπ)) ⨣ (πΊβπ¦)) = ((π
Γ (πΊβπ)) ⨣ (πΊβπ))) |
27 | 24, 26 | eqeq12d 2753 |
. . . 4
β’ (π¦ = π β ((πΊβ((π
Β· π) + π¦)) = ((π
Γ (πΊβπ)) ⨣ (πΊβπ¦)) β (πΊβ((π
Β· π) + π)) = ((π
Γ (πΊβπ)) ⨣ (πΊβπ)))) |
28 | 16, 22, 27 | rspc3v 3596 |
. . 3
β’ ((π
β πΎ β§ π β π β§ π β π) β (βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)) β (πΊβ((π
Β· π) + π)) = ((π
Γ (πΊβπ)) ⨣ (πΊβπ)))) |
29 | 28 | 3ad2ant3 1136 |
. 2
β’ ((π β π β§ πΊ β πΉ β§ (π
β πΎ β§ π β π β§ π β π)) β (βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦)) β (πΊβ((π
Β· π) + π)) = ((π
Γ (πΊβπ)) ⨣ (πΊβπ)))) |
30 | 11, 29 | mpd 15 |
1
β’ ((π β π β§ πΊ β πΉ β§ (π
β πΎ β§ π β π β§ π β π)) β (πΊβ((π
Β· π) + π)) = ((π
Γ (πΊβπ)) ⨣ (πΊβπ))) |