Step | Hyp | Ref
| Expression |
1 | | phlsrng.f |
. . . . . 6
β’ πΉ = (Scalarβπ) |
2 | | phllmhm.h |
. . . . . 6
β’ , =
(Β·πβπ) |
3 | | phllmhm.v |
. . . . . 6
β’ π = (Baseβπ) |
4 | | eqid 2733 |
. . . . . 6
β’ (π₯ β π β¦ (π₯ , πΆ)) = (π₯ β π β¦ (π₯ , πΆ)) |
5 | 1, 2, 3, 4 | phllmhm 21052 |
. . . . 5
β’ ((π β PreHil β§ πΆ β π) β (π₯ β π β¦ (π₯ , πΆ)) β (π LMHom (ringLModβπΉ))) |
6 | 5 | 3ad2antr3 1191 |
. . . 4
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π₯ β π β¦ (π₯ , πΆ)) β (π LMHom (ringLModβπΉ))) |
7 | | lmghm 20507 |
. . . 4
β’ ((π₯ β π β¦ (π₯ , πΆ)) β (π LMHom (ringLModβπΉ)) β (π₯ β π β¦ (π₯ , πΆ)) β (π GrpHom (ringLModβπΉ))) |
8 | 6, 7 | syl 17 |
. . 3
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π₯ β π β¦ (π₯ , πΆ)) β (π GrpHom (ringLModβπΉ))) |
9 | | simpr1 1195 |
. . 3
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β π΄ β π) |
10 | | simpr2 1196 |
. . 3
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β π΅ β π) |
11 | | ipdir.g |
. . . 4
β’ + =
(+gβπ) |
12 | | ipdir.p |
. . . . 5
⒠⨣ =
(+gβπΉ) |
13 | | rlmplusg 20681 |
. . . . 5
β’
(+gβπΉ) =
(+gβ(ringLModβπΉ)) |
14 | 12, 13 | eqtri 2761 |
. . . 4
⒠⨣ =
(+gβ(ringLModβπΉ)) |
15 | 3, 11, 14 | ghmlin 19018 |
. . 3
β’ (((π₯ β π β¦ (π₯ , πΆ)) β (π GrpHom (ringLModβπΉ)) β§ π΄ β π β§ π΅ β π) β ((π₯ β π β¦ (π₯ , πΆ))β(π΄ + π΅)) = (((π₯ β π β¦ (π₯ , πΆ))βπ΄) ⨣ ((π₯ β π β¦ (π₯ , πΆ))βπ΅))) |
16 | 8, 9, 10, 15 | syl3anc 1372 |
. 2
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π₯ β π β¦ (π₯ , πΆ))β(π΄ + π΅)) = (((π₯ β π β¦ (π₯ , πΆ))βπ΄) ⨣ ((π₯ β π β¦ (π₯ , πΆ))βπ΅))) |
17 | | phllmod 21050 |
. . . . 5
β’ (π β PreHil β π β LMod) |
18 | 3, 11 | lmodvacl 20351 |
. . . . 5
β’ ((π β LMod β§ π΄ β π β§ π΅ β π) β (π΄ + π΅) β π) |
19 | 17, 18 | syl3an1 1164 |
. . . 4
β’ ((π β PreHil β§ π΄ β π β§ π΅ β π) β (π΄ + π΅) β π) |
20 | 19 | 3adant3r3 1185 |
. . 3
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄ + π΅) β π) |
21 | | oveq1 7365 |
. . . 4
β’ (π₯ = (π΄ + π΅) β (π₯ , πΆ) = ((π΄ + π΅) , πΆ)) |
22 | | ovex 7391 |
. . . 4
β’ (π₯ , πΆ) β V |
23 | 21, 4, 22 | fvmpt3i 6954 |
. . 3
β’ ((π΄ + π΅) β π β ((π₯ β π β¦ (π₯ , πΆ))β(π΄ + π΅)) = ((π΄ + π΅) , πΆ)) |
24 | 20, 23 | syl 17 |
. 2
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π₯ β π β¦ (π₯ , πΆ))β(π΄ + π΅)) = ((π΄ + π΅) , πΆ)) |
25 | | oveq1 7365 |
. . . . 5
β’ (π₯ = π΄ β (π₯ , πΆ) = (π΄ , πΆ)) |
26 | 25, 4, 22 | fvmpt3i 6954 |
. . . 4
β’ (π΄ β π β ((π₯ β π β¦ (π₯ , πΆ))βπ΄) = (π΄ , πΆ)) |
27 | 9, 26 | syl 17 |
. . 3
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π₯ β π β¦ (π₯ , πΆ))βπ΄) = (π΄ , πΆ)) |
28 | | oveq1 7365 |
. . . . 5
β’ (π₯ = π΅ β (π₯ , πΆ) = (π΅ , πΆ)) |
29 | 28, 4, 22 | fvmpt3i 6954 |
. . . 4
β’ (π΅ β π β ((π₯ β π β¦ (π₯ , πΆ))βπ΅) = (π΅ , πΆ)) |
30 | 10, 29 | syl 17 |
. . 3
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π₯ β π β¦ (π₯ , πΆ))βπ΅) = (π΅ , πΆ)) |
31 | 27, 30 | oveq12d 7376 |
. 2
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (((π₯ β π β¦ (π₯ , πΆ))βπ΄) ⨣ ((π₯ β π β¦ (π₯ , πΆ))βπ΅)) = ((π΄ , πΆ) ⨣ (π΅ , πΆ))) |
32 | 16, 24, 31 | 3eqtr3d 2781 |
1
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ + π΅) , πΆ) = ((π΄ , πΆ) ⨣ (π΅ , πΆ))) |