Metamath Proof Explorer


Theorem cnnvm

Description: The vector subtraction operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis cnnvm.6 โŠข ๐‘ˆ = โŸจ โŸจ + , ยท โŸฉ , abs โŸฉ
Assertion cnnvm โˆ’ = ( โˆ’๐‘ฃ โ€˜ ๐‘ˆ )

Proof

Step Hyp Ref Expression
1 cnnvm.6 โŠข ๐‘ˆ = โŸจ โŸจ + , ยท โŸฉ , abs โŸฉ
2 mulm1 โŠข ( ๐‘ฆ โˆˆ โ„‚ โ†’ ( - 1 ยท ๐‘ฆ ) = - ๐‘ฆ )
3 2 adantl โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โ†’ ( - 1 ยท ๐‘ฆ ) = - ๐‘ฆ )
4 3 oveq2d โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โ†’ ( ๐‘ฅ + ( - 1 ยท ๐‘ฆ ) ) = ( ๐‘ฅ + - ๐‘ฆ ) )
5 negsub โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โ†’ ( ๐‘ฅ + - ๐‘ฆ ) = ( ๐‘ฅ โˆ’ ๐‘ฆ ) )
6 4 5 eqtr2d โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) = ( ๐‘ฅ + ( - 1 ยท ๐‘ฆ ) ) )
7 6 mpoeq3ia โŠข ( ๐‘ฅ โˆˆ โ„‚ , ๐‘ฆ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) = ( ๐‘ฅ โˆˆ โ„‚ , ๐‘ฆ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ + ( - 1 ยท ๐‘ฆ ) ) )
8 subf โŠข โˆ’ : ( โ„‚ ร— โ„‚ ) โŸถ โ„‚
9 ffn โŠข ( โˆ’ : ( โ„‚ ร— โ„‚ ) โŸถ โ„‚ โ†’ โˆ’ Fn ( โ„‚ ร— โ„‚ ) )
10 8 9 ax-mp โŠข โˆ’ Fn ( โ„‚ ร— โ„‚ )
11 fnov โŠข ( โˆ’ Fn ( โ„‚ ร— โ„‚ ) โ†” โˆ’ = ( ๐‘ฅ โˆˆ โ„‚ , ๐‘ฆ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โˆ’ ๐‘ฆ ) ) )
12 10 11 mpbi โŠข โˆ’ = ( ๐‘ฅ โˆˆ โ„‚ , ๐‘ฆ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ โˆ’ ๐‘ฆ ) )
13 1 cnnv โŠข ๐‘ˆ โˆˆ NrmCVec
14 1 cnnvba โŠข โ„‚ = ( BaseSet โ€˜ ๐‘ˆ )
15 1 cnnvg โŠข + = ( +๐‘ฃ โ€˜ ๐‘ˆ )
16 1 cnnvs โŠข ยท = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
17 eqid โŠข ( โˆ’๐‘ฃ โ€˜ ๐‘ˆ ) = ( โˆ’๐‘ฃ โ€˜ ๐‘ˆ )
18 14 15 16 17 nvmfval โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ( โˆ’๐‘ฃ โ€˜ ๐‘ˆ ) = ( ๐‘ฅ โˆˆ โ„‚ , ๐‘ฆ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ + ( - 1 ยท ๐‘ฆ ) ) ) )
19 13 18 ax-mp โŠข ( โˆ’๐‘ฃ โ€˜ ๐‘ˆ ) = ( ๐‘ฅ โˆˆ โ„‚ , ๐‘ฆ โˆˆ โ„‚ โ†ฆ ( ๐‘ฅ + ( - 1 ยท ๐‘ฆ ) ) )
20 7 12 19 3eqtr4i โŠข โˆ’ = ( โˆ’๐‘ฃ โ€˜ ๐‘ˆ )