Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . 5
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β π β PreHil) |
2 | | simpr3 1197 |
. . . . 5
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β πΆ β πΎ) |
3 | | simpr2 1196 |
. . . . 5
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β π΅ β π) |
4 | | simpr1 1195 |
. . . . 5
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β π΄ β π) |
5 | | phlsrng.f |
. . . . . 6
β’ πΉ = (Scalarβπ) |
6 | | phllmhm.h |
. . . . . 6
β’ , =
(Β·πβπ) |
7 | | phllmhm.v |
. . . . . 6
β’ π = (Baseβπ) |
8 | | ipdir.f |
. . . . . 6
β’ πΎ = (BaseβπΉ) |
9 | | ipass.s |
. . . . . 6
β’ Β· = (
Β·π βπ) |
10 | | ipass.p |
. . . . . 6
β’ Γ =
(.rβπΉ) |
11 | 5, 6, 7, 8, 9, 10 | ipass 21072 |
. . . . 5
β’ ((π β PreHil β§ (πΆ β πΎ β§ π΅ β π β§ π΄ β π)) β ((πΆ Β· π΅) , π΄) = (πΆ Γ (π΅ , π΄))) |
12 | 1, 2, 3, 4, 11 | syl13anc 1373 |
. . . 4
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β ((πΆ Β· π΅) , π΄) = (πΆ Γ (π΅ , π΄))) |
13 | 12 | fveq2d 6850 |
. . 3
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β ( β β((πΆ Β· π΅) , π΄)) = ( β β(πΆ Γ (π΅ , π΄)))) |
14 | | phllmod 21057 |
. . . . . 6
β’ (π β PreHil β π β LMod) |
15 | 14 | adantr 482 |
. . . . 5
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β π β LMod) |
16 | 7, 5, 9, 8 | lmodvscl 20383 |
. . . . 5
β’ ((π β LMod β§ πΆ β πΎ β§ π΅ β π) β (πΆ Β· π΅) β π) |
17 | 15, 2, 3, 16 | syl3anc 1372 |
. . . 4
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β (πΆ Β· π΅) β π) |
18 | | ipassr.i |
. . . . 5
β’ β =
(*πβπΉ) |
19 | 5, 6, 7, 18 | ipcj 21061 |
. . . 4
β’ ((π β PreHil β§ (πΆ Β· π΅) β π β§ π΄ β π) β ( β β((πΆ Β· π΅) , π΄)) = (π΄ , (πΆ Β· π΅))) |
20 | 1, 17, 4, 19 | syl3anc 1372 |
. . 3
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β ( β β((πΆ Β· π΅) , π΄)) = (π΄ , (πΆ Β· π΅))) |
21 | 5 | phlsrng 21058 |
. . . . 5
β’ (π β PreHil β πΉ β *-Ring) |
22 | 21 | adantr 482 |
. . . 4
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β πΉ β *-Ring) |
23 | 5, 6, 7, 8 | ipcl 21060 |
. . . . 5
β’ ((π β PreHil β§ π΅ β π β§ π΄ β π) β (π΅ , π΄) β πΎ) |
24 | 1, 3, 4, 23 | syl3anc 1372 |
. . . 4
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β (π΅ , π΄) β πΎ) |
25 | 18, 8, 10 | srngmul 20360 |
. . . 4
β’ ((πΉ β *-Ring β§ πΆ β πΎ β§ (π΅ , π΄) β πΎ) β ( β β(πΆ Γ (π΅ , π΄))) = (( β β(π΅ , π΄)) Γ ( β βπΆ))) |
26 | 22, 2, 24, 25 | syl3anc 1372 |
. . 3
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β ( β β(πΆ Γ (π΅ , π΄))) = (( β β(π΅ , π΄)) Γ ( β βπΆ))) |
27 | 13, 20, 26 | 3eqtr3d 2781 |
. 2
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β (π΄ , (πΆ Β· π΅)) = (( β β(π΅ , π΄)) Γ ( β βπΆ))) |
28 | 5, 6, 7, 18 | ipcj 21061 |
. . . 4
β’ ((π β PreHil β§ π΅ β π β§ π΄ β π) β ( β β(π΅ , π΄)) = (π΄ , π΅)) |
29 | 1, 3, 4, 28 | syl3anc 1372 |
. . 3
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β ( β β(π΅ , π΄)) = (π΄ , π΅)) |
30 | 29 | oveq1d 7376 |
. 2
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β (( β β(π΅ , π΄)) Γ ( β βπΆ)) = ((π΄ , π΅) Γ ( β βπΆ))) |
31 | 27, 30 | eqtrd 2773 |
1
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β (π΄ , (πΆ Β· π΅)) = ((π΄ , π΅) Γ ( β βπΆ))) |