Step | Hyp | Ref
| Expression |
1 | | df-nsg 12962 |
. . 3
β’ NrmSGrp =
(π β Grp β¦
{π β
(SubGrpβπ) β£
[(Baseβπ) /
π][(+gβπ) / π]βπ₯ β π βπ¦ β π ((π₯ππ¦) β π β (π¦ππ₯) β π )}) |
2 | 1 | mptrcl 5597 |
. 2
β’ (π β (NrmSGrpβπΊ) β πΊ β Grp) |
3 | | subgrcl 12970 |
. . 3
β’ (π β (SubGrpβπΊ) β πΊ β Grp) |
4 | 3 | adantr 276 |
. 2
β’ ((π β (SubGrpβπΊ) β§ βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π)) β πΊ β Grp) |
5 | | fveq2 5514 |
. . . . . 6
β’ (π = πΊ β (SubGrpβπ) = (SubGrpβπΊ)) |
6 | | basfn 12512 |
. . . . . . . . . 10
β’ Base Fn
V |
7 | | funfvex 5531 |
. . . . . . . . . . 11
β’ ((Fun
Base β§ π β dom
Base) β (Baseβπ)
β V) |
8 | 7 | funfni 5315 |
. . . . . . . . . 10
β’ ((Base Fn
V β§ π β V) β
(Baseβπ) β
V) |
9 | 6, 8 | mpan 424 |
. . . . . . . . 9
β’ (π β V β
(Baseβπ) β
V) |
10 | 9 | elv 2741 |
. . . . . . . 8
β’
(Baseβπ)
β V |
11 | 10 | a1i 9 |
. . . . . . 7
β’ (π = πΊ β (Baseβπ) β V) |
12 | | fveq2 5514 |
. . . . . . . 8
β’ (π = πΊ β (Baseβπ) = (BaseβπΊ)) |
13 | | isnsg.1 |
. . . . . . . 8
β’ π = (BaseβπΊ) |
14 | 12, 13 | eqtr4di 2228 |
. . . . . . 7
β’ (π = πΊ β (Baseβπ) = π) |
15 | | plusgslid 12563 |
. . . . . . . . . . 11
β’
(+g = Slot (+gβndx) β§
(+gβndx) β β) |
16 | 15 | slotex 12481 |
. . . . . . . . . 10
β’ (π β V β
(+gβπ)
β V) |
17 | 16 | elv 2741 |
. . . . . . . . 9
β’
(+gβπ) β V |
18 | 17 | a1i 9 |
. . . . . . . 8
β’ ((π = πΊ β§ π = π) β (+gβπ) β V) |
19 | | simpl 109 |
. . . . . . . . . 10
β’ ((π = πΊ β§ π = π) β π = πΊ) |
20 | 19 | fveq2d 5518 |
. . . . . . . . 9
β’ ((π = πΊ β§ π = π) β (+gβπ) = (+gβπΊ)) |
21 | | isnsg.2 |
. . . . . . . . 9
β’ + =
(+gβπΊ) |
22 | 20, 21 | eqtr4di 2228 |
. . . . . . . 8
β’ ((π = πΊ β§ π = π) β (+gβπ) = + ) |
23 | | simplr 528 |
. . . . . . . . 9
β’ (((π = πΊ β§ π = π) β§ π = + ) β π = π) |
24 | | simpr 110 |
. . . . . . . . . . . . 13
β’ (((π = πΊ β§ π = π) β§ π = + ) β π = + ) |
25 | 24 | oveqd 5889 |
. . . . . . . . . . . 12
β’ (((π = πΊ β§ π = π) β§ π = + ) β (π₯ππ¦) = (π₯ + π¦)) |
26 | 25 | eleq1d 2246 |
. . . . . . . . . . 11
β’ (((π = πΊ β§ π = π) β§ π = + ) β ((π₯ππ¦) β π β (π₯ + π¦) β π )) |
27 | 24 | oveqd 5889 |
. . . . . . . . . . . 12
β’ (((π = πΊ β§ π = π) β§ π = + ) β (π¦ππ₯) = (π¦ + π₯)) |
28 | 27 | eleq1d 2246 |
. . . . . . . . . . 11
β’ (((π = πΊ β§ π = π) β§ π = + ) β ((π¦ππ₯) β π β (π¦ + π₯) β π )) |
29 | 26, 28 | bibi12d 235 |
. . . . . . . . . 10
β’ (((π = πΊ β§ π = π) β§ π = + ) β (((π₯ππ¦) β π β (π¦ππ₯) β π ) β ((π₯ + π¦) β π β (π¦ + π₯) β π ))) |
30 | 23, 29 | raleqbidv 2684 |
. . . . . . . . 9
β’ (((π = πΊ β§ π = π) β§ π = + ) β (βπ¦ β π ((π₯ππ¦) β π β (π¦ππ₯) β π ) β βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π ))) |
31 | 23, 30 | raleqbidv 2684 |
. . . . . . . 8
β’ (((π = πΊ β§ π = π) β§ π = + ) β (βπ₯ β π βπ¦ β π ((π₯ππ¦) β π β (π¦ππ₯) β π ) β βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π ))) |
32 | 18, 22, 31 | sbcied2 3000 |
. . . . . . 7
β’ ((π = πΊ β§ π = π) β ([(+gβπ) / π]βπ₯ β π βπ¦ β π ((π₯ππ¦) β π β (π¦ππ₯) β π ) β βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π ))) |
33 | 11, 14, 32 | sbcied2 3000 |
. . . . . 6
β’ (π = πΊ β ([(Baseβπ) / π][(+gβπ) / π]βπ₯ β π βπ¦ β π ((π₯ππ¦) β π β (π¦ππ₯) β π ) β βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π ))) |
34 | 5, 33 | rabeqbidv 2732 |
. . . . 5
β’ (π = πΊ β {π β (SubGrpβπ) β£ [(Baseβπ) / π][(+gβπ) / π]βπ₯ β π βπ¦ β π ((π₯ππ¦) β π β (π¦ππ₯) β π )} = {π β (SubGrpβπΊ) β£ βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π )}) |
35 | | id 19 |
. . . . 5
β’ (πΊ β Grp β πΊ β Grp) |
36 | | subgex 12967 |
. . . . . 6
β’ (πΊ β Grp β
(SubGrpβπΊ) β
V) |
37 | | rabexg 4145 |
. . . . . 6
β’
((SubGrpβπΊ)
β V β {π β
(SubGrpβπΊ) β£
βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π )} β V) |
38 | 36, 37 | syl 14 |
. . . . 5
β’ (πΊ β Grp β {π β (SubGrpβπΊ) β£ βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π )} β V) |
39 | 1, 34, 35, 38 | fvmptd3 5608 |
. . . 4
β’ (πΊ β Grp β
(NrmSGrpβπΊ) = {π β (SubGrpβπΊ) β£ βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π )}) |
40 | 39 | eleq2d 2247 |
. . 3
β’ (πΊ β Grp β (π β (NrmSGrpβπΊ) β π β {π β (SubGrpβπΊ) β£ βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π )})) |
41 | | eleq2 2241 |
. . . . . 6
β’ (π = π β ((π₯ + π¦) β π β (π₯ + π¦) β π)) |
42 | | eleq2 2241 |
. . . . . 6
β’ (π = π β ((π¦ + π₯) β π β (π¦ + π₯) β π)) |
43 | 41, 42 | bibi12d 235 |
. . . . 5
β’ (π = π β (((π₯ + π¦) β π β (π¦ + π₯) β π ) β ((π₯ + π¦) β π β (π¦ + π₯) β π))) |
44 | 43 | 2ralbidv 2501 |
. . . 4
β’ (π = π β (βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π ) β βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π))) |
45 | 44 | elrab 2893 |
. . 3
β’ (π β {π β (SubGrpβπΊ) β£ βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π )} β (π β (SubGrpβπΊ) β§ βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π))) |
46 | 40, 45 | bitrdi 196 |
. 2
β’ (πΊ β Grp β (π β (NrmSGrpβπΊ) β (π β (SubGrpβπΊ) β§ βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π)))) |
47 | 2, 4, 46 | pm5.21nii 704 |
1
β’ (π β (NrmSGrpβπΊ) β (π β (SubGrpβπΊ) β§ βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π))) |