Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . 3
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β π β AssAlg) |
2 | | simpr 485 |
. . . 4
β’ ((π΄ β π΅ β§ πΆ β π΅) β πΆ β π΅) |
3 | 2 | 3ad2ant2 1134 |
. . 3
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β πΆ β π΅) |
4 | | assalmod 21406 |
. . . 4
β’ (π β AssAlg β π β LMod) |
5 | | simpl 483 |
. . . 4
β’ ((π΄ β π΅ β§ πΆ β π΅) β π΄ β π΅) |
6 | | simpl 483 |
. . . 4
β’ ((π β π β§ π β π) β π β π) |
7 | | assa2ass.v |
. . . . 5
β’ π = (Baseβπ) |
8 | | assa2ass.f |
. . . . 5
β’ πΉ = (Scalarβπ) |
9 | | assa2ass.s |
. . . . 5
β’ Β· = (
Β·π βπ) |
10 | | assa2ass.b |
. . . . 5
β’ π΅ = (BaseβπΉ) |
11 | 7, 8, 9, 10 | lmodvscl 20481 |
. . . 4
β’ ((π β LMod β§ π΄ β π΅ β§ π β π) β (π΄ Β· π) β π) |
12 | 4, 5, 6, 11 | syl3an 1160 |
. . 3
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β (π΄ Β· π) β π) |
13 | | simpr 485 |
. . . 4
β’ ((π β π β§ π β π) β π β π) |
14 | 13 | 3ad2ant3 1135 |
. . 3
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β π β π) |
15 | | assa2ass.t |
. . . 4
β’ Γ =
(.rβπ) |
16 | 7, 8, 10, 9, 15 | assaassr 21405 |
. . 3
β’ ((π β AssAlg β§ (πΆ β π΅ β§ (π΄ Β· π) β π β§ π β π)) β ((π΄ Β· π) Γ (πΆ Β· π)) = (πΆ Β· ((π΄ Β· π) Γ π))) |
17 | 1, 3, 12, 14, 16 | syl13anc 1372 |
. 2
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β ((π΄ Β· π) Γ (πΆ Β· π)) = (πΆ Β· ((π΄ Β· π) Γ π))) |
18 | 7, 8, 10, 9, 15 | assaass 21404 |
. . . 4
β’ ((π β AssAlg β§ (πΆ β π΅ β§ (π΄ Β· π) β π β§ π β π)) β ((πΆ Β· (π΄ Β· π)) Γ π) = (πΆ Β· ((π΄ Β· π) Γ π))) |
19 | 18 | eqcomd 2738 |
. . 3
β’ ((π β AssAlg β§ (πΆ β π΅ β§ (π΄ Β· π) β π β§ π β π)) β (πΆ Β· ((π΄ Β· π) Γ π)) = ((πΆ Β· (π΄ Β· π)) Γ π)) |
20 | 1, 3, 12, 14, 19 | syl13anc 1372 |
. 2
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β (πΆ Β· ((π΄ Β· π) Γ π)) = ((πΆ Β· (π΄ Β· π)) Γ π)) |
21 | 4 | 3ad2ant1 1133 |
. . . 4
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β π β LMod) |
22 | 5 | 3ad2ant2 1134 |
. . . 4
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β π΄ β π΅) |
23 | 6 | 3ad2ant3 1135 |
. . . 4
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β π β π) |
24 | | assa2ass.m |
. . . . . . 7
β’ β =
(.rβπΉ) |
25 | 7, 8, 9, 10, 24 | lmodvsass 20489 |
. . . . . 6
β’ ((π β LMod β§ (πΆ β π΅ β§ π΄ β π΅ β§ π β π)) β ((πΆ β π΄) Β· π) = (πΆ Β· (π΄ Β· π))) |
26 | 25 | eqcomd 2738 |
. . . . 5
β’ ((π β LMod β§ (πΆ β π΅ β§ π΄ β π΅ β§ π β π)) β (πΆ Β· (π΄ Β· π)) = ((πΆ β π΄) Β· π)) |
27 | 26 | oveq1d 7420 |
. . . 4
β’ ((π β LMod β§ (πΆ β π΅ β§ π΄ β π΅ β§ π β π)) β ((πΆ Β· (π΄ Β· π)) Γ π) = (((πΆ β π΄) Β· π) Γ π)) |
28 | 21, 3, 22, 23, 27 | syl13anc 1372 |
. . 3
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β ((πΆ Β· (π΄ Β· π)) Γ π) = (((πΆ β π΄) Β· π) Γ π)) |
29 | 8 | assasca 21408 |
. . . . . . 7
β’ (π β AssAlg β πΉ β Ring) |
30 | 29 | adantr 481 |
. . . . . 6
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅)) β πΉ β Ring) |
31 | 2 | adantl 482 |
. . . . . 6
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅)) β πΆ β π΅) |
32 | 5 | adantl 482 |
. . . . . 6
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅)) β π΄ β π΅) |
33 | 10, 24 | ringcl 20066 |
. . . . . 6
β’ ((πΉ β Ring β§ πΆ β π΅ β§ π΄ β π΅) β (πΆ β π΄) β π΅) |
34 | 30, 31, 32, 33 | syl3anc 1371 |
. . . . 5
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅)) β (πΆ β π΄) β π΅) |
35 | 34 | 3adant3 1132 |
. . . 4
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β (πΆ β π΄) β π΅) |
36 | 7, 8, 10, 9, 15 | assaass 21404 |
. . . 4
β’ ((π β AssAlg β§ ((πΆ β π΄) β π΅ β§ π β π β§ π β π)) β (((πΆ β π΄) Β· π) Γ π) = ((πΆ β π΄) Β· (π Γ π))) |
37 | 1, 35, 23, 14, 36 | syl13anc 1372 |
. . 3
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β (((πΆ β π΄) Β· π) Γ π) = ((πΆ β π΄) Β· (π Γ π))) |
38 | 28, 37 | eqtrd 2772 |
. 2
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β ((πΆ Β· (π΄ Β· π)) Γ π) = ((πΆ β π΄) Β· (π Γ π))) |
39 | 17, 20, 38 | 3eqtrd 2776 |
1
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β ((π΄ Β· π) Γ (πΆ Β· π)) = ((πΆ β π΄) Β· (π Γ π))) |