Step | Hyp | Ref
| Expression |
1 | | oveq1 7365 |
. . . . . . 7
β’ (π₯ = 0 β (π₯πΈ(π΄ Β· π)) = (0πΈ(π΄ Β· π))) |
2 | | oveq1 7365 |
. . . . . . . 8
β’ (π₯ = 0 β (π₯ β π΄) = (0 β π΄)) |
3 | | oveq1 7365 |
. . . . . . . 8
β’ (π₯ = 0 β (π₯πΈπ) = (0πΈπ)) |
4 | 2, 3 | oveq12d 7376 |
. . . . . . 7
β’ (π₯ = 0 β ((π₯ β π΄) Β· (π₯πΈπ)) = ((0 β π΄) Β· (0πΈπ))) |
5 | 1, 4 | eqeq12d 2749 |
. . . . . 6
β’ (π₯ = 0 β ((π₯πΈ(π΄ Β· π)) = ((π₯ β π΄) Β· (π₯πΈπ)) β (0πΈ(π΄ Β· π)) = ((0 β π΄) Β· (0πΈπ)))) |
6 | 5 | imbi2d 341 |
. . . . 5
β’ (π₯ = 0 β ((((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (π₯πΈ(π΄ Β· π)) = ((π₯ β π΄) Β· (π₯πΈπ))) β (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (0πΈ(π΄ Β· π)) = ((0 β π΄) Β· (0πΈπ))))) |
7 | | oveq1 7365 |
. . . . . . 7
β’ (π₯ = π¦ β (π₯πΈ(π΄ Β· π)) = (π¦πΈ(π΄ Β· π))) |
8 | | oveq1 7365 |
. . . . . . . 8
β’ (π₯ = π¦ β (π₯ β π΄) = (π¦ β π΄)) |
9 | | oveq1 7365 |
. . . . . . . 8
β’ (π₯ = π¦ β (π₯πΈπ) = (π¦πΈπ)) |
10 | 8, 9 | oveq12d 7376 |
. . . . . . 7
β’ (π₯ = π¦ β ((π₯ β π΄) Β· (π₯πΈπ)) = ((π¦ β π΄) Β· (π¦πΈπ))) |
11 | 7, 10 | eqeq12d 2749 |
. . . . . 6
β’ (π₯ = π¦ β ((π₯πΈ(π΄ Β· π)) = ((π₯ β π΄) Β· (π₯πΈπ)) β (π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ)))) |
12 | 11 | imbi2d 341 |
. . . . 5
β’ (π₯ = π¦ β ((((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (π₯πΈ(π΄ Β· π)) = ((π₯ β π΄) Β· (π₯πΈπ))) β (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ))))) |
13 | | oveq1 7365 |
. . . . . . 7
β’ (π₯ = (π¦ + 1) β (π₯πΈ(π΄ Β· π)) = ((π¦ + 1)πΈ(π΄ Β· π))) |
14 | | oveq1 7365 |
. . . . . . . 8
β’ (π₯ = (π¦ + 1) β (π₯ β π΄) = ((π¦ + 1) β π΄)) |
15 | | oveq1 7365 |
. . . . . . . 8
β’ (π₯ = (π¦ + 1) β (π₯πΈπ) = ((π¦ + 1)πΈπ)) |
16 | 14, 15 | oveq12d 7376 |
. . . . . . 7
β’ (π₯ = (π¦ + 1) β ((π₯ β π΄) Β· (π₯πΈπ)) = (((π¦ + 1) β π΄) Β· ((π¦ + 1)πΈπ))) |
17 | 13, 16 | eqeq12d 2749 |
. . . . . 6
β’ (π₯ = (π¦ + 1) β ((π₯πΈ(π΄ Β· π)) = ((π₯ β π΄) Β· (π₯πΈπ)) β ((π¦ + 1)πΈ(π΄ Β· π)) = (((π¦ + 1) β π΄) Β· ((π¦ + 1)πΈπ)))) |
18 | 17 | imbi2d 341 |
. . . . 5
β’ (π₯ = (π¦ + 1) β ((((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (π₯πΈ(π΄ Β· π)) = ((π₯ β π΄) Β· (π₯πΈπ))) β (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β ((π¦ + 1)πΈ(π΄ Β· π)) = (((π¦ + 1) β π΄) Β· ((π¦ + 1)πΈπ))))) |
19 | | oveq1 7365 |
. . . . . . 7
β’ (π₯ = π β (π₯πΈ(π΄ Β· π)) = (ππΈ(π΄ Β· π))) |
20 | | oveq1 7365 |
. . . . . . . 8
β’ (π₯ = π β (π₯ β π΄) = (π β π΄)) |
21 | | oveq1 7365 |
. . . . . . . 8
β’ (π₯ = π β (π₯πΈπ) = (ππΈπ)) |
22 | 20, 21 | oveq12d 7376 |
. . . . . . 7
β’ (π₯ = π β ((π₯ β π΄) Β· (π₯πΈπ)) = ((π β π΄) Β· (ππΈπ))) |
23 | 19, 22 | eqeq12d 2749 |
. . . . . 6
β’ (π₯ = π β ((π₯πΈ(π΄ Β· π)) = ((π₯ β π΄) Β· (π₯πΈπ)) β (ππΈ(π΄ Β· π)) = ((π β π΄) Β· (ππΈπ)))) |
24 | 23 | imbi2d 341 |
. . . . 5
β’ (π₯ = π β ((((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (π₯πΈ(π΄ Β· π)) = ((π₯ β π΄) Β· (π₯πΈπ))) β (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (ππΈ(π΄ Β· π)) = ((π β π΄) Β· (ππΈπ))))) |
25 | | assamulgscm.v |
. . . . . 6
β’ π = (Baseβπ) |
26 | | assamulgscm.f |
. . . . . 6
β’ πΉ = (Scalarβπ) |
27 | | assamulgscm.b |
. . . . . 6
β’ π΅ = (BaseβπΉ) |
28 | | assamulgscm.s |
. . . . . 6
β’ Β· = (
Β·π βπ) |
29 | | assamulgscm.g |
. . . . . 6
β’ πΊ = (mulGrpβπΉ) |
30 | | assamulgscm.p |
. . . . . 6
β’ β =
(.gβπΊ) |
31 | | assamulgscm.h |
. . . . . 6
β’ π» = (mulGrpβπ) |
32 | | assamulgscm.e |
. . . . . 6
β’ πΈ = (.gβπ») |
33 | 25, 26, 27, 28, 29, 30, 31, 32 | assamulgscmlem1 21318 |
. . . . 5
β’ (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (0πΈ(π΄ Β· π)) = ((0 β π΄) Β· (0πΈπ))) |
34 | 25, 26, 27, 28, 29, 30, 31, 32 | assamulgscmlem2 21319 |
. . . . . 6
β’ (π¦ β β0
β (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β ((π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ)) β ((π¦ + 1)πΈ(π΄ Β· π)) = (((π¦ + 1) β π΄) Β· ((π¦ + 1)πΈπ))))) |
35 | 34 | a2d 29 |
. . . . 5
β’ (π¦ β β0
β ((((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (π¦πΈ(π΄ Β· π)) = ((π¦ β π΄) Β· (π¦πΈπ))) β (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β ((π¦ + 1)πΈ(π΄ Β· π)) = (((π¦ + 1) β π΄) Β· ((π¦ + 1)πΈπ))))) |
36 | 6, 12, 18, 24, 33, 35 | nn0ind 12603 |
. . . 4
β’ (π β β0
β (((π΄ β π΅ β§ π β π) β§ π β AssAlg) β (ππΈ(π΄ Β· π)) = ((π β π΄) Β· (ππΈπ)))) |
37 | 36 | exp4c 434 |
. . 3
β’ (π β β0
β (π΄ β π΅ β (π β π β (π β AssAlg β (ππΈ(π΄ Β· π)) = ((π β π΄) Β· (ππΈπ)))))) |
38 | 37 | 3imp 1112 |
. 2
β’ ((π β β0
β§ π΄ β π΅ β§ π β π) β (π β AssAlg β (ππΈ(π΄ Β· π)) = ((π β π΄) Β· (ππΈπ)))) |
39 | 38 | impcom 409 |
1
β’ ((π β AssAlg β§ (π β β0
β§ π΄ β π΅ β§ π β π)) β (ππΈ(π΄ Β· π)) = ((π β π΄) Β· (ππΈπ))) |