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 = ran G
isnvlem.2 Z = GId G
Assertion isnvlem G V S V N V G S N NrmCVec G S CVec OLD N : X x X N x = 0 x = Z y N y S x = y N x y X N x G y N x + N y

Proof

Step Hyp Ref Expression
1 isnvlem.1 X = ran G
2 isnvlem.2 Z = GId G
3 df-nv NrmCVec = g s n | g s CVec OLD n : ran g x ran g n x = 0 x = GId g y n y s x = y n x y ran g n x g y n x + n y
4 3 eleq2i G S N NrmCVec G S N g s n | g s CVec OLD n : ran g x ran g n x = 0 x = GId g y n y s x = y n x y ran g n x g y n x + n y
5 opeq1 g = G g s = G s
6 5 eleq1d g = G g s CVec OLD G s CVec OLD
7 rneq g = G ran g = ran G
8 7 1 eqtr4di g = G ran g = X
9 8 feq2d g = G n : ran g n : X
10 fveq2 g = G GId g = GId G
11 10 2 eqtr4di g = G GId g = Z
12 11 eqeq2d g = G x = GId g x = Z
13 12 imbi2d g = G n x = 0 x = GId g n x = 0 x = Z
14 oveq g = G x g y = x G y
15 14 fveq2d g = G n x g y = n x G y
16 15 breq1d g = G n x g y n x + n y n x G y n x + n y
17 8 16 raleqbidv g = G y ran g n x g y n x + n y y X n x G y n x + n y
18 13 17 3anbi13d g = G n x = 0 x = GId g y n y s x = y n x y ran g n x g y n x + n y n x = 0 x = Z y n y s x = y n x y X n x G y n x + n y
19 8 18 raleqbidv g = G x ran g n x = 0 x = GId g y n y s x = y n x y ran g n x g y n x + n y x X n x = 0 x = Z y n y s x = y n x y X n x G y n x + n y
20 6 9 19 3anbi123d g = G g s CVec OLD n : ran g x ran g n x = 0 x = GId g y n y s x = y n x y ran g n x g y n x + n y G s CVec OLD n : X x X n x = 0 x = Z y n y s x = y n x y X n x G y n x + n y
21 opeq2 s = S G s = G S
22 21 eleq1d s = S G s CVec OLD G S CVec OLD
23 oveq s = S y s x = y S x
24 23 fveqeq2d s = S n y s x = y n x n y S x = y n x
25 24 ralbidv s = S y n y s x = y n x y n y S x = y n x
26 25 3anbi2d s = S n x = 0 x = Z y n y s x = y n x y X n x G y n x + n y n x = 0 x = Z y n y S x = y n x y X n x G y n x + n y
27 26 ralbidv s = S x X n x = 0 x = Z y n y s x = y n x y X n x G y n x + n y x X n x = 0 x = Z y n y S x = y n x y X n x G y n x + n y
28 22 27 3anbi13d s = S G s CVec OLD n : X x X n x = 0 x = Z y n y s x = y n x y X n x G y n x + n y G S CVec OLD n : X x X n x = 0 x = Z y n y S x = y n x y X n x G y n x + n y
29 feq1 n = N n : X N : X
30 fveq1 n = N n x = N x
31 30 eqeq1d n = N n x = 0 N x = 0
32 31 imbi1d n = N n x = 0 x = Z N x = 0 x = Z
33 fveq1 n = N n y S x = N y S x
34 30 oveq2d n = N y n x = y N x
35 33 34 eqeq12d n = N n y S x = y n x N y S x = y N x
36 35 ralbidv n = N y n y S x = y n x y N y S x = y N x
37 fveq1 n = N n x G y = N x G y
38 fveq1 n = N n y = N y
39 30 38 oveq12d n = N n x + n y = N x + N y
40 37 39 breq12d n = N n x G y n x + n y N x G y N x + N y
41 40 ralbidv n = N y X n x G y n x + n y y X N x G y N x + N y
42 32 36 41 3anbi123d n = N n x = 0 x = Z y n y S x = y n x y X n x G y n x + n y N x = 0 x = Z y N y S x = y N x y X N x G y N x + N y
43 42 ralbidv n = N x X n x = 0 x = Z y n y S x = y n x y X n x G y n x + n y x X N x = 0 x = Z y N y S x = y N x y X N x G y N x + N y
44 29 43 3anbi23d n = N G S CVec OLD n : X x X n x = 0 x = Z y n y S x = y n x y X n x G y n x + n y G S CVec OLD N : X x X N x = 0 x = Z y N y S x = y N x y X N x G y N x + N y
45 20 28 44 eloprabg G V S V N V G S N g s n | g s CVec OLD n : ran g x ran g n x = 0 x = GId g y n y s x = y n x y ran g n x g y n x + n y G S CVec OLD N : X x X N x = 0 x = Z y N y S x = y N x y X N x G y N x + N y
46 4 45 syl5bb G V S V N V G S N NrmCVec G S CVec OLD N : X x X N x = 0 x = Z y N y S x = y N x y X N x G y N x + N y