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

Theorem scmatval 20586
Description: The set of 𝑁 x 𝑁 scalar matrices over (a ring) 𝑅. (Contributed by AV, 18-Dec-2019.)
Hypotheses
Ref Expression
scmatval.k 𝐾 = (Base‘𝑅)
scmatval.a 𝐴 = (𝑁 Mat 𝑅)
scmatval.b 𝐵 = (Base‘𝐴)
scmatval.1 1 = (1r𝐴)
scmatval.t · = ( ·𝑠𝐴)
scmatval.s 𝑆 = (𝑁 ScMat 𝑅)
Assertion
Ref Expression
scmatval ((𝑁 ∈ Fin ∧ 𝑅𝑉) → 𝑆 = {𝑚𝐵 ∣ ∃𝑐𝐾 𝑚 = (𝑐 · 1 )})
Distinct variable groups:   𝐵,𝑚   𝐾,𝑐   𝑁,𝑐,𝑚   𝑅,𝑐,𝑚
Allowed substitution hints:   𝐴(𝑚,𝑐)   𝐵(𝑐)   𝑆(𝑚,𝑐)   · (𝑚,𝑐)   1 (𝑚,𝑐)   𝐾(𝑚)   𝑉(𝑚,𝑐)

Proof of Theorem scmatval
Dummy variables 𝑛 𝑟 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 scmatval.s . 2 𝑆 = (𝑁 ScMat 𝑅)
2 df-scmat 20573 . . . 4 ScMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑛 Mat 𝑟) / 𝑎{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))})
32a1i 11 . . 3 ((𝑁 ∈ Fin ∧ 𝑅𝑉) → ScMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑛 Mat 𝑟) / 𝑎{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))}))
4 ovexd 6875 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅𝑉) ∧ (𝑛 = 𝑁𝑟 = 𝑅)) → (𝑛 Mat 𝑟) ∈ V)
5 fveq2 6374 . . . . . . 7 (𝑎 = (𝑛 Mat 𝑟) → (Base‘𝑎) = (Base‘(𝑛 Mat 𝑟)))
6 fveq2 6374 . . . . . . . . . 10 (𝑎 = (𝑛 Mat 𝑟) → ( ·𝑠𝑎) = ( ·𝑠 ‘(𝑛 Mat 𝑟)))
7 eqidd 2765 . . . . . . . . . 10 (𝑎 = (𝑛 Mat 𝑟) → 𝑐 = 𝑐)
8 fveq2 6374 . . . . . . . . . 10 (𝑎 = (𝑛 Mat 𝑟) → (1r𝑎) = (1r‘(𝑛 Mat 𝑟)))
96, 7, 8oveq123d 6862 . . . . . . . . 9 (𝑎 = (𝑛 Mat 𝑟) → (𝑐( ·𝑠𝑎)(1r𝑎)) = (𝑐( ·𝑠 ‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟))))
109eqeq2d 2774 . . . . . . . 8 (𝑎 = (𝑛 Mat 𝑟) → (𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎)) ↔ 𝑚 = (𝑐( ·𝑠 ‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))))
1110rexbidv 3198 . . . . . . 7 (𝑎 = (𝑛 Mat 𝑟) → (∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎)) ↔ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))))
125, 11rabeqbidv 3343 . . . . . 6 (𝑎 = (𝑛 Mat 𝑟) → {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))} = {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))})
1312adantl 473 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅𝑉) ∧ (𝑛 = 𝑁𝑟 = 𝑅)) ∧ 𝑎 = (𝑛 Mat 𝑟)) → {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))} = {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))})
144, 13csbied 3717 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅𝑉) ∧ (𝑛 = 𝑁𝑟 = 𝑅)) → (𝑛 Mat 𝑟) / 𝑎{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))} = {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))})
15 oveq12 6850 . . . . . . . 8 ((𝑛 = 𝑁𝑟 = 𝑅) → (𝑛 Mat 𝑟) = (𝑁 Mat 𝑅))
1615fveq2d 6378 . . . . . . 7 ((𝑛 = 𝑁𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = (Base‘(𝑁 Mat 𝑅)))
17 scmatval.b . . . . . . . 8 𝐵 = (Base‘𝐴)
18 scmatval.a . . . . . . . . 9 𝐴 = (𝑁 Mat 𝑅)
1918fveq2i 6377 . . . . . . . 8 (Base‘𝐴) = (Base‘(𝑁 Mat 𝑅))
2017, 19eqtri 2786 . . . . . . 7 𝐵 = (Base‘(𝑁 Mat 𝑅))
2116, 20syl6eqr 2816 . . . . . 6 ((𝑛 = 𝑁𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = 𝐵)
22 fveq2 6374 . . . . . . . . 9 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
23 scmatval.k . . . . . . . . 9 𝐾 = (Base‘𝑅)
2422, 23syl6eqr 2816 . . . . . . . 8 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐾)
2524adantl 473 . . . . . . 7 ((𝑛 = 𝑁𝑟 = 𝑅) → (Base‘𝑟) = 𝐾)
2615fveq2d 6378 . . . . . . . . . 10 ((𝑛 = 𝑁𝑟 = 𝑅) → ( ·𝑠 ‘(𝑛 Mat 𝑟)) = ( ·𝑠 ‘(𝑁 Mat 𝑅)))
27 scmatval.t . . . . . . . . . . 11 · = ( ·𝑠𝐴)
2818fveq2i 6377 . . . . . . . . . . 11 ( ·𝑠𝐴) = ( ·𝑠 ‘(𝑁 Mat 𝑅))
2927, 28eqtri 2786 . . . . . . . . . 10 · = ( ·𝑠 ‘(𝑁 Mat 𝑅))
3026, 29syl6eqr 2816 . . . . . . . . 9 ((𝑛 = 𝑁𝑟 = 𝑅) → ( ·𝑠 ‘(𝑛 Mat 𝑟)) = · )
31 eqidd 2765 . . . . . . . . 9 ((𝑛 = 𝑁𝑟 = 𝑅) → 𝑐 = 𝑐)
3215fveq2d 6378 . . . . . . . . . 10 ((𝑛 = 𝑁𝑟 = 𝑅) → (1r‘(𝑛 Mat 𝑟)) = (1r‘(𝑁 Mat 𝑅)))
33 scmatval.1 . . . . . . . . . . 11 1 = (1r𝐴)
3418fveq2i 6377 . . . . . . . . . . 11 (1r𝐴) = (1r‘(𝑁 Mat 𝑅))
3533, 34eqtri 2786 . . . . . . . . . 10 1 = (1r‘(𝑁 Mat 𝑅))
3632, 35syl6eqr 2816 . . . . . . . . 9 ((𝑛 = 𝑁𝑟 = 𝑅) → (1r‘(𝑛 Mat 𝑟)) = 1 )
3730, 31, 36oveq123d 6862 . . . . . . . 8 ((𝑛 = 𝑁𝑟 = 𝑅) → (𝑐( ·𝑠 ‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟))) = (𝑐 · 1 ))
3837eqeq2d 2774 . . . . . . 7 ((𝑛 = 𝑁𝑟 = 𝑅) → (𝑚 = (𝑐( ·𝑠 ‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟))) ↔ 𝑚 = (𝑐 · 1 )))
3925, 38rexeqbidv 3300 . . . . . 6 ((𝑛 = 𝑁𝑟 = 𝑅) → (∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟))) ↔ ∃𝑐𝐾 𝑚 = (𝑐 · 1 )))
4021, 39rabeqbidv 3343 . . . . 5 ((𝑛 = 𝑁𝑟 = 𝑅) → {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))} = {𝑚𝐵 ∣ ∃𝑐𝐾 𝑚 = (𝑐 · 1 )})
4140adantl 473 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅𝑉) ∧ (𝑛 = 𝑁𝑟 = 𝑅)) → {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))} = {𝑚𝐵 ∣ ∃𝑐𝐾 𝑚 = (𝑐 · 1 )})
4214, 41eqtrd 2798 . . 3 (((𝑁 ∈ Fin ∧ 𝑅𝑉) ∧ (𝑛 = 𝑁𝑟 = 𝑅)) → (𝑛 Mat 𝑟) / 𝑎{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))} = {𝑚𝐵 ∣ ∃𝑐𝐾 𝑚 = (𝑐 · 1 )})
43 simpl 474 . . 3 ((𝑁 ∈ Fin ∧ 𝑅𝑉) → 𝑁 ∈ Fin)
44 elex 3364 . . . 4 (𝑅𝑉𝑅 ∈ V)
4544adantl 473 . . 3 ((𝑁 ∈ Fin ∧ 𝑅𝑉) → 𝑅 ∈ V)
4617fvexi 6388 . . . . 5 𝐵 ∈ V
4746rabex 4972 . . . 4 {𝑚𝐵 ∣ ∃𝑐𝐾 𝑚 = (𝑐 · 1 )} ∈ V
4847a1i 11 . . 3 ((𝑁 ∈ Fin ∧ 𝑅𝑉) → {𝑚𝐵 ∣ ∃𝑐𝐾 𝑚 = (𝑐 · 1 )} ∈ V)
493, 42, 43, 45, 48ovmpt2d 6985 . 2 ((𝑁 ∈ Fin ∧ 𝑅𝑉) → (𝑁 ScMat 𝑅) = {𝑚𝐵 ∣ ∃𝑐𝐾 𝑚 = (𝑐 · 1 )})
501, 49syl5eq 2810 1 ((𝑁 ∈ Fin ∧ 𝑅𝑉) → 𝑆 = {𝑚𝐵 ∣ ∃𝑐𝐾 𝑚 = (𝑐 · 1 )})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  wrex 3055  {crab 3058  Vcvv 3349  csb 3690  cfv 6067  (class class class)co 6841  cmpt2 6843  Fincfn 8159  Basecbs 16131   ·𝑠 cvsca 16219  1rcur 18767   Mat cmat 20488   ScMat cscmat 20571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pr 5061
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-br 4809  df-opab 4871  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-iota 6030  df-fun 6069  df-fv 6075  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-scmat 20573
This theorem is referenced by:  scmatel  20587  scmatmats  20593  scmatlss  20607
  Copyright terms: Public domain W3C validator