MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vcass Structured version   Visualization version   GIF version

Theorem vcass 30370
Description: Associative law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
vciOLD.1 ๐บ = (1st โ€˜๐‘Š)
vciOLD.2 ๐‘† = (2nd โ€˜๐‘Š)
vciOLD.3 ๐‘‹ = ran ๐บ
Assertion
Ref Expression
vcass ((๐‘Š โˆˆ CVecOLD โˆง (๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ ๐‘‹)) โ†’ ((๐ด ยท ๐ต)๐‘†๐ถ) = (๐ด๐‘†(๐ต๐‘†๐ถ)))

Proof of Theorem vcass
Dummy variables ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vciOLD.1 . . . . . 6 ๐บ = (1st โ€˜๐‘Š)
2 vciOLD.2 . . . . . 6 ๐‘† = (2nd โ€˜๐‘Š)
3 vciOLD.3 . . . . . 6 ๐‘‹ = ran ๐บ
41, 2, 3vciOLD 30364 . . . . 5 (๐‘Š โˆˆ CVecOLD โ†’ (๐บ โˆˆ AbelOp โˆง ๐‘†:(โ„‚ ร— ๐‘‹)โŸถ๐‘‹ โˆง โˆ€๐‘ฅ โˆˆ ๐‘‹ ((1๐‘†๐‘ฅ) = ๐‘ฅ โˆง โˆ€๐‘ฆ โˆˆ โ„‚ (โˆ€๐‘ง โˆˆ ๐‘‹ (๐‘ฆ๐‘†(๐‘ฅ๐บ๐‘ง)) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ฆ๐‘†๐‘ง)) โˆง โˆ€๐‘ง โˆˆ โ„‚ (((๐‘ฆ + ๐‘ง)๐‘†๐‘ฅ) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ง๐‘†๐‘ฅ)) โˆง ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)))))))
5 simpr 484 . . . . . . . . . . 11 ((((๐‘ฆ + ๐‘ง)๐‘†๐‘ฅ) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ง๐‘†๐‘ฅ)) โˆง ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ))) โ†’ ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)))
65ralimi 3079 . . . . . . . . . 10 (โˆ€๐‘ง โˆˆ โ„‚ (((๐‘ฆ + ๐‘ง)๐‘†๐‘ฅ) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ง๐‘†๐‘ฅ)) โˆง ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ))) โ†’ โˆ€๐‘ง โˆˆ โ„‚ ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)))
76adantl 481 . . . . . . . . 9 ((โˆ€๐‘ง โˆˆ ๐‘‹ (๐‘ฆ๐‘†(๐‘ฅ๐บ๐‘ง)) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ฆ๐‘†๐‘ง)) โˆง โˆ€๐‘ง โˆˆ โ„‚ (((๐‘ฆ + ๐‘ง)๐‘†๐‘ฅ) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ง๐‘†๐‘ฅ)) โˆง ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)))) โ†’ โˆ€๐‘ง โˆˆ โ„‚ ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)))
87ralimi 3079 . . . . . . . 8 (โˆ€๐‘ฆ โˆˆ โ„‚ (โˆ€๐‘ง โˆˆ ๐‘‹ (๐‘ฆ๐‘†(๐‘ฅ๐บ๐‘ง)) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ฆ๐‘†๐‘ง)) โˆง โˆ€๐‘ง โˆˆ โ„‚ (((๐‘ฆ + ๐‘ง)๐‘†๐‘ฅ) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ง๐‘†๐‘ฅ)) โˆง ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)))) โ†’ โˆ€๐‘ฆ โˆˆ โ„‚ โˆ€๐‘ง โˆˆ โ„‚ ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)))
98adantl 481 . . . . . . 7 (((1๐‘†๐‘ฅ) = ๐‘ฅ โˆง โˆ€๐‘ฆ โˆˆ โ„‚ (โˆ€๐‘ง โˆˆ ๐‘‹ (๐‘ฆ๐‘†(๐‘ฅ๐บ๐‘ง)) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ฆ๐‘†๐‘ง)) โˆง โˆ€๐‘ง โˆˆ โ„‚ (((๐‘ฆ + ๐‘ง)๐‘†๐‘ฅ) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ง๐‘†๐‘ฅ)) โˆง ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ))))) โ†’ โˆ€๐‘ฆ โˆˆ โ„‚ โˆ€๐‘ง โˆˆ โ„‚ ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)))
109ralimi 3079 . . . . . 6 (โˆ€๐‘ฅ โˆˆ ๐‘‹ ((1๐‘†๐‘ฅ) = ๐‘ฅ โˆง โˆ€๐‘ฆ โˆˆ โ„‚ (โˆ€๐‘ง โˆˆ ๐‘‹ (๐‘ฆ๐‘†(๐‘ฅ๐บ๐‘ง)) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ฆ๐‘†๐‘ง)) โˆง โˆ€๐‘ง โˆˆ โ„‚ (((๐‘ฆ + ๐‘ง)๐‘†๐‘ฅ) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ง๐‘†๐‘ฅ)) โˆง ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ))))) โ†’ โˆ€๐‘ฅ โˆˆ ๐‘‹ โˆ€๐‘ฆ โˆˆ โ„‚ โˆ€๐‘ง โˆˆ โ„‚ ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)))
11103ad2ant3 1133 . . . . 5 ((๐บ โˆˆ AbelOp โˆง ๐‘†:(โ„‚ ร— ๐‘‹)โŸถ๐‘‹ โˆง โˆ€๐‘ฅ โˆˆ ๐‘‹ ((1๐‘†๐‘ฅ) = ๐‘ฅ โˆง โˆ€๐‘ฆ โˆˆ โ„‚ (โˆ€๐‘ง โˆˆ ๐‘‹ (๐‘ฆ๐‘†(๐‘ฅ๐บ๐‘ง)) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ฆ๐‘†๐‘ง)) โˆง โˆ€๐‘ง โˆˆ โ„‚ (((๐‘ฆ + ๐‘ง)๐‘†๐‘ฅ) = ((๐‘ฆ๐‘†๐‘ฅ)๐บ(๐‘ง๐‘†๐‘ฅ)) โˆง ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)))))) โ†’ โˆ€๐‘ฅ โˆˆ ๐‘‹ โˆ€๐‘ฆ โˆˆ โ„‚ โˆ€๐‘ง โˆˆ โ„‚ ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)))
124, 11syl 17 . . . 4 (๐‘Š โˆˆ CVecOLD โ†’ โˆ€๐‘ฅ โˆˆ ๐‘‹ โˆ€๐‘ฆ โˆˆ โ„‚ โˆ€๐‘ง โˆˆ โ„‚ ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)))
13 oveq2 7422 . . . . . 6 (๐‘ฅ = ๐ถ โ†’ ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = ((๐‘ฆ ยท ๐‘ง)๐‘†๐ถ))
14 oveq2 7422 . . . . . . 7 (๐‘ฅ = ๐ถ โ†’ (๐‘ง๐‘†๐‘ฅ) = (๐‘ง๐‘†๐ถ))
1514oveq2d 7430 . . . . . 6 (๐‘ฅ = ๐ถ โ†’ (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐ถ)))
1613, 15eqeq12d 2744 . . . . 5 (๐‘ฅ = ๐ถ โ†’ (((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)) โ†” ((๐‘ฆ ยท ๐‘ง)๐‘†๐ถ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐ถ))))
17 oveq1 7421 . . . . . . 7 (๐‘ฆ = ๐ด โ†’ (๐‘ฆ ยท ๐‘ง) = (๐ด ยท ๐‘ง))
1817oveq1d 7429 . . . . . 6 (๐‘ฆ = ๐ด โ†’ ((๐‘ฆ ยท ๐‘ง)๐‘†๐ถ) = ((๐ด ยท ๐‘ง)๐‘†๐ถ))
19 oveq1 7421 . . . . . 6 (๐‘ฆ = ๐ด โ†’ (๐‘ฆ๐‘†(๐‘ง๐‘†๐ถ)) = (๐ด๐‘†(๐‘ง๐‘†๐ถ)))
2018, 19eqeq12d 2744 . . . . 5 (๐‘ฆ = ๐ด โ†’ (((๐‘ฆ ยท ๐‘ง)๐‘†๐ถ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐ถ)) โ†” ((๐ด ยท ๐‘ง)๐‘†๐ถ) = (๐ด๐‘†(๐‘ง๐‘†๐ถ))))
21 oveq2 7422 . . . . . . 7 (๐‘ง = ๐ต โ†’ (๐ด ยท ๐‘ง) = (๐ด ยท ๐ต))
2221oveq1d 7429 . . . . . 6 (๐‘ง = ๐ต โ†’ ((๐ด ยท ๐‘ง)๐‘†๐ถ) = ((๐ด ยท ๐ต)๐‘†๐ถ))
23 oveq1 7421 . . . . . . 7 (๐‘ง = ๐ต โ†’ (๐‘ง๐‘†๐ถ) = (๐ต๐‘†๐ถ))
2423oveq2d 7430 . . . . . 6 (๐‘ง = ๐ต โ†’ (๐ด๐‘†(๐‘ง๐‘†๐ถ)) = (๐ด๐‘†(๐ต๐‘†๐ถ)))
2522, 24eqeq12d 2744 . . . . 5 (๐‘ง = ๐ต โ†’ (((๐ด ยท ๐‘ง)๐‘†๐ถ) = (๐ด๐‘†(๐‘ง๐‘†๐ถ)) โ†” ((๐ด ยท ๐ต)๐‘†๐ถ) = (๐ด๐‘†(๐ต๐‘†๐ถ))))
2616, 20, 25rspc3v 3624 . . . 4 ((๐ถ โˆˆ ๐‘‹ โˆง ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (โˆ€๐‘ฅ โˆˆ ๐‘‹ โˆ€๐‘ฆ โˆˆ โ„‚ โˆ€๐‘ง โˆˆ โ„‚ ((๐‘ฆ ยท ๐‘ง)๐‘†๐‘ฅ) = (๐‘ฆ๐‘†(๐‘ง๐‘†๐‘ฅ)) โ†’ ((๐ด ยท ๐ต)๐‘†๐ถ) = (๐ด๐‘†(๐ต๐‘†๐ถ))))
2712, 26syl5 34 . . 3 ((๐ถ โˆˆ ๐‘‹ โˆง ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐‘Š โˆˆ CVecOLD โ†’ ((๐ด ยท ๐ต)๐‘†๐ถ) = (๐ด๐‘†(๐ต๐‘†๐ถ))))
28273coml 1125 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ ๐‘‹) โ†’ (๐‘Š โˆˆ CVecOLD โ†’ ((๐ด ยท ๐ต)๐‘†๐ถ) = (๐ด๐‘†(๐ต๐‘†๐ถ))))
2928impcom 407 1 ((๐‘Š โˆˆ CVecOLD โˆง (๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ ๐‘‹)) โ†’ ((๐ด ยท ๐ต)๐‘†๐ถ) = (๐ด๐‘†(๐ต๐‘†๐ถ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   โˆง w3a 1085   = wceq 1534   โˆˆ wcel 2099  โˆ€wral 3057   ร— cxp 5670  ran crn 5673  โŸถwf 6538  โ€˜cfv 6542  (class class class)co 7414  1st c1st 7985  2nd c2nd 7986  โ„‚cc 11130  1c1 11133   + caddc 11135   ยท cmul 11137  AbelOpcablo 30347  CVecOLDcvc 30361
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7417  df-1st 7987  df-2nd 7988  df-vc 30362
This theorem is referenced by:  vcz  30378  nvsass  30431
  Copyright terms: Public domain W3C validator