Colors of
variables: wff
setvar class |
Syntax hints:
β wi 4 β§ wa 396
= wceq 1541 β
wcel 2106 βcfv 6516
βcr 11074 NrmCVeccnv 29623 BaseSetcba 29625
normCVcnmcv 29629 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5262 ax-sep 5276 ax-nul 5283 ax-pr 5404 ax-un 7692 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-reu 3365 df-rab 3419 df-v 3461 df-sbc 3758 df-csb 3874 df-dif 3931 df-un 3933 df-in 3935 df-ss 3945 df-nul 4303 df-if 4507 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4886 df-iun 4976 df-br 5126 df-opab 5188 df-mpt 5209 df-id 5551 df-xp 5659 df-rel 5660 df-cnv 5661 df-co 5662 df-dm 5663 df-rn 5664 df-res 5665 df-ima 5666 df-iota 6468 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-ov 7380 df-oprab 7381 df-1st 7941 df-2nd 7942 df-vc 29598 df-nv 29631 df-va 29634 df-ba 29635 df-sm 29636 df-0v 29637 df-nmcv 29639 |
This theorem is referenced by: nvcli
29701 nvm1
29704 nvpi
29706 nvz0
29707 nvmtri
29710 nvabs
29711 nvge0
29712 nvgt0
29713 nv1
29714 nmcvcn
29734 smcnlem
29736 ipval2lem2
29743 4ipval2
29747 ipidsq
29749 ipnm
29750 ipz
29758 nmosetre
29803 nmooge0
29806 nmoub3i
29812 nmounbi
29815 nmlno0lem
29832 nmblolbii
29838 blocnilem
29843 ipblnfi
29894 ubthlem1
29909 ubthlem2
29910 ubthlem3
29911 minvecolem1
29913 minvecolem2
29914 minvecolem4
29919 minvecolem5
29920 minvecolem6
29921 hlipgt0
29953 htthlem
29956 |