Step | Hyp | Ref
| Expression |
1 | | hilablo 29901 |
. . 3
β’
+β β AbelOp |
2 | | ablogrpo 29288 |
. . 3
β’ (
+β β AbelOp β +β β
GrpOp) |
3 | 1, 2 | ax-mp 5 |
. 2
β’
+β β GrpOp |
4 | | hhssabl.1 |
. . . 4
β’ π» β
Sβ |
5 | 4 | elexi 3463 |
. . 3
β’ π» β V |
6 | | eqid 2738 |
. . . . . . . 8
β’ ran
+β = ran +β |
7 | 6 | grpofo 29240 |
. . . . . . 7
β’ (
+β β GrpOp β +β :(ran
+β Γ ran +β )βontoβran +β ) |
8 | | fof 6752 |
. . . . . . 7
β’ (
+β :(ran +β Γ ran
+β )βontoβran
+β β +β :(ran +β
Γ ran +β )βΆran +β
) |
9 | 3, 7, 8 | mp2b 10 |
. . . . . 6
β’
+β :(ran +β Γ ran
+β )βΆran +β |
10 | 4 | shssii 29954 |
. . . . . . . 8
β’ π» β
β |
11 | | df-hba 29710 |
. . . . . . . . 9
β’ β
= (BaseSetββ¨β¨ +β ,
Β·β β©,
normββ©) |
12 | | eqid 2738 |
. . . . . . . . . 10
β’
β¨β¨ +β , Β·β
β©, normββ© = β¨β¨ +β ,
Β·β β©,
normββ© |
13 | 12 | hhva 29907 |
. . . . . . . . 9
β’
+β = ( +π£ ββ¨β¨
+β , Β·β β©,
normββ©) |
14 | 11, 13 | bafval 29345 |
. . . . . . . 8
β’ β
= ran +β |
15 | 10, 14 | sseqtri 3979 |
. . . . . . 7
β’ π» β ran
+β |
16 | | xpss12 5646 |
. . . . . . 7
β’ ((π» β ran
+β β§ π» β ran +β ) β
(π» Γ π») β (ran
+β Γ ran +β )) |
17 | 15, 15, 16 | mp2an 691 |
. . . . . 6
β’ (π» Γ π») β (ran +β Γ
ran +β ) |
18 | | fssres 6704 |
. . . . . 6
β’ ((
+β :(ran +β Γ ran
+β )βΆran +β β§ (π» Γ π») β (ran +β Γ
ran +β )) β ( +β βΎ (π» Γ π»)):(π» Γ π»)βΆran +β
) |
19 | 9, 17, 18 | mp2an 691 |
. . . . 5
β’ (
+β βΎ (π» Γ π»)):(π» Γ π»)βΆran
+β |
20 | | ffn 6664 |
. . . . 5
β’ ((
+β βΎ (π» Γ π»)):(π» Γ π»)βΆran +β β (
+β βΎ (π» Γ π»)) Fn (π» Γ π»)) |
21 | 19, 20 | ax-mp 5 |
. . . 4
β’ (
+β βΎ (π» Γ π»)) Fn (π» Γ π») |
22 | | ovres 7513 |
. . . . . 6
β’ ((π₯ β π» β§ π¦ β π») β (π₯( +β βΎ (π» Γ π»))π¦) = (π₯ +β π¦)) |
23 | | shaddcl 29958 |
. . . . . . 7
β’ ((π» β
Sβ β§ π₯ β π» β§ π¦ β π») β (π₯ +β π¦) β π») |
24 | 4, 23 | mp3an1 1449 |
. . . . . 6
β’ ((π₯ β π» β§ π¦ β π») β (π₯ +β π¦) β π») |
25 | 22, 24 | eqeltrd 2839 |
. . . . 5
β’ ((π₯ β π» β§ π¦ β π») β (π₯( +β βΎ (π» Γ π»))π¦) β π») |
26 | 25 | rgen2 3193 |
. . . 4
β’
βπ₯ β
π» βπ¦ β π» (π₯( +β βΎ (π» Γ π»))π¦) β π» |
27 | | ffnov 7476 |
. . . 4
β’ ((
+β βΎ (π» Γ π»)):(π» Γ π»)βΆπ» β (( +β βΎ
(π» Γ π»)) Fn (π» Γ π») β§ βπ₯ β π» βπ¦ β π» (π₯( +β βΎ (π» Γ π»))π¦) β π»)) |
28 | 21, 26, 27 | mpbir2an 710 |
. . 3
β’ (
+β βΎ (π» Γ π»)):(π» Γ π»)βΆπ» |
29 | 22 | oveq1d 7365 |
. . . . 5
β’ ((π₯ β π» β§ π¦ β π») β ((π₯( +β βΎ (π» Γ π»))π¦) +β π§) = ((π₯ +β π¦) +β π§)) |
30 | 29 | 3adant3 1133 |
. . . 4
β’ ((π₯ β π» β§ π¦ β π» β§ π§ β π») β ((π₯( +β βΎ (π» Γ π»))π¦) +β π§) = ((π₯ +β π¦) +β π§)) |
31 | | ovres 7513 |
. . . . 5
β’ (((π₯( +β βΎ
(π» Γ π»))π¦) β π» β§ π§ β π») β ((π₯( +β βΎ (π» Γ π»))π¦)( +β βΎ (π» Γ π»))π§) = ((π₯( +β βΎ (π» Γ π»))π¦) +β π§)) |
32 | 25, 31 | stoic3 1779 |
. . . 4
β’ ((π₯ β π» β§ π¦ β π» β§ π§ β π») β ((π₯( +β βΎ (π» Γ π»))π¦)( +β βΎ (π» Γ π»))π§) = ((π₯( +β βΎ (π» Γ π»))π¦) +β π§)) |
33 | | ovres 7513 |
. . . . . . 7
β’ ((π¦ β π» β§ π§ β π») β (π¦( +β βΎ (π» Γ π»))π§) = (π¦ +β π§)) |
34 | 33 | oveq2d 7366 |
. . . . . 6
β’ ((π¦ β π» β§ π§ β π») β (π₯ +β (π¦( +β βΎ (π» Γ π»))π§)) = (π₯ +β (π¦ +β π§))) |
35 | 34 | 3adant1 1131 |
. . . . 5
β’ ((π₯ β π» β§ π¦ β π» β§ π§ β π») β (π₯ +β (π¦( +β βΎ (π» Γ π»))π§)) = (π₯ +β (π¦ +β π§))) |
36 | 28 | fovcl 7477 |
. . . . . . 7
β’ ((π¦ β π» β§ π§ β π») β (π¦( +β βΎ (π» Γ π»))π§) β π») |
37 | | ovres 7513 |
. . . . . . 7
β’ ((π₯ β π» β§ (π¦( +β βΎ (π» Γ π»))π§) β π») β (π₯( +β βΎ (π» Γ π»))(π¦( +β βΎ (π» Γ π»))π§)) = (π₯ +β (π¦( +β βΎ (π» Γ π»))π§))) |
38 | 36, 37 | sylan2 594 |
. . . . . 6
β’ ((π₯ β π» β§ (π¦ β π» β§ π§ β π»)) β (π₯( +β βΎ (π» Γ π»))(π¦( +β βΎ (π» Γ π»))π§)) = (π₯ +β (π¦( +β βΎ (π» Γ π»))π§))) |
39 | 38 | 3impb 1116 |
. . . . 5
β’ ((π₯ β π» β§ π¦ β π» β§ π§ β π») β (π₯( +β βΎ (π» Γ π»))(π¦( +β βΎ (π» Γ π»))π§)) = (π₯ +β (π¦( +β βΎ (π» Γ π»))π§))) |
40 | 15 | sseli 3939 |
. . . . . 6
β’ (π₯ β π» β π₯ β ran +β
) |
41 | 15 | sseli 3939 |
. . . . . 6
β’ (π¦ β π» β π¦ β ran +β
) |
42 | 15 | sseli 3939 |
. . . . . 6
β’ (π§ β π» β π§ β ran +β
) |
43 | 6 | grpoass 29244 |
. . . . . . 7
β’ ((
+β β GrpOp β§ (π₯ β ran +β β§ π¦ β ran +β
β§ π§ β ran
+β )) β ((π₯ +β π¦) +β π§) = (π₯ +β (π¦ +β π§))) |
44 | 3, 43 | mpan 689 |
. . . . . 6
β’ ((π₯ β ran +β
β§ π¦ β ran
+β β§ π§ β ran +β ) β
((π₯ +β
π¦) +β
π§) = (π₯ +β (π¦ +β π§))) |
45 | 40, 41, 42, 44 | syl3an 1161 |
. . . . 5
β’ ((π₯ β π» β§ π¦ β π» β§ π§ β π») β ((π₯ +β π¦) +β π§) = (π₯ +β (π¦ +β π§))) |
46 | 35, 39, 45 | 3eqtr4d 2788 |
. . . 4
β’ ((π₯ β π» β§ π¦ β π» β§ π§ β π») β (π₯( +β βΎ (π» Γ π»))(π¦( +β βΎ (π» Γ π»))π§)) = ((π₯ +β π¦) +β π§)) |
47 | 30, 32, 46 | 3eqtr4d 2788 |
. . 3
β’ ((π₯ β π» β§ π¦ β π» β§ π§ β π») β ((π₯( +β βΎ (π» Γ π»))π¦)( +β βΎ (π» Γ π»))π§) = (π₯( +β βΎ (π» Γ π»))(π¦( +β βΎ (π» Γ π»))π§))) |
48 | | hilid 29902 |
. . . 4
β’
(GIdβ +β ) =
0β |
49 | | sh0 29957 |
. . . . 5
β’ (π» β
Sβ β 0β β π») |
50 | 4, 49 | ax-mp 5 |
. . . 4
β’
0β β π» |
51 | 48, 50 | eqeltri 2835 |
. . 3
β’
(GIdβ +β ) β π» |
52 | | ovres 7513 |
. . . . 5
β’
(((GIdβ +β ) β π» β§ π₯ β π») β ((GIdβ +β
)( +β βΎ (π» Γ π»))π₯) = ((GIdβ +β )
+β π₯)) |
53 | 51, 52 | mpan 689 |
. . . 4
β’ (π₯ β π» β ((GIdβ +β )(
+β βΎ (π» Γ π»))π₯) = ((GIdβ +β )
+β π₯)) |
54 | | eqid 2738 |
. . . . . 6
β’
(GIdβ +β ) = (GIdβ +β
) |
55 | 6, 54 | grpolid 29257 |
. . . . 5
β’ ((
+β β GrpOp β§ π₯ β ran +β ) β
((GIdβ +β ) +β π₯) = π₯) |
56 | 3, 40, 55 | sylancr 588 |
. . . 4
β’ (π₯ β π» β ((GIdβ +β )
+β π₯) =
π₯) |
57 | 53, 56 | eqtrd 2778 |
. . 3
β’ (π₯ β π» β ((GIdβ +β )(
+β βΎ (π» Γ π»))π₯) = π₯) |
58 | 12 | hhnv 29906 |
. . . . . . 7
β’
β¨β¨ +β , Β·β
β©, normββ© β NrmCVec |
59 | 12 | hhsm 29910 |
. . . . . . . 8
β’
Β·β = ( Β·π OLD
ββ¨β¨ +β , Β·β
β©, normββ©) |
60 | | eqid 2738 |
. . . . . . . 8
β’ (
Β·β β β‘(2nd βΎ ({-1} Γ V))) =
( Β·β β β‘(2nd βΎ ({-1} Γ
V))) |
61 | 13, 59, 60 | nvinvfval 29381 |
. . . . . . 7
β’
(β¨β¨ +β , Β·β
β©, normββ© β NrmCVec β (
Β·β β β‘(2nd βΎ ({-1} Γ V))) =
(invβ +β )) |
62 | 58, 61 | ax-mp 5 |
. . . . . 6
β’ (
Β·β β β‘(2nd βΎ ({-1} Γ V))) =
(invβ +β ) |
63 | 62 | eqcomi 2747 |
. . . . 5
β’
(invβ +β ) = (
Β·β β β‘(2nd βΎ ({-1} Γ
V))) |
64 | 63 | fveq1i 6839 |
. . . 4
β’
((invβ +β )βπ₯) = (( Β·β
β β‘(2nd βΎ ({-1}
Γ V)))βπ₯) |
65 | | ax-hfvmul 29746 |
. . . . . . 7
β’
Β·β :(β Γ β)βΆ
β |
66 | | ffn 6664 |
. . . . . . 7
β’ (
Β·β :(β Γ β)βΆ β
β Β·β Fn (β Γ
β)) |
67 | 65, 66 | ax-mp 5 |
. . . . . 6
β’
Β·β Fn (β Γ
β) |
68 | | neg1cn 12201 |
. . . . . 6
β’ -1 β
β |
69 | 60 | curry1val 8026 |
. . . . . 6
β’ ((
Β·β Fn (β Γ β) β§ -1 β
β) β (( Β·β β β‘(2nd βΎ ({-1} Γ
V)))βπ₯) = (-1
Β·β π₯)) |
70 | 67, 68, 69 | mp2an 691 |
. . . . 5
β’ ((
Β·β β β‘(2nd βΎ ({-1} Γ
V)))βπ₯) = (-1
Β·β π₯) |
71 | | shmulcl 29959 |
. . . . . 6
β’ ((π» β
Sβ β§ -1 β β β§ π₯ β π») β (-1
Β·β π₯) β π») |
72 | 4, 68, 71 | mp3an12 1452 |
. . . . 5
β’ (π₯ β π» β (-1
Β·β π₯) β π») |
73 | 70, 72 | eqeltrid 2843 |
. . . 4
β’ (π₯ β π» β ((
Β·β β β‘(2nd βΎ ({-1} Γ
V)))βπ₯) β π») |
74 | 64, 73 | eqeltrid 2843 |
. . 3
β’ (π₯ β π» β ((invβ +β
)βπ₯) β π») |
75 | | ovres 7513 |
. . . . 5
β’
((((invβ +β )βπ₯) β π» β§ π₯ β π») β (((invβ +β
)βπ₯)(
+β βΎ (π» Γ π»))π₯) = (((invβ +β
)βπ₯)
+β π₯)) |
76 | 74, 75 | mpancom 687 |
. . . 4
β’ (π₯ β π» β (((invβ +β
)βπ₯)(
+β βΎ (π» Γ π»))π₯) = (((invβ +β
)βπ₯)
+β π₯)) |
77 | | eqid 2738 |
. . . . . 6
β’
(invβ +β ) = (invβ +β
) |
78 | 6, 54, 77 | grpolinv 29267 |
. . . . 5
β’ ((
+β β GrpOp β§ π₯ β ran +β ) β
(((invβ +β )βπ₯) +β π₯) = (GIdβ +β
)) |
79 | 3, 40, 78 | sylancr 588 |
. . . 4
β’ (π₯ β π» β (((invβ +β
)βπ₯)
+β π₯) =
(GIdβ +β )) |
80 | 76, 79 | eqtrd 2778 |
. . 3
β’ (π₯ β π» β (((invβ +β
)βπ₯)(
+β βΎ (π» Γ π»))π₯) = (GIdβ +β
)) |
81 | 5, 28, 47, 51, 57, 74, 80 | isgrpoi 29239 |
. 2
β’ (
+β βΎ (π» Γ π»)) β GrpOp |
82 | | resss 5959 |
. 2
β’ (
+β βΎ (π» Γ π»)) β
+β |
83 | 3, 81, 82 | 3pm3.2i 1340 |
1
β’ (
+β β GrpOp β§ ( +β βΎ (π» Γ π»)) β GrpOp β§ ( +β
βΎ (π» Γ π»)) β +β
) |