Step | Hyp | Ref
| Expression |
1 | | hhssnv.2 |
. . . . 5
|
2 | 1 | hhssabloi 28119 |
. . . 4
|
3 | | ablogrpo 27401 |
. . . 4
|
4 | 2, 3 | ax-mp 5 |
. . 3
|
5 | 1 | shssii 28070 |
. . . . . 6
|
6 | | xpss12 5225 |
. . . . . 6
|
7 | 5, 5, 6 | mp2an 708 |
. . . . 5
|
8 | | ax-hfvadd 27857 |
. . . . . 6
|
9 | 8 | fdmi 6052 |
. . . . 5
|
10 | 7, 9 | sseqtr4i 3638 |
. . . 4
|
11 | | ssdmres 5420 |
. . . 4
|
12 | 10, 11 | mpbi 220 |
. . 3
|
13 | 4, 12 | grporn 27375 |
. 2
|
14 | | sh0 28073 |
. . . . . 6
|
15 | 1, 14 | ax-mp 5 |
. . . . 5
|
16 | | ovres 6800 |
. . . . 5
|
17 | 15, 15, 16 | mp2an 708 |
. . . 4
|
18 | | ax-hv0cl 27860 |
. . . . 5
|
19 | 18 | hvaddid2i 27886 |
. . . 4
|
20 | 17, 19 | eqtri 2644 |
. . 3
|
21 | | eqid 2622 |
. . . . 5
GId
GId |
22 | 13, 21 | grpoid 27374 |
. . . 4
GId |
23 | 4, 15, 22 | mp2an 708 |
. . 3
GId |
24 | 20, 23 | mpbir 221 |
. 2
GId |
25 | | ax-hfvmul 27862 |
. . . . . 6
|
26 | | ffn 6045 |
. . . . . 6
|
27 | 25, 26 | ax-mp 5 |
. . . . 5
|
28 | | ssid 3624 |
. . . . . 6
|
29 | | xpss12 5225 |
. . . . . 6
|
30 | 28, 5, 29 | mp2an 708 |
. . . . 5
|
31 | | fnssres 6004 |
. . . . 5
|
32 | 27, 30, 31 | mp2an 708 |
. . . 4
|
33 | | ovelrn 6810 |
. . . . . . 7
|
34 | 32, 33 | ax-mp 5 |
. . . . . 6
|
35 | | ovres 6800 |
. . . . . . . . 9
|
36 | | shmulcl 28075 |
. . . . . . . . . 10
|
37 | 1, 36 | mp3an1 1411 |
. . . . . . . . 9
|
38 | 35, 37 | eqeltrd 2701 |
. . . . . . . 8
|
39 | | eleq1 2689 |
. . . . . . . 8
|
40 | 38, 39 | syl5ibrcom 237 |
. . . . . . 7
|
41 | 40 | rexlimivv 3036 |
. . . . . 6
|
42 | 34, 41 | sylbi 207 |
. . . . 5
|
43 | 42 | ssriv 3607 |
. . . 4
|
44 | | df-f 5892 |
. . . 4
|
45 | 32, 43, 44 | mpbir2an 955 |
. . 3
|
46 | | ax-1cn 9994 |
. . . . 5
|
47 | | ovres 6800 |
. . . . 5
|
48 | 46, 47 | mpan 706 |
. . . 4
|
49 | 1 | sheli 28071 |
. . . . 5
|
50 | | ax-hvmulid 27863 |
. . . . 5
|
51 | 49, 50 | syl 17 |
. . . 4
|
52 | 48, 51 | eqtrd 2656 |
. . 3
|
53 | | id 22 |
. . . . 5
|
54 | 1 | sheli 28071 |
. . . . 5
|
55 | | ax-hvdistr1 27865 |
. . . . 5
|
56 | 53, 49, 54, 55 | syl3an 1368 |
. . . 4
|
57 | | ovres 6800 |
. . . . . . 7
|
58 | 57 | 3adant1 1079 |
. . . . . 6
|
59 | 58 | oveq2d 6666 |
. . . . 5
|
60 | | shaddcl 28074 |
. . . . . . . 8
|
61 | 1, 60 | mp3an1 1411 |
. . . . . . 7
|
62 | | ovres 6800 |
. . . . . . 7
|
63 | 61, 62 | sylan2 491 |
. . . . . 6
|
64 | 63 | 3impb 1260 |
. . . . 5
|
65 | 59, 64 | eqtrd 2656 |
. . . 4
|
66 | | ovres 6800 |
. . . . . . 7
|
67 | 66 | 3adant3 1081 |
. . . . . 6
|
68 | | ovres 6800 |
. . . . . . 7
|
69 | 68 | 3adant2 1080 |
. . . . . 6
|
70 | 67, 69 | oveq12d 6668 |
. . . . 5
|
71 | | shmulcl 28075 |
. . . . . . . 8
|
72 | 1, 71 | mp3an1 1411 |
. . . . . . 7
|
73 | 72 | 3adant3 1081 |
. . . . . 6
|
74 | | shmulcl 28075 |
. . . . . . . 8
|
75 | 1, 74 | mp3an1 1411 |
. . . . . . 7
|
76 | 75 | 3adant2 1080 |
. . . . . 6
|
77 | 73, 76 | ovresd 6801 |
. . . . 5
|
78 | 70, 77 | eqtrd 2656 |
. . . 4
|
79 | 56, 65, 78 | 3eqtr4d 2666 |
. . 3
|
80 | | ax-hvdistr2 27866 |
. . . . 5
|
81 | 49, 80 | syl3an3 1361 |
. . . 4
|
82 | | addcl 10018 |
. . . . 5
|
83 | | ovres 6800 |
. . . . 5
|
84 | 82, 83 | stoic3 1701 |
. . . 4
|
85 | 66 | 3adant2 1080 |
. . . . . 6
|
86 | | ovres 6800 |
. . . . . . 7
|
87 | 86 | 3adant1 1079 |
. . . . . 6
|
88 | 85, 87 | oveq12d 6668 |
. . . . 5
|
89 | 72 | 3adant2 1080 |
. . . . . 6
|
90 | | shmulcl 28075 |
. . . . . . . 8
|
91 | 1, 90 | mp3an1 1411 |
. . . . . . 7
|
92 | 91 | 3adant1 1079 |
. . . . . 6
|
93 | 89, 92 | ovresd 6801 |
. . . . 5
|
94 | 88, 93 | eqtrd 2656 |
. . . 4
|
95 | 81, 84, 94 | 3eqtr4d 2666 |
. . 3
|
96 | | ax-hvmulass 27864 |
. . . . 5
|
97 | 49, 96 | syl3an3 1361 |
. . . 4
|
98 | | mulcl 10020 |
. . . . 5
|
99 | | ovres 6800 |
. . . . 5
|
100 | 98, 99 | stoic3 1701 |
. . . 4
|
101 | 87 | oveq2d 6666 |
. . . . 5
|
102 | | ovres 6800 |
. . . . . . 7
|
103 | 91, 102 | sylan2 491 |
. . . . . 6
|
104 | 103 | 3impb 1260 |
. . . . 5
|
105 | 101, 104 | eqtrd 2656 |
. . . 4
|
106 | 97, 100, 105 | 3eqtr4d 2666 |
. . 3
|
107 | | eqid 2622 |
. . 3
|
108 | 2, 12, 45, 52, 79, 95, 106, 107 | isvciOLD 27435 |
. 2
|
109 | | normf 27980 |
. . 3
|
110 | | fssres 6070 |
. . 3
|
111 | 109, 5, 110 | mp2an 708 |
. 2
|
112 | | fvres 6207 |
. . . . 5
|
113 | 112 | eqeq1d 2624 |
. . . 4
|
114 | | norm-i 27986 |
. . . . 5
|
115 | 49, 114 | syl 17 |
. . . 4
|
116 | 113, 115 | bitrd 268 |
. . 3
|
117 | 116 | biimpa 501 |
. 2
|
118 | | norm-iii 27997 |
. . . 4
|
119 | 49, 118 | sylan2 491 |
. . 3
|
120 | 66 | fveq2d 6195 |
. . . 4
|
121 | | fvres 6207 |
. . . . 5
|
122 | 72, 121 | syl 17 |
. . . 4
|
123 | 120, 122 | eqtrd 2656 |
. . 3
|
124 | 112 | adantl 482 |
. . . 4
|
125 | 124 | oveq2d 6666 |
. . 3
|
126 | 119, 123,
125 | 3eqtr4d 2666 |
. 2
|
127 | 1 | sheli 28071 |
. . . 4
|
128 | | norm-ii 27995 |
. . . 4
|
129 | 49, 127, 128 | syl2an 494 |
. . 3
|
130 | | ovres 6800 |
. . . . 5
|
131 | 130 | fveq2d 6195 |
. . . 4
|
132 | | shaddcl 28074 |
. . . . . 6
|
133 | 1, 132 | mp3an1 1411 |
. . . . 5
|
134 | | fvres 6207 |
. . . . 5
|
135 | 133, 134 | syl 17 |
. . . 4
|
136 | 131, 135 | eqtrd 2656 |
. . 3
|
137 | | fvres 6207 |
. . . 4
|
138 | 112, 137 | oveqan12d 6669 |
. . 3
|
139 | 129, 136,
138 | 3brtr4d 4685 |
. 2
|
140 | | hhssnvt.1 |
. 2
|
141 | 13, 24, 108, 111, 117, 126, 139, 140 | isnvi 27468 |
1
|