# Metamath Proof Explorer

## Theorem isnvlem

Description: Lemma for isnv . (Contributed by NM, 11-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses isnvlem.1 ${⊢}{X}=\mathrm{ran}{G}$
isnvlem.2 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
Assertion isnvlem ${⊢}\left({G}\in \mathrm{V}\wedge {S}\in \mathrm{V}\wedge {N}\in \mathrm{V}\right)\to \left(⟨⟨{G},{S}⟩,{N}⟩\in \mathrm{NrmCVec}↔\left(⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\wedge {N}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 isnvlem.1 ${⊢}{X}=\mathrm{ran}{G}$
2 isnvlem.2 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
3 df-nv ${⊢}\mathrm{NrmCVec}=\left\{⟨⟨{g},{s}⟩,{n}⟩|\left(⟨{g},{s}⟩\in {CVec}_{\mathrm{OLD}}\wedge {n}:\mathrm{ran}{g}⟶ℝ\wedge \forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}=\mathrm{GId}\left({g}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{n}\left({x}{g}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)\right)\right\}$
4 3 eleq2i ${⊢}⟨⟨{G},{S}⟩,{N}⟩\in \mathrm{NrmCVec}↔⟨⟨{G},{S}⟩,{N}⟩\in \left\{⟨⟨{g},{s}⟩,{n}⟩|\left(⟨{g},{s}⟩\in {CVec}_{\mathrm{OLD}}\wedge {n}:\mathrm{ran}{g}⟶ℝ\wedge \forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}=\mathrm{GId}\left({g}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{n}\left({x}{g}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)\right)\right\}$
5 opeq1 ${⊢}{g}={G}\to ⟨{g},{s}⟩=⟨{G},{s}⟩$
6 5 eleq1d ${⊢}{g}={G}\to \left(⟨{g},{s}⟩\in {CVec}_{\mathrm{OLD}}↔⟨{G},{s}⟩\in {CVec}_{\mathrm{OLD}}\right)$
7 rneq ${⊢}{g}={G}\to \mathrm{ran}{g}=\mathrm{ran}{G}$
8 7 1 syl6eqr ${⊢}{g}={G}\to \mathrm{ran}{g}={X}$
9 8 feq2d ${⊢}{g}={G}\to \left({n}:\mathrm{ran}{g}⟶ℝ↔{n}:{X}⟶ℝ\right)$
10 fveq2 ${⊢}{g}={G}\to \mathrm{GId}\left({g}\right)=\mathrm{GId}\left({G}\right)$
11 10 2 syl6eqr ${⊢}{g}={G}\to \mathrm{GId}\left({g}\right)={Z}$
12 11 eqeq2d ${⊢}{g}={G}\to \left({x}=\mathrm{GId}\left({g}\right)↔{x}={Z}\right)$
13 12 imbi2d ${⊢}{g}={G}\to \left(\left({n}\left({x}\right)=0\to {x}=\mathrm{GId}\left({g}\right)\right)↔\left({n}\left({x}\right)=0\to {x}={Z}\right)\right)$
14 oveq ${⊢}{g}={G}\to {x}{g}{y}={x}{G}{y}$
15 14 fveq2d ${⊢}{g}={G}\to {n}\left({x}{g}{y}\right)={n}\left({x}{G}{y}\right)$
16 15 breq1d ${⊢}{g}={G}\to \left({n}\left({x}{g}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)↔{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)$
17 8 16 raleqbidv ${⊢}{g}={G}\to \left(\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{n}\left({x}{g}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)$
18 13 17 3anbi13d ${⊢}{g}={G}\to \left(\left(\left({n}\left({x}\right)=0\to {x}=\mathrm{GId}\left({g}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{n}\left({x}{g}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)↔\left(\left({n}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)\right)$
19 8 18 raleqbidv ${⊢}{g}={G}\to \left(\forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}=\mathrm{GId}\left({g}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{n}\left({x}{g}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)\right)$
20 6 9 19 3anbi123d ${⊢}{g}={G}\to \left(\left(⟨{g},{s}⟩\in {CVec}_{\mathrm{OLD}}\wedge {n}:\mathrm{ran}{g}⟶ℝ\wedge \forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}=\mathrm{GId}\left({g}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{n}\left({x}{g}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)\right)↔\left(⟨{G},{s}⟩\in {CVec}_{\mathrm{OLD}}\wedge {n}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)\right)\right)$
21 opeq2 ${⊢}{s}={S}\to ⟨{G},{s}⟩=⟨{G},{S}⟩$
22 21 eleq1d ${⊢}{s}={S}\to \left(⟨{G},{s}⟩\in {CVec}_{\mathrm{OLD}}↔⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\right)$
23 oveq ${⊢}{s}={S}\to {y}{s}{x}={y}{S}{x}$
24 23 fveqeq2d ${⊢}{s}={S}\to \left({n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)↔{n}\left({y}{S}{x}\right)=\left|{y}\right|{n}\left({x}\right)\right)$
25 24 ralbidv ${⊢}{s}={S}\to \left(\forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)↔\forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{S}{x}\right)=\left|{y}\right|{n}\left({x}\right)\right)$
26 25 3anbi2d ${⊢}{s}={S}\to \left(\left(\left({n}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)↔\left(\left({n}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{S}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)\right)$
27 26 ralbidv ${⊢}{s}={S}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{S}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)\right)$
28 22 27 3anbi13d ${⊢}{s}={S}\to \left(\left(⟨{G},{s}⟩\in {CVec}_{\mathrm{OLD}}\wedge {n}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)\right)↔\left(⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\wedge {n}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{S}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)\right)\right)$
29 feq1 ${⊢}{n}={N}\to \left({n}:{X}⟶ℝ↔{N}:{X}⟶ℝ\right)$
30 fveq1 ${⊢}{n}={N}\to {n}\left({x}\right)={N}\left({x}\right)$
31 30 eqeq1d ${⊢}{n}={N}\to \left({n}\left({x}\right)=0↔{N}\left({x}\right)=0\right)$
32 31 imbi1d ${⊢}{n}={N}\to \left(\left({n}\left({x}\right)=0\to {x}={Z}\right)↔\left({N}\left({x}\right)=0\to {x}={Z}\right)\right)$
33 fveq1 ${⊢}{n}={N}\to {n}\left({y}{S}{x}\right)={N}\left({y}{S}{x}\right)$
34 30 oveq2d ${⊢}{n}={N}\to \left|{y}\right|{n}\left({x}\right)=\left|{y}\right|{N}\left({x}\right)$
35 33 34 eqeq12d ${⊢}{n}={N}\to \left({n}\left({y}{S}{x}\right)=\left|{y}\right|{n}\left({x}\right)↔{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\right)$
36 35 ralbidv ${⊢}{n}={N}\to \left(\forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{S}{x}\right)=\left|{y}\right|{n}\left({x}\right)↔\forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\right)$
37 fveq1 ${⊢}{n}={N}\to {n}\left({x}{G}{y}\right)={N}\left({x}{G}{y}\right)$
38 fveq1 ${⊢}{n}={N}\to {n}\left({y}\right)={N}\left({y}\right)$
39 30 38 oveq12d ${⊢}{n}={N}\to {n}\left({x}\right)+{n}\left({y}\right)={N}\left({x}\right)+{N}\left({y}\right)$
40 37 39 breq12d ${⊢}{n}={N}\to \left({n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)↔{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)$
41 40 ralbidv ${⊢}{n}={N}\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)$
42 32 36 41 3anbi123d ${⊢}{n}={N}\to \left(\left(\left({n}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{S}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)↔\left(\left({N}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)$
43 42 ralbidv ${⊢}{n}={N}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{S}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)$
44 29 43 3anbi23d ${⊢}{n}={N}\to \left(\left(⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\wedge {n}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{S}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{n}\left({x}{G}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)\right)↔\left(⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\wedge {N}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)\right)$
45 20 28 44 eloprabg ${⊢}\left({G}\in \mathrm{V}\wedge {S}\in \mathrm{V}\wedge {N}\in \mathrm{V}\right)\to \left(⟨⟨{G},{S}⟩,{N}⟩\in \left\{⟨⟨{g},{s}⟩,{n}⟩|\left(⟨{g},{s}⟩\in {CVec}_{\mathrm{OLD}}\wedge {n}:\mathrm{ran}{g}⟶ℝ\wedge \forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)=0\to {x}=\mathrm{GId}\left({g}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{n}\left({y}{s}{x}\right)=\left|{y}\right|{n}\left({x}\right)\wedge \forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}{n}\left({x}{g}{y}\right)\le {n}\left({x}\right)+{n}\left({y}\right)\right)\right)\right\}↔\left(⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\wedge {N}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)\right)$
46 4 45 syl5bb ${⊢}\left({G}\in \mathrm{V}\wedge {S}\in \mathrm{V}\wedge {N}\in \mathrm{V}\right)\to \left(⟨⟨{G},{S}⟩,{N}⟩\in \mathrm{NrmCVec}↔\left(⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\wedge {N}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)\right)$