Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β π β AssAlg) |
2 | | simpr 486 |
. . . 4
β’ ((π΄ β π΅ β§ πΆ β π΅) β πΆ β π΅) |
3 | 2 | 3ad2ant2 1135 |
. . 3
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β πΆ β π΅) |
4 | | assalmod 21282 |
. . . 4
β’ (π β AssAlg β π β LMod) |
5 | | simpl 484 |
. . . 4
β’ ((π΄ β π΅ β§ πΆ β π΅) β π΄ β π΅) |
6 | | simpl 484 |
. . . 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 20354 |
. . . 4
β’ ((π β LMod β§ π΄ β π΅ β§ π β π) β (π΄ Β· π) β π) |
12 | 4, 5, 6, 11 | syl3an 1161 |
. . 3
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β (π΄ Β· π) β π) |
13 | | simpr 486 |
. . . 4
β’ ((π β π β§ π β π) β π β π) |
14 | 13 | 3ad2ant3 1136 |
. . 3
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β π β π) |
15 | | assa2ass.t |
. . . 4
β’ Γ =
(.rβπ) |
16 | 7, 8, 10, 9, 15 | assaassr 21281 |
. . 3
β’ ((π β AssAlg β§ (πΆ β π΅ β§ (π΄ Β· π) β π β§ π β π)) β ((π΄ Β· π) Γ (πΆ Β· π)) = (πΆ Β· ((π΄ Β· π) Γ π))) |
17 | 1, 3, 12, 14, 16 | syl13anc 1373 |
. 2
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β ((π΄ Β· π) Γ (πΆ Β· π)) = (πΆ Β· ((π΄ Β· π) Γ π))) |
18 | 7, 8, 10, 9, 15 | assaass 21280 |
. . . 4
β’ ((π β AssAlg β§ (πΆ β π΅ β§ (π΄ Β· π) β π β§ π β π)) β ((πΆ Β· (π΄ Β· π)) Γ π) = (πΆ Β· ((π΄ Β· π) Γ π))) |
19 | 18 | eqcomd 2739 |
. . 3
β’ ((π β AssAlg β§ (πΆ β π΅ β§ (π΄ Β· π) β π β§ π β π)) β (πΆ Β· ((π΄ Β· π) Γ π)) = ((πΆ Β· (π΄ Β· π)) Γ π)) |
20 | 1, 3, 12, 14, 19 | syl13anc 1373 |
. 2
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β (πΆ Β· ((π΄ Β· π) Γ π)) = ((πΆ Β· (π΄ Β· π)) Γ π)) |
21 | 4 | 3ad2ant1 1134 |
. . . 4
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β π β LMod) |
22 | 5 | 3ad2ant2 1135 |
. . . 4
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β π΄ β π΅) |
23 | 6 | 3ad2ant3 1136 |
. . . 4
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β π β π) |
24 | | assa2ass.m |
. . . . . . 7
β’ β =
(.rβπΉ) |
25 | 7, 8, 9, 10, 24 | lmodvsass 20362 |
. . . . . 6
β’ ((π β LMod β§ (πΆ β π΅ β§ π΄ β π΅ β§ π β π)) β ((πΆ β π΄) Β· π) = (πΆ Β· (π΄ Β· π))) |
26 | 25 | eqcomd 2739 |
. . . . 5
β’ ((π β LMod β§ (πΆ β π΅ β§ π΄ β π΅ β§ π β π)) β (πΆ Β· (π΄ Β· π)) = ((πΆ β π΄) Β· π)) |
27 | 26 | oveq1d 7373 |
. . . 4
β’ ((π β LMod β§ (πΆ β π΅ β§ π΄ β π΅ β§ π β π)) β ((πΆ Β· (π΄ Β· π)) Γ π) = (((πΆ β π΄) Β· π) Γ π)) |
28 | 21, 3, 22, 23, 27 | syl13anc 1373 |
. . 3
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β ((πΆ Β· (π΄ Β· π)) Γ π) = (((πΆ β π΄) Β· π) Γ π)) |
29 | 8 | assasca 21284 |
. . . . . . . 8
β’ (π β AssAlg β πΉ β CRing) |
30 | | crngring 19981 |
. . . . . . . 8
β’ (πΉ β CRing β πΉ β Ring) |
31 | 29, 30 | syl 17 |
. . . . . . 7
β’ (π β AssAlg β πΉ β Ring) |
32 | 31 | adantr 482 |
. . . . . 6
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅)) β πΉ β Ring) |
33 | 2 | adantl 483 |
. . . . . 6
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅)) β πΆ β π΅) |
34 | 5 | adantl 483 |
. . . . . 6
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅)) β π΄ β π΅) |
35 | 10, 24 | ringcl 19986 |
. . . . . 6
β’ ((πΉ β Ring β§ πΆ β π΅ β§ π΄ β π΅) β (πΆ β π΄) β π΅) |
36 | 32, 33, 34, 35 | syl3anc 1372 |
. . . . 5
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅)) β (πΆ β π΄) β π΅) |
37 | 36 | 3adant3 1133 |
. . . 4
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β (πΆ β π΄) β π΅) |
38 | 7, 8, 10, 9, 15 | assaass 21280 |
. . . 4
β’ ((π β AssAlg β§ ((πΆ β π΄) β π΅ β§ π β π β§ π β π)) β (((πΆ β π΄) Β· π) Γ π) = ((πΆ β π΄) Β· (π Γ π))) |
39 | 1, 37, 23, 14, 38 | syl13anc 1373 |
. . 3
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β (((πΆ β π΄) Β· π) Γ π) = ((πΆ β π΄) Β· (π Γ π))) |
40 | 28, 39 | eqtrd 2773 |
. 2
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β ((πΆ Β· (π΄ Β· π)) Γ π) = ((πΆ β π΄) Β· (π Γ π))) |
41 | 17, 20, 40 | 3eqtrd 2777 |
1
β’ ((π β AssAlg β§ (π΄ β π΅ β§ πΆ β π΅) β§ (π β π β§ π β π)) β ((π΄ Β· π) Γ (πΆ Β· π)) = ((πΆ β π΄) Β· (π Γ π))) |