Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nvnncan Structured version   Unicode version

Theorem nvnncan 22175
 Description: Cancellation law for a normed complex vector space. (Contributed by NM, 17-Dec-2007.) (New usage is discouraged.)
Hypotheses
Ref Expression
nvsubsub23.1
nvsubsub23.3
Assertion
Ref Expression
nvnncan

Proof of Theorem nvnncan
StepHypRef Expression
1 nvsubsub23.1 . . . 4
2 nvsubsub23.3 . . . 4
31, 2nvmcl 22159 . . 3
4 eqid 2442 . . . 4
5 eqid 2442 . . . 4
61, 4, 5, 2nvmval 22154 . . 3
73, 6syld3an3 1230 . 2
8 simp1 958 . . . . . 6
9 neg1cn 10098 . . . . . . 7
109a1i 11 . . . . . 6
11 simp2 959 . . . . . 6
121, 5nvscl 22138 . . . . . . . 8
139, 12mp3an2 1268 . . . . . . 7
14133adant2 977 . . . . . 6
151, 4, 5nvdi 22142 . . . . . 6
168, 10, 11, 14, 15syl13anc 1187 . . . . 5
171, 4, 5, 2nvmval 22154 . . . . . 6
1817oveq2d 6126 . . . . 5
19 ax-1cn 9079 . . . . . . . . . . . 12
2019, 19mul2negi 9512 . . . . . . . . . . 11
21 1t1e1 10157 . . . . . . . . . . 11
2220, 21eqtri 2462 . . . . . . . . . 10
2322oveq1i 6120 . . . . . . . . 9
241, 5nvsid 22139 . . . . . . . . 9
2523, 24syl5eq 2486 . . . . . . . 8
261, 5nvsass 22140 . . . . . . . . . 10
279, 26mp3anr1 1277 . . . . . . . . 9
289, 27mpanr1 666 . . . . . . . 8
2925, 28eqtr3d 2476 . . . . . . 7
30293adant2 977 . . . . . 6
3130oveq2d 6126 . . . . 5
3216, 18, 313eqtr4d 2484 . . . 4
3332oveq2d 6126 . . 3
341, 5nvscl 22138 . . . . . 6
359, 34mp3an2 1268 . . . . 5
36353adant3 978 . . . 4
37 simp3 960 . . . 4
381, 4nvass 22132 . . . 4
398, 11, 36, 37, 38syl13anc 1187 . . 3
40 eqid 2442 . . . . . 6
411, 4, 5, 40nvrinv 22165 . . . . 5
42413adant3 978 . . . 4
4342oveq1d 6125 . . 3
4433, 39, 433eqtr2d 2480 . 2
451, 4, 40nv0lid 22148 . . 3