Metamath Proof Explorer


Theorem mulcnsr

Description: Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion mulcnsr ( ( ( ๐ด โˆˆ R โˆง ๐ต โˆˆ R ) โˆง ( ๐ถ โˆˆ R โˆง ๐ท โˆˆ R ) ) โ†’ ( โŸจ ๐ด , ๐ต โŸฉ ยท โŸจ ๐ถ , ๐ท โŸฉ ) = โŸจ ( ( ๐ด ยทR ๐ถ ) +R ( -1R ยทR ( ๐ต ยทR ๐ท ) ) ) , ( ( ๐ต ยทR ๐ถ ) +R ( ๐ด ยทR ๐ท ) ) โŸฉ )

Proof

Step Hyp Ref Expression
1 opex โŠข โŸจ ( ( ๐ด ยทR ๐ถ ) +R ( -1R ยทR ( ๐ต ยทR ๐ท ) ) ) , ( ( ๐ต ยทR ๐ถ ) +R ( ๐ด ยทR ๐ท ) ) โŸฉ โˆˆ V
2 oveq1 โŠข ( ๐‘ค = ๐ด โ†’ ( ๐‘ค ยทR ๐‘ข ) = ( ๐ด ยทR ๐‘ข ) )
3 oveq1 โŠข ( ๐‘ฃ = ๐ต โ†’ ( ๐‘ฃ ยทR ๐‘“ ) = ( ๐ต ยทR ๐‘“ ) )
4 3 oveq2d โŠข ( ๐‘ฃ = ๐ต โ†’ ( -1R ยทR ( ๐‘ฃ ยทR ๐‘“ ) ) = ( -1R ยทR ( ๐ต ยทR ๐‘“ ) ) )
5 2 4 oveqan12d โŠข ( ( ๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต ) โ†’ ( ( ๐‘ค ยทR ๐‘ข ) +R ( -1R ยทR ( ๐‘ฃ ยทR ๐‘“ ) ) ) = ( ( ๐ด ยทR ๐‘ข ) +R ( -1R ยทR ( ๐ต ยทR ๐‘“ ) ) ) )
6 oveq1 โŠข ( ๐‘ฃ = ๐ต โ†’ ( ๐‘ฃ ยทR ๐‘ข ) = ( ๐ต ยทR ๐‘ข ) )
7 oveq1 โŠข ( ๐‘ค = ๐ด โ†’ ( ๐‘ค ยทR ๐‘“ ) = ( ๐ด ยทR ๐‘“ ) )
8 6 7 oveqan12rd โŠข ( ( ๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต ) โ†’ ( ( ๐‘ฃ ยทR ๐‘ข ) +R ( ๐‘ค ยทR ๐‘“ ) ) = ( ( ๐ต ยทR ๐‘ข ) +R ( ๐ด ยทR ๐‘“ ) ) )
9 5 8 opeq12d โŠข ( ( ๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต ) โ†’ โŸจ ( ( ๐‘ค ยทR ๐‘ข ) +R ( -1R ยทR ( ๐‘ฃ ยทR ๐‘“ ) ) ) , ( ( ๐‘ฃ ยทR ๐‘ข ) +R ( ๐‘ค ยทR ๐‘“ ) ) โŸฉ = โŸจ ( ( ๐ด ยทR ๐‘ข ) +R ( -1R ยทR ( ๐ต ยทR ๐‘“ ) ) ) , ( ( ๐ต ยทR ๐‘ข ) +R ( ๐ด ยทR ๐‘“ ) ) โŸฉ )
10 oveq2 โŠข ( ๐‘ข = ๐ถ โ†’ ( ๐ด ยทR ๐‘ข ) = ( ๐ด ยทR ๐ถ ) )
11 oveq2 โŠข ( ๐‘“ = ๐ท โ†’ ( ๐ต ยทR ๐‘“ ) = ( ๐ต ยทR ๐ท ) )
12 11 oveq2d โŠข ( ๐‘“ = ๐ท โ†’ ( -1R ยทR ( ๐ต ยทR ๐‘“ ) ) = ( -1R ยทR ( ๐ต ยทR ๐ท ) ) )
13 10 12 oveqan12d โŠข ( ( ๐‘ข = ๐ถ โˆง ๐‘“ = ๐ท ) โ†’ ( ( ๐ด ยทR ๐‘ข ) +R ( -1R ยทR ( ๐ต ยทR ๐‘“ ) ) ) = ( ( ๐ด ยทR ๐ถ ) +R ( -1R ยทR ( ๐ต ยทR ๐ท ) ) ) )
14 oveq2 โŠข ( ๐‘ข = ๐ถ โ†’ ( ๐ต ยทR ๐‘ข ) = ( ๐ต ยทR ๐ถ ) )
15 oveq2 โŠข ( ๐‘“ = ๐ท โ†’ ( ๐ด ยทR ๐‘“ ) = ( ๐ด ยทR ๐ท ) )
16 14 15 oveqan12d โŠข ( ( ๐‘ข = ๐ถ โˆง ๐‘“ = ๐ท ) โ†’ ( ( ๐ต ยทR ๐‘ข ) +R ( ๐ด ยทR ๐‘“ ) ) = ( ( ๐ต ยทR ๐ถ ) +R ( ๐ด ยทR ๐ท ) ) )
17 13 16 opeq12d โŠข ( ( ๐‘ข = ๐ถ โˆง ๐‘“ = ๐ท ) โ†’ โŸจ ( ( ๐ด ยทR ๐‘ข ) +R ( -1R ยทR ( ๐ต ยทR ๐‘“ ) ) ) , ( ( ๐ต ยทR ๐‘ข ) +R ( ๐ด ยทR ๐‘“ ) ) โŸฉ = โŸจ ( ( ๐ด ยทR ๐ถ ) +R ( -1R ยทR ( ๐ต ยทR ๐ท ) ) ) , ( ( ๐ต ยทR ๐ถ ) +R ( ๐ด ยทR ๐ท ) ) โŸฉ )
18 9 17 sylan9eq โŠข ( ( ( ๐‘ค = ๐ด โˆง ๐‘ฃ = ๐ต ) โˆง ( ๐‘ข = ๐ถ โˆง ๐‘“ = ๐ท ) ) โ†’ โŸจ ( ( ๐‘ค ยทR ๐‘ข ) +R ( -1R ยทR ( ๐‘ฃ ยทR ๐‘“ ) ) ) , ( ( ๐‘ฃ ยทR ๐‘ข ) +R ( ๐‘ค ยทR ๐‘“ ) ) โŸฉ = โŸจ ( ( ๐ด ยทR ๐ถ ) +R ( -1R ยทR ( ๐ต ยทR ๐ท ) ) ) , ( ( ๐ต ยทR ๐ถ ) +R ( ๐ด ยทR ๐ท ) ) โŸฉ )
19 df-mul โŠข ยท = { โŸจ โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ , ๐‘ง โŸฉ โˆฃ ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง โˆƒ ๐‘ค โˆƒ ๐‘ฃ โˆƒ ๐‘ข โˆƒ ๐‘“ ( ( ๐‘ฅ = โŸจ ๐‘ค , ๐‘ฃ โŸฉ โˆง ๐‘ฆ = โŸจ ๐‘ข , ๐‘“ โŸฉ ) โˆง ๐‘ง = โŸจ ( ( ๐‘ค ยทR ๐‘ข ) +R ( -1R ยทR ( ๐‘ฃ ยทR ๐‘“ ) ) ) , ( ( ๐‘ฃ ยทR ๐‘ข ) +R ( ๐‘ค ยทR ๐‘“ ) ) โŸฉ ) ) }
20 df-c โŠข โ„‚ = ( R ร— R )
21 20 eleq2i โŠข ( ๐‘ฅ โˆˆ โ„‚ โ†” ๐‘ฅ โˆˆ ( R ร— R ) )
22 20 eleq2i โŠข ( ๐‘ฆ โˆˆ โ„‚ โ†” ๐‘ฆ โˆˆ ( R ร— R ) )
23 21 22 anbi12i โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โ†” ( ๐‘ฅ โˆˆ ( R ร— R ) โˆง ๐‘ฆ โˆˆ ( R ร— R ) ) )
24 23 anbi1i โŠข ( ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง โˆƒ ๐‘ค โˆƒ ๐‘ฃ โˆƒ ๐‘ข โˆƒ ๐‘“ ( ( ๐‘ฅ = โŸจ ๐‘ค , ๐‘ฃ โŸฉ โˆง ๐‘ฆ = โŸจ ๐‘ข , ๐‘“ โŸฉ ) โˆง ๐‘ง = โŸจ ( ( ๐‘ค ยทR ๐‘ข ) +R ( -1R ยทR ( ๐‘ฃ ยทR ๐‘“ ) ) ) , ( ( ๐‘ฃ ยทR ๐‘ข ) +R ( ๐‘ค ยทR ๐‘“ ) ) โŸฉ ) ) โ†” ( ( ๐‘ฅ โˆˆ ( R ร— R ) โˆง ๐‘ฆ โˆˆ ( R ร— R ) ) โˆง โˆƒ ๐‘ค โˆƒ ๐‘ฃ โˆƒ ๐‘ข โˆƒ ๐‘“ ( ( ๐‘ฅ = โŸจ ๐‘ค , ๐‘ฃ โŸฉ โˆง ๐‘ฆ = โŸจ ๐‘ข , ๐‘“ โŸฉ ) โˆง ๐‘ง = โŸจ ( ( ๐‘ค ยทR ๐‘ข ) +R ( -1R ยทR ( ๐‘ฃ ยทR ๐‘“ ) ) ) , ( ( ๐‘ฃ ยทR ๐‘ข ) +R ( ๐‘ค ยทR ๐‘“ ) ) โŸฉ ) ) )
25 24 oprabbii โŠข { โŸจ โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ , ๐‘ง โŸฉ โˆฃ ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง โˆƒ ๐‘ค โˆƒ ๐‘ฃ โˆƒ ๐‘ข โˆƒ ๐‘“ ( ( ๐‘ฅ = โŸจ ๐‘ค , ๐‘ฃ โŸฉ โˆง ๐‘ฆ = โŸจ ๐‘ข , ๐‘“ โŸฉ ) โˆง ๐‘ง = โŸจ ( ( ๐‘ค ยทR ๐‘ข ) +R ( -1R ยทR ( ๐‘ฃ ยทR ๐‘“ ) ) ) , ( ( ๐‘ฃ ยทR ๐‘ข ) +R ( ๐‘ค ยทR ๐‘“ ) ) โŸฉ ) ) } = { โŸจ โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ , ๐‘ง โŸฉ โˆฃ ( ( ๐‘ฅ โˆˆ ( R ร— R ) โˆง ๐‘ฆ โˆˆ ( R ร— R ) ) โˆง โˆƒ ๐‘ค โˆƒ ๐‘ฃ โˆƒ ๐‘ข โˆƒ ๐‘“ ( ( ๐‘ฅ = โŸจ ๐‘ค , ๐‘ฃ โŸฉ โˆง ๐‘ฆ = โŸจ ๐‘ข , ๐‘“ โŸฉ ) โˆง ๐‘ง = โŸจ ( ( ๐‘ค ยทR ๐‘ข ) +R ( -1R ยทR ( ๐‘ฃ ยทR ๐‘“ ) ) ) , ( ( ๐‘ฃ ยทR ๐‘ข ) +R ( ๐‘ค ยทR ๐‘“ ) ) โŸฉ ) ) }
26 19 25 eqtri โŠข ยท = { โŸจ โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ , ๐‘ง โŸฉ โˆฃ ( ( ๐‘ฅ โˆˆ ( R ร— R ) โˆง ๐‘ฆ โˆˆ ( R ร— R ) ) โˆง โˆƒ ๐‘ค โˆƒ ๐‘ฃ โˆƒ ๐‘ข โˆƒ ๐‘“ ( ( ๐‘ฅ = โŸจ ๐‘ค , ๐‘ฃ โŸฉ โˆง ๐‘ฆ = โŸจ ๐‘ข , ๐‘“ โŸฉ ) โˆง ๐‘ง = โŸจ ( ( ๐‘ค ยทR ๐‘ข ) +R ( -1R ยทR ( ๐‘ฃ ยทR ๐‘“ ) ) ) , ( ( ๐‘ฃ ยทR ๐‘ข ) +R ( ๐‘ค ยทR ๐‘“ ) ) โŸฉ ) ) }
27 1 18 26 ov3 โŠข ( ( ( ๐ด โˆˆ R โˆง ๐ต โˆˆ R ) โˆง ( ๐ถ โˆˆ R โˆง ๐ท โˆˆ R ) ) โ†’ ( โŸจ ๐ด , ๐ต โŸฉ ยท โŸจ ๐ถ , ๐ท โŸฉ ) = โŸจ ( ( ๐ด ยทR ๐ถ ) +R ( -1R ยทR ( ๐ต ยทR ๐ท ) ) ) , ( ( ๐ต ยทR ๐ถ ) +R ( ๐ด ยทR ๐ท ) ) โŸฉ )