Step | Hyp | Ref
| Expression |
1 | | eqgvscpbl.m |
. . . . . 6
β’ (π β π β LMod) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β π β LMod) |
3 | | eqgvscpbl.k |
. . . . . 6
β’ (π β πΎ β π) |
4 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β πΎ β π) |
5 | | simpr1 1195 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β π β π΅) |
6 | | eqgvscpbl.v |
. . . . . 6
β’ π΅ = (Baseβπ) |
7 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
8 | | eqgvscpbl.p |
. . . . . 6
β’ Β· = (
Β·π βπ) |
9 | | eqgvscpbl.s |
. . . . . 6
β’ π =
(Baseβ(Scalarβπ)) |
10 | 6, 7, 8, 9 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ πΎ β π β§ π β π΅) β (πΎ Β· π) β π΅) |
11 | 2, 4, 5, 10 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β (πΎ Β· π) β π΅) |
12 | | simpr2 1196 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β π β π΅) |
13 | 6, 7, 8, 9 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ πΎ β π β§ π β π΅) β (πΎ Β· π) β π΅) |
14 | 2, 4, 12, 13 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β (πΎ Β· π) β π΅) |
15 | 1 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π β π΅) β π β LMod) |
16 | 3 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π β π΅) β πΎ β π) |
17 | | lmodgrp 20343 |
. . . . . . . . . . 11
β’ (π β LMod β π β Grp) |
18 | 15, 17 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ π β π΅) β π β Grp) |
19 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ π β π΅) β π β π΅) |
20 | | eqid 2733 |
. . . . . . . . . . 11
β’
(invgβπ) = (invgβπ) |
21 | 6, 20 | grpinvcl 18803 |
. . . . . . . . . 10
β’ ((π β Grp β§ π β π΅) β ((invgβπ)βπ) β π΅) |
22 | 18, 19, 21 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π β π΅) β ((invgβπ)βπ) β π΅) |
23 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π β π΅) β π β π΅) |
24 | | eqid 2733 |
. . . . . . . . . 10
β’
(+gβπ) = (+gβπ) |
25 | 6, 24, 7, 8, 9 | lmodvsdi 20360 |
. . . . . . . . 9
β’ ((π β LMod β§ (πΎ β π β§ ((invgβπ)βπ) β π΅ β§ π β π΅)) β (πΎ Β·
(((invgβπ)βπ)(+gβπ)π)) = ((πΎ Β·
((invgβπ)βπ))(+gβπ)(πΎ Β· π))) |
26 | 15, 16, 22, 23, 25 | syl13anc 1373 |
. . . . . . . 8
β’ (((π β§ π β π΅) β§ π β π΅) β (πΎ Β·
(((invgβπ)βπ)(+gβπ)π)) = ((πΎ Β·
((invgβπ)βπ))(+gβπ)(πΎ Β· π))) |
27 | 6, 7, 8, 20, 9 | lmodvsinv2 20513 |
. . . . . . . . . 10
β’ ((π β LMod β§ πΎ β π β§ π β π΅) β (πΎ Β·
((invgβπ)βπ)) = ((invgβπ)β(πΎ Β· π))) |
28 | 15, 16, 19, 27 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π β π΅) β (πΎ Β·
((invgβπ)βπ)) = ((invgβπ)β(πΎ Β· π))) |
29 | 28 | oveq1d 7373 |
. . . . . . . 8
β’ (((π β§ π β π΅) β§ π β π΅) β ((πΎ Β·
((invgβπ)βπ))(+gβπ)(πΎ Β· π)) = (((invgβπ)β(πΎ Β· π))(+gβπ)(πΎ Β· π))) |
30 | 26, 29 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π β π΅) β§ π β π΅) β (πΎ Β·
(((invgβπ)βπ)(+gβπ)π)) = (((invgβπ)β(πΎ Β· π))(+gβπ)(πΎ Β· π))) |
31 | 30 | anasss 468 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅)) β (πΎ Β·
(((invgβπ)βπ)(+gβπ)π)) = (((invgβπ)β(πΎ Β· π))(+gβπ)(πΎ Β· π))) |
32 | 31 | 3adantr3 1172 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β (πΎ Β·
(((invgβπ)βπ)(+gβπ)π)) = (((invgβπ)β(πΎ Β· π))(+gβπ)(πΎ Β· π))) |
33 | | eqgvscpbl.g |
. . . . . . 7
β’ (π β πΊ β (LSubSpβπ)) |
34 | 33 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β πΊ β (LSubSpβπ)) |
35 | | simpr3 1197 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β (((invgβπ)βπ)(+gβπ)π) β πΊ) |
36 | | eqid 2733 |
. . . . . . 7
β’
(LSubSpβπ) =
(LSubSpβπ) |
37 | 7, 8, 9, 36 | lssvscl 20431 |
. . . . . 6
β’ (((π β LMod β§ πΊ β (LSubSpβπ)) β§ (πΎ β π β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β (πΎ Β·
(((invgβπ)βπ)(+gβπ)π)) β πΊ) |
38 | 2, 34, 4, 35, 37 | syl22anc 838 |
. . . . 5
β’ ((π β§ (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β (πΎ Β·
(((invgβπ)βπ)(+gβπ)π)) β πΊ) |
39 | 32, 38 | eqeltrrd 2835 |
. . . 4
β’ ((π β§ (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β (((invgβπ)β(πΎ Β· π))(+gβπ)(πΎ Β· π)) β πΊ) |
40 | 11, 14, 39 | 3jca 1129 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ)) β ((πΎ Β· π) β π΅ β§ (πΎ Β· π) β π΅ β§ (((invgβπ)β(πΎ Β· π))(+gβπ)(πΎ Β· π)) β πΊ)) |
41 | 40 | ex 414 |
. 2
β’ (π β ((π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ) β ((πΎ Β· π) β π΅ β§ (πΎ Β· π) β π΅ β§ (((invgβπ)β(πΎ Β· π))(+gβπ)(πΎ Β· π)) β πΊ))) |
42 | 1, 17 | syl 17 |
. . 3
β’ (π β π β Grp) |
43 | 36 | lsssubg 20433 |
. . . . 5
β’ ((π β LMod β§ πΊ β (LSubSpβπ)) β πΊ β (SubGrpβπ)) |
44 | 1, 33, 43 | syl2anc 585 |
. . . 4
β’ (π β πΊ β (SubGrpβπ)) |
45 | 6 | subgss 18934 |
. . . 4
β’ (πΊ β (SubGrpβπ) β πΊ β π΅) |
46 | 44, 45 | syl 17 |
. . 3
β’ (π β πΊ β π΅) |
47 | | eqgvscpbl.e |
. . . 4
β’ βΌ =
(π ~QG
πΊ) |
48 | 6, 20, 24, 47 | eqgval 18984 |
. . 3
β’ ((π β Grp β§ πΊ β π΅) β (π βΌ π β (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ))) |
49 | 42, 46, 48 | syl2anc 585 |
. 2
β’ (π β (π βΌ π β (π β π΅ β§ π β π΅ β§ (((invgβπ)βπ)(+gβπ)π) β πΊ))) |
50 | 6, 20, 24, 47 | eqgval 18984 |
. . 3
β’ ((π β Grp β§ πΊ β π΅) β ((πΎ Β· π) βΌ (πΎ Β· π) β ((πΎ Β· π) β π΅ β§ (πΎ Β· π) β π΅ β§ (((invgβπ)β(πΎ Β· π))(+gβπ)(πΎ Β· π)) β πΊ))) |
51 | 42, 46, 50 | syl2anc 585 |
. 2
β’ (π β ((πΎ Β· π) βΌ (πΎ Β· π) β ((πΎ Β· π) β π΅ β§ (πΎ Β· π) β π΅ β§ (((invgβπ)β(πΎ Β· π))(+gβπ)(πΎ Β· π)) β πΊ))) |
52 | 41, 49, 51 | 3imtr4d 294 |
1
β’ (π β (π βΌ π β (πΎ Β· π) βΌ (πΎ Β· π))) |