Step | Hyp | Ref
| Expression |
1 | | elin 3931 |
. . 3
β’ (πΊ β (Grp β© MetSp) β
(πΊ β Grp β§ πΊ β MetSp)) |
2 | 1 | anbi1i 625 |
. 2
β’ ((πΊ β (Grp β© MetSp) β§
(π β β )
β π·) β ((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·)) |
3 | | fveq2 6847 |
. . . . . 6
β’ (π = πΊ β (normβπ) = (normβπΊ)) |
4 | | isngp.n |
. . . . . 6
β’ π = (normβπΊ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . 5
β’ (π = πΊ β (normβπ) = π) |
6 | | fveq2 6847 |
. . . . . 6
β’ (π = πΊ β (-gβπ) = (-gβπΊ)) |
7 | | isngp.z |
. . . . . 6
β’ β =
(-gβπΊ) |
8 | 6, 7 | eqtr4di 2795 |
. . . . 5
β’ (π = πΊ β (-gβπ) = β ) |
9 | 5, 8 | coeq12d 5825 |
. . . 4
β’ (π = πΊ β ((normβπ) β (-gβπ)) = (π β β )) |
10 | | fveq2 6847 |
. . . . 5
β’ (π = πΊ β (distβπ) = (distβπΊ)) |
11 | | isngp.d |
. . . . 5
β’ π· = (distβπΊ) |
12 | 10, 11 | eqtr4di 2795 |
. . . 4
β’ (π = πΊ β (distβπ) = π·) |
13 | 9, 12 | sseq12d 3982 |
. . 3
β’ (π = πΊ β (((normβπ) β (-gβπ)) β (distβπ) β (π β β ) β π·)) |
14 | | df-ngp 23955 |
. . 3
β’ NrmGrp =
{π β (Grp β© MetSp)
β£ ((normβπ)
β (-gβπ)) β (distβπ)} |
15 | 13, 14 | elrab2 3653 |
. 2
β’ (πΊ β NrmGrp β (πΊ β (Grp β© MetSp) β§
(π β β )
β π·)) |
16 | | df-3an 1090 |
. 2
β’ ((πΊ β Grp β§ πΊ β MetSp β§ (π β β ) β π·) β ((πΊ β Grp β§ πΊ β MetSp) β§ (π β β ) β π·)) |
17 | 2, 15, 16 | 3bitr4i 303 |
1
β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ (π β β ) β π·)) |