Metamath Proof Explorer

Theorem hhssnv

Description: Normed complex vector space property of a subspace. (Contributed by NM, 26-Mar-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhssnvt.1 โŠข ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ
hhssnv.2 โŠข ๐ป โˆˆ Sโ„‹
Assertion hhssnv ๐‘Š โˆˆ NrmCVec

Proof

Step Hyp Ref Expression
1 hhssnvt.1 โŠข ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ
2 hhssnv.2 โŠข ๐ป โˆˆ Sโ„‹
3 2 hhssabloi โŠข ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โˆˆ AbelOp
4 ablogrpo โŠข ( ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โˆˆ AbelOp โ†’ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โˆˆ GrpOp )
5 3 4 ax-mp โŠข ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โˆˆ GrpOp
6 2 shssii โŠข ๐ป โŠ† โ„‹
7 xpss12 โŠข ( ( ๐ป โŠ† โ„‹ โˆง ๐ป โŠ† โ„‹ ) โ†’ ( ๐ป ร— ๐ป ) โŠ† ( โ„‹ ร— โ„‹ ) )
8 6 6 7 mp2an โŠข ( ๐ป ร— ๐ป ) โŠ† ( โ„‹ ร— โ„‹ )
9 ax-hfvadd โŠข +โ„Ž : ( โ„‹ ร— โ„‹ ) โŸถ โ„‹
10 9 fdmi โŠข dom +โ„Ž = ( โ„‹ ร— โ„‹ )
11 8 10 sseqtrri โŠข ( ๐ป ร— ๐ป ) โŠ† dom +โ„Ž
12 ssdmres โŠข ( ( ๐ป ร— ๐ป ) โŠ† dom +โ„Ž โ†” dom ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) = ( ๐ป ร— ๐ป ) )
13 11 12 mpbi โŠข dom ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) = ( ๐ป ร— ๐ป )
14 5 13 grporn โŠข ๐ป = ran ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) )
15 sh0 โŠข ( ๐ป โˆˆ Sโ„‹ โ†’ 0โ„Ž โˆˆ ๐ป )
16 2 15 ax-mp โŠข 0โ„Ž โˆˆ ๐ป
17 ovres โŠข ( ( 0โ„Ž โˆˆ ๐ป โˆง 0โ„Ž โˆˆ ๐ป ) โ†’ ( 0โ„Ž ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) 0โ„Ž ) = ( 0โ„Ž +โ„Ž 0โ„Ž ) )
18 16 16 17 mp2an โŠข ( 0โ„Ž ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) 0โ„Ž ) = ( 0โ„Ž +โ„Ž 0โ„Ž )
19 ax-hv0cl โŠข 0โ„Ž โˆˆ โ„‹
20 19 hvaddlidi โŠข ( 0โ„Ž +โ„Ž 0โ„Ž ) = 0โ„Ž
21 18 20 eqtri โŠข ( 0โ„Ž ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) 0โ„Ž ) = 0โ„Ž
22 eqid โŠข ( GId โ€˜ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ) = ( GId โ€˜ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) )
23 14 22 grpoid โŠข ( ( ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โˆˆ GrpOp โˆง 0โ„Ž โˆˆ ๐ป ) โ†’ ( 0โ„Ž = ( GId โ€˜ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ) โ†” ( 0โ„Ž ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) 0โ„Ž ) = 0โ„Ž ) )
24 5 16 23 mp2an โŠข ( 0โ„Ž = ( GId โ€˜ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ) โ†” ( 0โ„Ž ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) 0โ„Ž ) = 0โ„Ž )
25 21 24 mpbir โŠข 0โ„Ž = ( GId โ€˜ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) )
26 ax-hfvmul โŠข ยทโ„Ž : ( โ„‚ ร— โ„‹ ) โŸถ โ„‹
27 ffn โŠข ( ยทโ„Ž : ( โ„‚ ร— โ„‹ ) โŸถ โ„‹ โ†’ ยทโ„Ž Fn ( โ„‚ ร— โ„‹ ) )
28 26 27 ax-mp โŠข ยทโ„Ž Fn ( โ„‚ ร— โ„‹ )
29 ssid โŠข โ„‚ โŠ† โ„‚
30 xpss12 โŠข ( ( โ„‚ โŠ† โ„‚ โˆง ๐ป โŠ† โ„‹ ) โ†’ ( โ„‚ ร— ๐ป ) โŠ† ( โ„‚ ร— โ„‹ ) )
31 29 6 30 mp2an โŠข ( โ„‚ ร— ๐ป ) โŠ† ( โ„‚ ร— โ„‹ )
32 fnssres โŠข ( ( ยทโ„Ž Fn ( โ„‚ ร— โ„‹ ) โˆง ( โ„‚ ร— ๐ป ) โŠ† ( โ„‚ ร— โ„‹ ) ) โ†’ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) Fn ( โ„‚ ร— ๐ป ) )
33 28 31 32 mp2an โŠข ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) Fn ( โ„‚ ร— ๐ป )
34 ovelrn โŠข ( ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) Fn ( โ„‚ ร— ๐ป ) โ†’ ( ๐‘ง โˆˆ ran ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โ†” โˆƒ ๐‘ฅ โˆˆ โ„‚ โˆƒ ๐‘ฆ โˆˆ ๐ป ๐‘ง = ( ๐‘ฅ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฆ ) ) )
35 33 34 ax-mp โŠข ( ๐‘ง โˆˆ ran ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โ†” โˆƒ ๐‘ฅ โˆˆ โ„‚ โˆƒ ๐‘ฆ โˆˆ ๐ป ๐‘ง = ( ๐‘ฅ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฆ ) )
36 ovres โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ๐‘ฅ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฆ ) = ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) )
37 shmulcl โŠข ( ( ๐ป โˆˆ Sโ„‹ โˆง ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ ๐ป )
38 2 37 mp3an1 โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ ๐ป )
39 36 38 eqeltrd โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ๐‘ฅ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฆ ) โˆˆ ๐ป )
40 eleq1 โŠข ( ๐‘ง = ( ๐‘ฅ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฆ ) โ†’ ( ๐‘ง โˆˆ ๐ป โ†” ( ๐‘ฅ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฆ ) โˆˆ ๐ป ) )
41 39 40 syl5ibrcom โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ๐‘ง = ( ๐‘ฅ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฆ ) โ†’ ๐‘ง โˆˆ ๐ป ) )
42 41 rexlimivv โŠข ( โˆƒ ๐‘ฅ โˆˆ โ„‚ โˆƒ ๐‘ฆ โˆˆ ๐ป ๐‘ง = ( ๐‘ฅ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฆ ) โ†’ ๐‘ง โˆˆ ๐ป )
43 35 42 sylbi โŠข ( ๐‘ง โˆˆ ran ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โ†’ ๐‘ง โˆˆ ๐ป )
44 43 ssriv โŠข ran ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป
45 df-f โŠข ( ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) : ( โ„‚ ร— ๐ป ) โŸถ ๐ป โ†” ( ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) Fn ( โ„‚ ร— ๐ป ) โˆง ran ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) )
46 33 44 45 mpbir2an โŠข ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) : ( โ„‚ ร— ๐ป ) โŸถ ๐ป
47 ax-1cn โŠข 1 โˆˆ โ„‚
48 ovres โŠข ( ( 1 โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( 1 ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( 1 ยทโ„Ž ๐‘ฅ ) )
49 47 48 mpan โŠข ( ๐‘ฅ โˆˆ ๐ป โ†’ ( 1 ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( 1 ยทโ„Ž ๐‘ฅ ) )
50 2 sheli โŠข ( ๐‘ฅ โˆˆ ๐ป โ†’ ๐‘ฅ โˆˆ โ„‹ )
51 ax-hvmulid โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( 1 ยทโ„Ž ๐‘ฅ ) = ๐‘ฅ )
52 50 51 syl โŠข ( ๐‘ฅ โˆˆ ๐ป โ†’ ( 1 ยทโ„Ž ๐‘ฅ ) = ๐‘ฅ )
53 49 52 eqtrd โŠข ( ๐‘ฅ โˆˆ ๐ป โ†’ ( 1 ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ๐‘ฅ )
54 id โŠข ( ๐‘ฆ โˆˆ โ„‚ โ†’ ๐‘ฆ โˆˆ โ„‚ )
55 2 sheli โŠข ( ๐‘ง โˆˆ ๐ป โ†’ ๐‘ง โˆˆ โ„‹ )
56 ax-hvdistr1 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘ฆ ยทโ„Ž ( ๐‘ฅ +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) +โ„Ž ( ๐‘ฆ ยทโ„Ž ๐‘ง ) ) )
57 54 50 55 56 syl3an โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ยทโ„Ž ( ๐‘ฅ +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) +โ„Ž ( ๐‘ฆ ยทโ„Ž ๐‘ง ) ) )
58 ovres โŠข ( ( ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฅ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ๐‘ง ) = ( ๐‘ฅ +โ„Ž ๐‘ง ) )
59 58 3adant1 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฅ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ๐‘ง ) = ( ๐‘ฅ +โ„Ž ๐‘ง ) )
60 59 oveq2d โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ฅ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ๐‘ง ) ) = ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ฅ +โ„Ž ๐‘ง ) ) )
61 shaddcl โŠข ( ( ๐ป โˆˆ Sโ„‹ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฅ +โ„Ž ๐‘ง ) โˆˆ ๐ป )
62 2 61 mp3an1 โŠข ( ( ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฅ +โ„Ž ๐‘ง ) โˆˆ ๐ป )
63 ovres โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐‘ฅ +โ„Ž ๐‘ง ) โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ฅ +โ„Ž ๐‘ง ) ) = ( ๐‘ฆ ยทโ„Ž ( ๐‘ฅ +โ„Ž ๐‘ง ) ) )
64 62 63 sylan2 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ฅ +โ„Ž ๐‘ง ) ) = ( ๐‘ฆ ยทโ„Ž ( ๐‘ฅ +โ„Ž ๐‘ง ) ) )
65 64 3impb โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ฅ +โ„Ž ๐‘ง ) ) = ( ๐‘ฆ ยทโ„Ž ( ๐‘ฅ +โ„Ž ๐‘ง ) ) )
66 60 65 eqtrd โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ฅ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ๐‘ง ) ) = ( ๐‘ฆ ยทโ„Ž ( ๐‘ฅ +โ„Ž ๐‘ง ) ) )
67 ovres โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) )
68 67 3adant3 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) )
69 ovres โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ง ) = ( ๐‘ฆ ยทโ„Ž ๐‘ง ) )
70 69 3adant2 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ง ) = ( ๐‘ฆ ยทโ„Ž ๐‘ง ) )
71 68 70 oveq12d โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ง ) ) = ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ( ๐‘ฆ ยทโ„Ž ๐‘ง ) ) )
72 shmulcl โŠข ( ( ๐ป โˆˆ Sโ„‹ โˆง ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) โˆˆ ๐ป )
73 2 72 mp3an1 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) โˆˆ ๐ป )
74 73 3adant3 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) โˆˆ ๐ป )
75 shmulcl โŠข ( ( ๐ป โˆˆ Sโ„‹ โˆง ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ยทโ„Ž ๐‘ง ) โˆˆ ๐ป )
76 2 75 mp3an1 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ยทโ„Ž ๐‘ง ) โˆˆ ๐ป )
77 76 3adant2 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ยทโ„Ž ๐‘ง ) โˆˆ ๐ป )
78 74 77 ovresd โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ( ๐‘ฆ ยทโ„Ž ๐‘ง ) ) = ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) +โ„Ž ( ๐‘ฆ ยทโ„Ž ๐‘ง ) ) )
79 71 78 eqtrd โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ง ) ) = ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) +โ„Ž ( ๐‘ฆ ยทโ„Ž ๐‘ง ) ) )
80 57 66 79 3eqtr4d โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ง โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ฅ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ๐‘ง ) ) = ( ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ง ) ) )
81 ax-hvdistr2 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฆ + ๐‘ง ) ยทโ„Ž ๐‘ฅ ) = ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) +โ„Ž ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) )
82 50 81 syl3an3 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ + ๐‘ง ) ยทโ„Ž ๐‘ฅ ) = ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) +โ„Ž ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) )
83 addcl โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ ) โ†’ ( ๐‘ฆ + ๐‘ง ) โˆˆ โ„‚ )
84 ovres โŠข ( ( ( ๐‘ฆ + ๐‘ง ) โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ + ๐‘ง ) ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( ( ๐‘ฆ + ๐‘ง ) ยทโ„Ž ๐‘ฅ ) )
85 83 84 stoic3 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ + ๐‘ง ) ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( ( ๐‘ฆ + ๐‘ง ) ยทโ„Ž ๐‘ฅ ) )
86 67 3adant2 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) )
87 ovres โŠข ( ( ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ง ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( ๐‘ง ยทโ„Ž ๐‘ฅ ) )
88 87 3adant1 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ง ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( ๐‘ง ยทโ„Ž ๐‘ฅ ) )
89 86 88 oveq12d โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ( ๐‘ง ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ) = ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) )
90 73 3adant2 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) โˆˆ ๐ป )
91 shmulcl โŠข ( ( ๐ป โˆˆ Sโ„‹ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ง ยทโ„Ž ๐‘ฅ ) โˆˆ ๐ป )
92 2 91 mp3an1 โŠข ( ( ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ง ยทโ„Ž ๐‘ฅ ) โˆˆ ๐ป )
93 92 3adant1 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ง ยทโ„Ž ๐‘ฅ ) โˆˆ ๐ป )
94 90 93 ovresd โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) = ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) +โ„Ž ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) )
95 89 94 eqtrd โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ( ๐‘ง ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ) = ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) +โ„Ž ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) )
96 82 85 95 3eqtr4d โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ + ๐‘ง ) ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ( ๐‘ง ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ) )
97 ax-hvmulass โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฆ ยท ๐‘ง ) ยทโ„Ž ๐‘ฅ ) = ( ๐‘ฆ ยทโ„Ž ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) )
98 50 97 syl3an3 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ ยท ๐‘ง ) ยทโ„Ž ๐‘ฅ ) = ( ๐‘ฆ ยทโ„Ž ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) )
99 mulcl โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ ) โ†’ ( ๐‘ฆ ยท ๐‘ง ) โˆˆ โ„‚ )
100 ovres โŠข ( ( ( ๐‘ฆ ยท ๐‘ง ) โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ ยท ๐‘ง ) ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( ( ๐‘ฆ ยท ๐‘ง ) ยทโ„Ž ๐‘ฅ ) )
101 99 100 stoic3 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ ยท ๐‘ง ) ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( ( ๐‘ฆ ยท ๐‘ง ) ยทโ„Ž ๐‘ฅ ) )
102 88 oveq2d โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ง ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ) = ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) )
103 ovres โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐‘ง ยทโ„Ž ๐‘ฅ ) โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) = ( ๐‘ฆ ยทโ„Ž ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) )
104 92 103 sylan2 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) = ( ๐‘ฆ ยทโ„Ž ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) )
105 104 3impb โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) = ( ๐‘ฆ ยทโ„Ž ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) )
106 102 105 eqtrd โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ง ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ) = ( ๐‘ฆ ยทโ„Ž ( ๐‘ง ยทโ„Ž ๐‘ฅ ) ) )
107 98 101 106 3eqtr4d โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ง โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( ๐‘ฆ ยท ๐‘ง ) ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) = ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ( ๐‘ง ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ) )
108 eqid โŠข โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ = โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ
109 3 13 46 53 80 96 107 108 isvciOLD โŠข โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ โˆˆ CVecOLD
110 normf โŠข normโ„Ž : โ„‹ โŸถ โ„
111 fssres โŠข ( ( normโ„Ž : โ„‹ โŸถ โ„ โˆง ๐ป โŠ† โ„‹ ) โ†’ ( normโ„Ž โ†พ ๐ป ) : ๐ป โŸถ โ„ )
112 110 6 111 mp2an โŠข ( normโ„Ž โ†พ ๐ป ) : ๐ป โŸถ โ„
113 fvres โŠข ( ๐‘ฅ โˆˆ ๐ป โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ๐‘ฅ ) = ( normโ„Ž โ€˜ ๐‘ฅ ) )
114 113 eqeq1d โŠข ( ๐‘ฅ โˆˆ ๐ป โ†’ ( ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ๐‘ฅ ) = 0 โ†” ( normโ„Ž โ€˜ ๐‘ฅ ) = 0 ) )
115 norm-i โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ๐‘ฅ ) = 0 โ†” ๐‘ฅ = 0โ„Ž ) )
116 50 115 syl โŠข ( ๐‘ฅ โˆˆ ๐ป โ†’ ( ( normโ„Ž โ€˜ ๐‘ฅ ) = 0 โ†” ๐‘ฅ = 0โ„Ž ) )
117 114 116 bitrd โŠข ( ๐‘ฅ โˆˆ ๐ป โ†’ ( ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ๐‘ฅ ) = 0 โ†” ๐‘ฅ = 0โ„Ž ) )
118 117 biimpa โŠข ( ( ๐‘ฅ โˆˆ ๐ป โˆง ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ๐‘ฅ ) = 0 ) โ†’ ๐‘ฅ = 0โ„Ž )
119 norm-iii โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( normโ„Ž โ€˜ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ) = ( ( abs โ€˜ ๐‘ฆ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) )
120 50 119 sylan2 โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( normโ„Ž โ€˜ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ) = ( ( abs โ€˜ ๐‘ฆ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) )
121 67 fveq2d โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ) = ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ) )
122 fvres โŠข ( ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) โˆˆ ๐ป โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ) )
123 73 122 syl โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ) )
124 121 123 eqtrd โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ) )
125 113 adantl โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ๐‘ฅ ) = ( normโ„Ž โ€˜ ๐‘ฅ ) )
126 125 oveq2d โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( abs โ€˜ ๐‘ฆ ) ยท ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ๐‘ฅ ) ) = ( ( abs โ€˜ ๐‘ฆ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) )
127 120 124 126 3eqtr4d โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ ๐ป ) โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ( ๐‘ฆ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) ๐‘ฅ ) ) = ( ( abs โ€˜ ๐‘ฆ ) ยท ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ๐‘ฅ ) ) )
128 2 sheli โŠข ( ๐‘ฆ โˆˆ ๐ป โ†’ ๐‘ฆ โˆˆ โ„‹ )
129 norm-ii โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( normโ„Ž โ€˜ ( ๐‘ฅ +โ„Ž ๐‘ฆ ) ) โ‰ค ( ( normโ„Ž โ€˜ ๐‘ฅ ) + ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
130 50 128 129 syl2an โŠข ( ( ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( normโ„Ž โ€˜ ( ๐‘ฅ +โ„Ž ๐‘ฆ ) ) โ‰ค ( ( normโ„Ž โ€˜ ๐‘ฅ ) + ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
131 ovres โŠข ( ( ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ๐‘ฅ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ๐‘ฆ ) = ( ๐‘ฅ +โ„Ž ๐‘ฆ ) )
132 131 fveq2d โŠข ( ( ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ( ๐‘ฅ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ๐‘ฆ ) ) = ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ( ๐‘ฅ +โ„Ž ๐‘ฆ ) ) )
133 shaddcl โŠข ( ( ๐ป โˆˆ Sโ„‹ โˆง ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ๐‘ฅ +โ„Ž ๐‘ฆ ) โˆˆ ๐ป )
134 2 133 mp3an1 โŠข ( ( ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ๐‘ฅ +โ„Ž ๐‘ฆ ) โˆˆ ๐ป )
135 fvres โŠข ( ( ๐‘ฅ +โ„Ž ๐‘ฆ ) โˆˆ ๐ป โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ( ๐‘ฅ +โ„Ž ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ( ๐‘ฅ +โ„Ž ๐‘ฆ ) ) )
136 134 135 syl โŠข ( ( ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ( ๐‘ฅ +โ„Ž ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ( ๐‘ฅ +โ„Ž ๐‘ฆ ) ) )
137 132 136 eqtrd โŠข ( ( ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ( ๐‘ฅ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ( ๐‘ฅ +โ„Ž ๐‘ฆ ) ) )
138 fvres โŠข ( ๐‘ฆ โˆˆ ๐ป โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ๐‘ฆ ) = ( normโ„Ž โ€˜ ๐‘ฆ ) )
139 113 138 oveqan12d โŠข ( ( ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ๐‘ฅ ) + ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ๐‘ฆ ) ) = ( ( normโ„Ž โ€˜ ๐‘ฅ ) + ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
140 130 137 139 3brtr4d โŠข ( ( ๐‘ฅ โˆˆ ๐ป โˆง ๐‘ฆ โˆˆ ๐ป ) โ†’ ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ( ๐‘ฅ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) ๐‘ฆ ) ) โ‰ค ( ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ๐‘ฅ ) + ( ( normโ„Ž โ†พ ๐ป ) โ€˜ ๐‘ฆ ) ) )
141 14 25 109 112 118 127 140 1 isnvi โŠข ๐‘Š โˆˆ NrmCVec