Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(BaseβπΉ) =
(BaseβπΉ) |
2 | | ip2subdi.p |
. . . 4
β’ + =
(+gβπΉ) |
3 | | ipsubdir.s |
. . . 4
β’ π = (-gβπΉ) |
4 | | ip2subdi.1 |
. . . . . . 7
β’ (π β π β PreHil) |
5 | | phllmod 21057 |
. . . . . . 7
β’ (π β PreHil β π β LMod) |
6 | 4, 5 | syl 17 |
. . . . . 6
β’ (π β π β LMod) |
7 | | phlsrng.f |
. . . . . . 7
β’ πΉ = (Scalarβπ) |
8 | 7 | lmodring 20373 |
. . . . . 6
β’ (π β LMod β πΉ β Ring) |
9 | 6, 8 | syl 17 |
. . . . 5
β’ (π β πΉ β Ring) |
10 | | ringabl 20010 |
. . . . 5
β’ (πΉ β Ring β πΉ β Abel) |
11 | 9, 10 | syl 17 |
. . . 4
β’ (π β πΉ β Abel) |
12 | | ip2subdi.2 |
. . . . 5
β’ (π β π΄ β π) |
13 | | ip2subdi.4 |
. . . . 5
β’ (π β πΆ β π) |
14 | | phllmhm.h |
. . . . . 6
β’ , =
(Β·πβπ) |
15 | | phllmhm.v |
. . . . . 6
β’ π = (Baseβπ) |
16 | 7, 14, 15, 1 | ipcl 21060 |
. . . . 5
β’ ((π β PreHil β§ π΄ β π β§ πΆ β π) β (π΄ , πΆ) β (BaseβπΉ)) |
17 | 4, 12, 13, 16 | syl3anc 1372 |
. . . 4
β’ (π β (π΄ , πΆ) β (BaseβπΉ)) |
18 | | ip2subdi.5 |
. . . . 5
β’ (π β π· β π) |
19 | 7, 14, 15, 1 | ipcl 21060 |
. . . . 5
β’ ((π β PreHil β§ π΄ β π β§ π· β π) β (π΄ , π·) β (BaseβπΉ)) |
20 | 4, 12, 18, 19 | syl3anc 1372 |
. . . 4
β’ (π β (π΄ , π·) β (BaseβπΉ)) |
21 | | ip2subdi.3 |
. . . . 5
β’ (π β π΅ β π) |
22 | 7, 14, 15, 1 | ipcl 21060 |
. . . . 5
β’ ((π β PreHil β§ π΅ β π β§ πΆ β π) β (π΅ , πΆ) β (BaseβπΉ)) |
23 | 4, 21, 13, 22 | syl3anc 1372 |
. . . 4
β’ (π β (π΅ , πΆ) β (BaseβπΉ)) |
24 | 1, 2, 3, 11, 17, 20, 23 | ablsubsub4 19605 |
. . 3
β’ (π β (((π΄ , πΆ)π(π΄ , π·))π(π΅ , πΆ)) = ((π΄ , πΆ)π((π΄ , π·) + (π΅ , πΆ)))) |
25 | 24 | oveq1d 7376 |
. 2
β’ (π β ((((π΄ , πΆ)π(π΄ , π·))π(π΅ , πΆ)) + (π΅ , π·)) = (((π΄ , πΆ)π((π΄ , π·) + (π΅ , πΆ))) + (π΅ , π·))) |
26 | | ipsubdir.m |
. . . . . 6
β’ β =
(-gβπ) |
27 | 15, 26 | lmodvsubcl 20411 |
. . . . 5
β’ ((π β LMod β§ πΆ β π β§ π· β π) β (πΆ β π·) β π) |
28 | 6, 13, 18, 27 | syl3anc 1372 |
. . . 4
β’ (π β (πΆ β π·) β π) |
29 | 7, 14, 15, 26, 3 | ipsubdir 21069 |
. . . 4
β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ (πΆ β π·) β π)) β ((π΄ β π΅) , (πΆ β π·)) = ((π΄ , (πΆ β π·))π(π΅ , (πΆ β π·)))) |
30 | 4, 12, 21, 28, 29 | syl13anc 1373 |
. . 3
β’ (π β ((π΄ β π΅) , (πΆ β π·)) = ((π΄ , (πΆ β π·))π(π΅ , (πΆ β π·)))) |
31 | 7, 14, 15, 26, 3 | ipsubdi 21070 |
. . . . 5
β’ ((π β PreHil β§ (π΄ β π β§ πΆ β π β§ π· β π)) β (π΄ , (πΆ β π·)) = ((π΄ , πΆ)π(π΄ , π·))) |
32 | 4, 12, 13, 18, 31 | syl13anc 1373 |
. . . 4
β’ (π β (π΄ , (πΆ β π·)) = ((π΄ , πΆ)π(π΄ , π·))) |
33 | 7, 14, 15, 26, 3 | ipsubdi 21070 |
. . . . 5
β’ ((π β PreHil β§ (π΅ β π β§ πΆ β π β§ π· β π)) β (π΅ , (πΆ β π·)) = ((π΅ , πΆ)π(π΅ , π·))) |
34 | 4, 21, 13, 18, 33 | syl13anc 1373 |
. . . 4
β’ (π β (π΅ , (πΆ β π·)) = ((π΅ , πΆ)π(π΅ , π·))) |
35 | 32, 34 | oveq12d 7379 |
. . 3
β’ (π β ((π΄ , (πΆ β π·))π(π΅ , (πΆ β π·))) = (((π΄ , πΆ)π(π΄ , π·))π((π΅ , πΆ)π(π΅ , π·)))) |
36 | | ringgrp 19977 |
. . . . . 6
β’ (πΉ β Ring β πΉ β Grp) |
37 | 9, 36 | syl 17 |
. . . . 5
β’ (π β πΉ β Grp) |
38 | 1, 3 | grpsubcl 18835 |
. . . . 5
β’ ((πΉ β Grp β§ (π΄ , πΆ) β (BaseβπΉ) β§ (π΄ , π·) β (BaseβπΉ)) β ((π΄ , πΆ)π(π΄ , π·)) β (BaseβπΉ)) |
39 | 37, 17, 20, 38 | syl3anc 1372 |
. . . 4
β’ (π β ((π΄ , πΆ)π(π΄ , π·)) β (BaseβπΉ)) |
40 | 7, 14, 15, 1 | ipcl 21060 |
. . . . 5
β’ ((π β PreHil β§ π΅ β π β§ π· β π) β (π΅ , π·) β (BaseβπΉ)) |
41 | 4, 21, 18, 40 | syl3anc 1372 |
. . . 4
β’ (π β (π΅ , π·) β (BaseβπΉ)) |
42 | 1, 2, 3, 11, 39, 23, 41 | ablsubsub 19604 |
. . 3
β’ (π β (((π΄ , πΆ)π(π΄ , π·))π((π΅ , πΆ)π(π΅ , π·))) = ((((π΄ , πΆ)π(π΄ , π·))π(π΅ , πΆ)) + (π΅ , π·))) |
43 | 30, 35, 42 | 3eqtrd 2777 |
. 2
β’ (π β ((π΄ β π΅) , (πΆ β π·)) = ((((π΄ , πΆ)π(π΄ , π·))π(π΅ , πΆ)) + (π΅ , π·))) |
44 | 1, 2 | ringacl 20007 |
. . . 4
β’ ((πΉ β Ring β§ (π΄ , π·) β (BaseβπΉ) β§ (π΅ , πΆ) β (BaseβπΉ)) β ((π΄ , π·) + (π΅ , πΆ)) β (BaseβπΉ)) |
45 | 9, 20, 23, 44 | syl3anc 1372 |
. . 3
β’ (π β ((π΄ , π·) + (π΅ , πΆ)) β (BaseβπΉ)) |
46 | 1, 2, 3 | abladdsub 19601 |
. . 3
β’ ((πΉ β Abel β§ ((π΄ , πΆ) β (BaseβπΉ) β§ (π΅ , π·) β (BaseβπΉ) β§ ((π΄ , π·) + (π΅ , πΆ)) β (BaseβπΉ))) β (((π΄ , πΆ) + (π΅ , π·))π((π΄ , π·) + (π΅ , πΆ))) = (((π΄ , πΆ)π((π΄ , π·) + (π΅ , πΆ))) + (π΅ , π·))) |
47 | 11, 17, 41, 45, 46 | syl13anc 1373 |
. 2
β’ (π β (((π΄ , πΆ) + (π΅ , π·))π((π΄ , π·) + (π΅ , πΆ))) = (((π΄ , πΆ)π((π΄ , π·) + (π΅ , πΆ))) + (π΅ , π·))) |
48 | 25, 43, 47 | 3eqtr4d 2783 |
1
β’ (π β ((π΄ β π΅) , (πΆ β π·)) = (((π΄ , πΆ) + (π΅ , π·))π((π΄ , π·) + (π΅ , πΆ)))) |