Step | Hyp | Ref
| Expression |
1 | | ngpgrp 23978 |
. . 3
β’ (πΊ β NrmGrp β πΊ β Grp) |
2 | | ngpms 23979 |
. . 3
β’ (πΊ β NrmGrp β πΊ β MetSp) |
3 | | ngprcan.x |
. . . . 5
β’ π = (BaseβπΊ) |
4 | | ngprcan.p |
. . . . 5
β’ + =
(+gβπΊ) |
5 | | ngprcan.d |
. . . . 5
β’ π· = (distβπΊ) |
6 | 3, 4, 5 | ngprcan 23989 |
. . . 4
β’ ((πΊ β NrmGrp β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦)) |
7 | 6 | ralrimivvva 3197 |
. . 3
β’ (πΊ β NrmGrp β
βπ₯ β π βπ¦ β π βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦)) |
8 | 1, 2, 7 | 3jca 1129 |
. 2
β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§
βπ₯ β π βπ¦ β π βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦))) |
9 | | simp1 1137 |
. . 3
β’ ((πΊ β Grp β§ πΊ β MetSp β§
βπ₯ β π βπ¦ β π βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦)) β πΊ β Grp) |
10 | | simp2 1138 |
. . 3
β’ ((πΊ β Grp β§ πΊ β MetSp β§
βπ₯ β π βπ¦ β π βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦)) β πΊ β MetSp) |
11 | | eqid 2733 |
. . . . . . . . 9
β’
(invgβπΊ) = (invgβπΊ) |
12 | 3, 11 | grpinvcl 18806 |
. . . . . . . 8
β’ ((πΊ β Grp β§ π¦ β π) β ((invgβπΊ)βπ¦) β π) |
13 | 12 | ad2ant2rl 748 |
. . . . . . 7
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β ((invgβπΊ)βπ¦) β π) |
14 | | eqcom 2740 |
. . . . . . . . 9
β’ (((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦) β (π₯π·π¦) = ((π₯ + π§)π·(π¦ + π§))) |
15 | | oveq2 7369 |
. . . . . . . . . . 11
β’ (π§ = ((invgβπΊ)βπ¦) β (π₯ + π§) = (π₯ +
((invgβπΊ)βπ¦))) |
16 | | oveq2 7369 |
. . . . . . . . . . 11
β’ (π§ = ((invgβπΊ)βπ¦) β (π¦ + π§) = (π¦ +
((invgβπΊ)βπ¦))) |
17 | 15, 16 | oveq12d 7379 |
. . . . . . . . . 10
β’ (π§ = ((invgβπΊ)βπ¦) β ((π₯ + π§)π·(π¦ + π§)) = ((π₯ +
((invgβπΊ)βπ¦))π·(π¦ +
((invgβπΊ)βπ¦)))) |
18 | 17 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π§ = ((invgβπΊ)βπ¦) β ((π₯π·π¦) = ((π₯ + π§)π·(π¦ + π§)) β (π₯π·π¦) = ((π₯ +
((invgβπΊ)βπ¦))π·(π¦ +
((invgβπΊ)βπ¦))))) |
19 | 14, 18 | bitrid 283 |
. . . . . . . 8
β’ (π§ = ((invgβπΊ)βπ¦) β (((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦) β (π₯π·π¦) = ((π₯ +
((invgβπΊ)βπ¦))π·(π¦ +
((invgβπΊ)βπ¦))))) |
20 | 19 | rspcv 3579 |
. . . . . . 7
β’
(((invgβπΊ)βπ¦) β π β (βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦) β (π₯π·π¦) = ((π₯ +
((invgβπΊ)βπ¦))π·(π¦ +
((invgβπΊ)βπ¦))))) |
21 | 13, 20 | syl 17 |
. . . . . 6
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β (βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦) β (π₯π·π¦) = ((π₯ +
((invgβπΊ)βπ¦))π·(π¦ +
((invgβπΊ)βπ¦))))) |
22 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(-gβπΊ) = (-gβπΊ) |
23 | 3, 4, 11, 22 | grpsubval 18804 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ π¦ β π) β (π₯(-gβπΊ)π¦) = (π₯ +
((invgβπΊ)βπ¦))) |
24 | 23 | adantl 483 |
. . . . . . . . . 10
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β (π₯(-gβπΊ)π¦) = (π₯ +
((invgβπΊ)βπ¦))) |
25 | 24 | eqcomd 2739 |
. . . . . . . . 9
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β (π₯ +
((invgβπΊ)βπ¦)) = (π₯(-gβπΊ)π¦)) |
26 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0gβπΊ) = (0gβπΊ) |
27 | 3, 4, 26, 11 | grprinv 18809 |
. . . . . . . . . 10
β’ ((πΊ β Grp β§ π¦ β π) β (π¦ +
((invgβπΊ)βπ¦)) = (0gβπΊ)) |
28 | 27 | ad2ant2rl 748 |
. . . . . . . . 9
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β (π¦ +
((invgβπΊ)βπ¦)) = (0gβπΊ)) |
29 | 25, 28 | oveq12d 7379 |
. . . . . . . 8
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β ((π₯ +
((invgβπΊ)βπ¦))π·(π¦ +
((invgβπΊ)βπ¦))) = ((π₯(-gβπΊ)π¦)π·(0gβπΊ))) |
30 | 3, 22 | grpsubcl 18835 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ π₯ β π β§ π¦ β π) β (π₯(-gβπΊ)π¦) β π) |
31 | 30 | 3expb 1121 |
. . . . . . . . . 10
β’ ((πΊ β Grp β§ (π₯ β π β§ π¦ β π)) β (π₯(-gβπΊ)π¦) β π) |
32 | 31 | adantlr 714 |
. . . . . . . . 9
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β (π₯(-gβπΊ)π¦) β π) |
33 | | eqid 2733 |
. . . . . . . . . 10
β’
(normβπΊ) =
(normβπΊ) |
34 | 33, 3, 26, 5 | nmval 23968 |
. . . . . . . . 9
β’ ((π₯(-gβπΊ)π¦) β π β ((normβπΊ)β(π₯(-gβπΊ)π¦)) = ((π₯(-gβπΊ)π¦)π·(0gβπΊ))) |
35 | 32, 34 | syl 17 |
. . . . . . . 8
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β ((normβπΊ)β(π₯(-gβπΊ)π¦)) = ((π₯(-gβπΊ)π¦)π·(0gβπΊ))) |
36 | 29, 35 | eqtr4d 2776 |
. . . . . . 7
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β ((π₯ +
((invgβπΊ)βπ¦))π·(π¦ +
((invgβπΊ)βπ¦))) = ((normβπΊ)β(π₯(-gβπΊ)π¦))) |
37 | 36 | eqeq2d 2744 |
. . . . . 6
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) = ((π₯ +
((invgβπΊ)βπ¦))π·(π¦ +
((invgβπΊ)βπ¦))) β (π₯π·π¦) = ((normβπΊ)β(π₯(-gβπΊ)π¦)))) |
38 | 21, 37 | sylibd 238 |
. . . . 5
β’ (((πΊ β Grp β§ πΊ β MetSp) β§ (π₯ β π β§ π¦ β π)) β (βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦) β (π₯π·π¦) = ((normβπΊ)β(π₯(-gβπΊ)π¦)))) |
39 | 38 | ralimdvva 3198 |
. . . 4
β’ ((πΊ β Grp β§ πΊ β MetSp) β
(βπ₯ β π βπ¦ β π βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦) β βπ₯ β π βπ¦ β π (π₯π·π¦) = ((normβπΊ)β(π₯(-gβπΊ)π¦)))) |
40 | 39 | 3impia 1118 |
. . 3
β’ ((πΊ β Grp β§ πΊ β MetSp β§
βπ₯ β π βπ¦ β π βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦)) β βπ₯ β π βπ¦ β π (π₯π·π¦) = ((normβπΊ)β(π₯(-gβπΊ)π¦))) |
41 | 33, 22, 5, 3 | isngp3 23977 |
. . 3
β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§
βπ₯ β π βπ¦ β π (π₯π·π¦) = ((normβπΊ)β(π₯(-gβπΊ)π¦)))) |
42 | 9, 10, 40, 41 | syl3anbrc 1344 |
. 2
β’ ((πΊ β Grp β§ πΊ β MetSp β§
βπ₯ β π βπ¦ β π βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦)) β πΊ β NrmGrp) |
43 | 8, 42 | impbii 208 |
1
β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§
βπ₯ β π βπ¦ β π βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦))) |