Step | Hyp | Ref
| Expression |
1 | | nmotri.1 |
. 2
β’ π = (π normOp π) |
2 | | eqid 2726 |
. 2
β’
(Baseβπ) =
(Baseβπ) |
3 | | eqid 2726 |
. 2
β’
(normβπ) =
(normβπ) |
4 | | eqid 2726 |
. 2
β’
(normβπ) =
(normβπ) |
5 | | eqid 2726 |
. 2
β’
(0gβπ) = (0gβπ) |
6 | | nghmrcl1 24600 |
. . 3
β’ (πΉ β (π NGHom π) β π β NrmGrp) |
7 | 6 | 3ad2ant2 1131 |
. 2
β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β π β NrmGrp) |
8 | | nghmrcl2 24601 |
. . 3
β’ (πΉ β (π NGHom π) β π β NrmGrp) |
9 | 8 | 3ad2ant2 1131 |
. 2
β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β π β NrmGrp) |
10 | | id 22 |
. . 3
β’ (π β Abel β π β Abel) |
11 | | nghmghm 24602 |
. . 3
β’ (πΉ β (π NGHom π) β πΉ β (π GrpHom π)) |
12 | | nghmghm 24602 |
. . 3
β’ (πΊ β (π NGHom π) β πΊ β (π GrpHom π)) |
13 | | nmotri.p |
. . . 4
β’ + =
(+gβπ) |
14 | 13 | ghmplusg 19764 |
. . 3
β’ ((π β Abel β§ πΉ β (π GrpHom π) β§ πΊ β (π GrpHom π)) β (πΉ βf + πΊ) β (π GrpHom π)) |
15 | 10, 11, 12, 14 | syl3an 1157 |
. 2
β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β (πΉ βf + πΊ) β (π GrpHom π)) |
16 | 1 | nghmcl 24595 |
. . . 4
β’ (πΉ β (π NGHom π) β (πβπΉ) β β) |
17 | 16 | 3ad2ant2 1131 |
. . 3
β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β (πβπΉ) β β) |
18 | 1 | nghmcl 24595 |
. . . 4
β’ (πΊ β (π NGHom π) β (πβπΊ) β β) |
19 | 18 | 3ad2ant3 1132 |
. . 3
β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β (πβπΊ) β β) |
20 | 17, 19 | readdcld 11244 |
. 2
β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β ((πβπΉ) + (πβπΊ)) β β) |
21 | 11 | 3ad2ant2 1131 |
. . . 4
β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β πΉ β (π GrpHom π)) |
22 | 1 | nmoge0 24589 |
. . . 4
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β 0 β€ (πβπΉ)) |
23 | 7, 9, 21, 22 | syl3anc 1368 |
. . 3
β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β 0 β€ (πβπΉ)) |
24 | 12 | 3ad2ant3 1132 |
. . . 4
β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β πΊ β (π GrpHom π)) |
25 | 1 | nmoge0 24589 |
. . . 4
β’ ((π β NrmGrp β§ π β NrmGrp β§ πΊ β (π GrpHom π)) β 0 β€ (πβπΊ)) |
26 | 7, 9, 24, 25 | syl3anc 1368 |
. . 3
β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β 0 β€ (πβπΊ)) |
27 | 17, 19, 23, 26 | addge0d 11791 |
. 2
β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β 0 β€ ((πβπΉ) + (πβπΊ))) |
28 | 9 | adantr 480 |
. . . . 5
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β π β NrmGrp) |
29 | | ngpgrp 24459 |
. . . . . . 7
β’ (π β NrmGrp β π β Grp) |
30 | 28, 29 | syl 17 |
. . . . . 6
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β π β Grp) |
31 | 21 | adantr 480 |
. . . . . . . 8
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β πΉ β (π GrpHom π)) |
32 | | eqid 2726 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
33 | 2, 32 | ghmf 19143 |
. . . . . . . 8
β’ (πΉ β (π GrpHom π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
34 | 31, 33 | syl 17 |
. . . . . . 7
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
35 | | simprl 768 |
. . . . . . 7
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β π₯ β (Baseβπ)) |
36 | 34, 35 | ffvelcdmd 7080 |
. . . . . 6
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β (πΉβπ₯) β (Baseβπ)) |
37 | 24 | adantr 480 |
. . . . . . . 8
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β πΊ β (π GrpHom π)) |
38 | 2, 32 | ghmf 19143 |
. . . . . . . 8
β’ (πΊ β (π GrpHom π) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
39 | 37, 38 | syl 17 |
. . . . . . 7
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
40 | 39, 35 | ffvelcdmd 7080 |
. . . . . 6
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β (πΊβπ₯) β (Baseβπ)) |
41 | 32, 13 | grpcl 18869 |
. . . . . 6
β’ ((π β Grp β§ (πΉβπ₯) β (Baseβπ) β§ (πΊβπ₯) β (Baseβπ)) β ((πΉβπ₯) + (πΊβπ₯)) β (Baseβπ)) |
42 | 30, 36, 40, 41 | syl3anc 1368 |
. . . . 5
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((πΉβπ₯) + (πΊβπ₯)) β (Baseβπ)) |
43 | 32, 4 | nmcl 24476 |
. . . . 5
β’ ((π β NrmGrp β§ ((πΉβπ₯) + (πΊβπ₯)) β (Baseβπ)) β ((normβπ)β((πΉβπ₯) + (πΊβπ₯))) β β) |
44 | 28, 42, 43 | syl2anc 583 |
. . . 4
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((normβπ)β((πΉβπ₯) + (πΊβπ₯))) β β) |
45 | 32, 4 | nmcl 24476 |
. . . . . 6
β’ ((π β NrmGrp β§ (πΉβπ₯) β (Baseβπ)) β ((normβπ)β(πΉβπ₯)) β β) |
46 | 28, 36, 45 | syl2anc 583 |
. . . . 5
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((normβπ)β(πΉβπ₯)) β β) |
47 | 32, 4 | nmcl 24476 |
. . . . . 6
β’ ((π β NrmGrp β§ (πΊβπ₯) β (Baseβπ)) β ((normβπ)β(πΊβπ₯)) β β) |
48 | 28, 40, 47 | syl2anc 583 |
. . . . 5
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((normβπ)β(πΊβπ₯)) β β) |
49 | 46, 48 | readdcld 11244 |
. . . 4
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β (((normβπ)β(πΉβπ₯)) + ((normβπ)β(πΊβπ₯))) β β) |
50 | 17 | adantr 480 |
. . . . . 6
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β (πβπΉ) β β) |
51 | | simpl 482 |
. . . . . . 7
β’ ((π₯ β (Baseβπ) β§ π₯ β (0gβπ)) β π₯ β (Baseβπ)) |
52 | 2, 3 | nmcl 24476 |
. . . . . . 7
β’ ((π β NrmGrp β§ π₯ β (Baseβπ)) β ((normβπ)βπ₯) β β) |
53 | 7, 51, 52 | syl2an 595 |
. . . . . 6
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((normβπ)βπ₯) β β) |
54 | 50, 53 | remulcld 11245 |
. . . . 5
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((πβπΉ) Β· ((normβπ)βπ₯)) β β) |
55 | 19 | adantr 480 |
. . . . . 6
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β (πβπΊ) β β) |
56 | 55, 53 | remulcld 11245 |
. . . . 5
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((πβπΊ) Β· ((normβπ)βπ₯)) β β) |
57 | 54, 56 | readdcld 11244 |
. . . 4
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β (((πβπΉ) Β· ((normβπ)βπ₯)) + ((πβπΊ) Β· ((normβπ)βπ₯))) β β) |
58 | 32, 4, 13 | nmtri 24486 |
. . . . 5
β’ ((π β NrmGrp β§ (πΉβπ₯) β (Baseβπ) β§ (πΊβπ₯) β (Baseβπ)) β ((normβπ)β((πΉβπ₯) + (πΊβπ₯))) β€ (((normβπ)β(πΉβπ₯)) + ((normβπ)β(πΊβπ₯)))) |
59 | 28, 36, 40, 58 | syl3anc 1368 |
. . . 4
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((normβπ)β((πΉβπ₯) + (πΊβπ₯))) β€ (((normβπ)β(πΉβπ₯)) + ((normβπ)β(πΊβπ₯)))) |
60 | | simpl2 1189 |
. . . . . 6
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β πΉ β (π NGHom π)) |
61 | 1, 2, 3, 4 | nmoi 24596 |
. . . . . 6
β’ ((πΉ β (π NGHom π) β§ π₯ β (Baseβπ)) β ((normβπ)β(πΉβπ₯)) β€ ((πβπΉ) Β· ((normβπ)βπ₯))) |
62 | 60, 35, 61 | syl2anc 583 |
. . . . 5
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((normβπ)β(πΉβπ₯)) β€ ((πβπΉ) Β· ((normβπ)βπ₯))) |
63 | | simpl3 1190 |
. . . . . 6
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β πΊ β (π NGHom π)) |
64 | 1, 2, 3, 4 | nmoi 24596 |
. . . . . 6
β’ ((πΊ β (π NGHom π) β§ π₯ β (Baseβπ)) β ((normβπ)β(πΊβπ₯)) β€ ((πβπΊ) Β· ((normβπ)βπ₯))) |
65 | 63, 35, 64 | syl2anc 583 |
. . . . 5
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((normβπ)β(πΊβπ₯)) β€ ((πβπΊ) Β· ((normβπ)βπ₯))) |
66 | 46, 48, 54, 56, 62, 65 | le2addd 11834 |
. . . 4
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β (((normβπ)β(πΉβπ₯)) + ((normβπ)β(πΊβπ₯))) β€ (((πβπΉ) Β· ((normβπ)βπ₯)) + ((πβπΊ) Β· ((normβπ)βπ₯)))) |
67 | 44, 49, 57, 59, 66 | letrd 11372 |
. . 3
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((normβπ)β((πΉβπ₯) + (πΊβπ₯))) β€ (((πβπΉ) Β· ((normβπ)βπ₯)) + ((πβπΊ) Β· ((normβπ)βπ₯)))) |
68 | 34 | ffnd 6711 |
. . . . 5
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β πΉ Fn (Baseβπ)) |
69 | 39 | ffnd 6711 |
. . . . 5
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β πΊ Fn (Baseβπ)) |
70 | | fvexd 6899 |
. . . . 5
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β (Baseβπ) β V) |
71 | | fnfvof 7683 |
. . . . 5
β’ (((πΉ Fn (Baseβπ) β§ πΊ Fn (Baseβπ)) β§ ((Baseβπ) β V β§ π₯ β (Baseβπ))) β ((πΉ βf + πΊ)βπ₯) = ((πΉβπ₯) + (πΊβπ₯))) |
72 | 68, 69, 70, 35, 71 | syl22anc 836 |
. . . 4
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((πΉ βf + πΊ)βπ₯) = ((πΉβπ₯) + (πΊβπ₯))) |
73 | 72 | fveq2d 6888 |
. . 3
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((normβπ)β((πΉ βf + πΊ)βπ₯)) = ((normβπ)β((πΉβπ₯) + (πΊβπ₯)))) |
74 | 50 | recnd 11243 |
. . . 4
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β (πβπΉ) β β) |
75 | 55 | recnd 11243 |
. . . 4
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β (πβπΊ) β β) |
76 | 53 | recnd 11243 |
. . . 4
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((normβπ)βπ₯) β β) |
77 | 74, 75, 76 | adddird 11240 |
. . 3
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β (((πβπΉ) + (πβπΊ)) Β· ((normβπ)βπ₯)) = (((πβπΉ) Β· ((normβπ)βπ₯)) + ((πβπΊ) Β· ((normβπ)βπ₯)))) |
78 | 67, 73, 77 | 3brtr4d 5173 |
. 2
β’ (((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β§ (π₯ β (Baseβπ) β§ π₯ β (0gβπ))) β ((normβπ)β((πΉ βf + πΊ)βπ₯)) β€ (((πβπΉ) + (πβπΊ)) Β· ((normβπ)βπ₯))) |
79 | 1, 2, 3, 4, 5, 7, 9, 15, 20, 27, 78 | nmolb2d 24586 |
1
β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β (πβ(πΉ βf + πΊ)) β€ ((πβπΉ) + (πβπΊ))) |