MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sraval Structured version   Visualization version   GIF version
Theorem sraval 20733
Description: Lemma for srabase 20736 through sravsca 20744. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.)
Assertion
Ref Expression
sraval ((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) β†’ ((subringAlg β€˜π‘Š)β€˜π‘†) = (((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑆)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘Š)⟩))
Proof of Theorem sraval
Dummy variables 𝑠 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3488 . . . 4 (π‘Š ∈ 𝑉 β†’ π‘Š ∈ V)
21adantr 481 . . 3 ((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) β†’ π‘Š ∈ V)
3 fveq2 6875 . . . . . 6 (𝑀 = π‘Š β†’ (Baseβ€˜π‘€) = (Baseβ€˜π‘Š))
43pweqd 4610 . . . . 5 (𝑀 = π‘Š β†’ 𝒫 (Baseβ€˜π‘€) = 𝒫 (Baseβ€˜π‘Š))
5 id 22 . . . . . . . 8 (𝑀 = π‘Š β†’ 𝑀 = π‘Š)
6 oveq1 7397 . . . . . . . . 9 (𝑀 = π‘Š β†’ (𝑀 β†Ύs 𝑠) = (π‘Š β†Ύs 𝑠))
76opeq2d 4870 . . . . . . . 8 (𝑀 = π‘Š β†’ ⟨(Scalarβ€˜ndx), (𝑀 β†Ύs 𝑠)⟩ = ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑠)⟩)
85, 7oveq12d 7408 . . . . . . 7 (𝑀 = π‘Š β†’ (𝑀 sSet ⟨(Scalarβ€˜ndx), (𝑀 β†Ύs 𝑠)⟩) = (π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑠)⟩))
9 fveq2 6875 . . . . . . . 8 (𝑀 = π‘Š β†’ (.rβ€˜π‘€) = (.rβ€˜π‘Š))
109opeq2d 4870 . . . . . . 7 (𝑀 = π‘Š β†’ ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘€)⟩ = ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩)
118, 10oveq12d 7408 . . . . . 6 (𝑀 = π‘Š β†’ ((𝑀 sSet ⟨(Scalarβ€˜ndx), (𝑀 β†Ύs 𝑠)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘€)⟩) = ((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑠)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩))
129opeq2d 4870 . . . . . 6 (𝑀 = π‘Š β†’ ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘€)⟩ = ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘Š)⟩)
1311, 12oveq12d 7408 . . . . 5 (𝑀 = π‘Š β†’ (((𝑀 sSet ⟨(Scalarβ€˜ndx), (𝑀 β†Ύs 𝑠)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘€)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘€)⟩) = (((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑠)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘Š)⟩))
144, 13mpteq12dv 5229 . . . 4 (𝑀 = π‘Š β†’ (𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ↦ (((𝑀 sSet ⟨(Scalarβ€˜ndx), (𝑀 β†Ύs 𝑠)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘€)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘€)⟩)) = (𝑠 ∈ 𝒫 (Baseβ€˜π‘Š) ↦ (((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑠)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘Š)⟩)))
15 df-sra 20729 . . . 4 subringAlg = (𝑀 ∈ V ↦ (𝑠 ∈ 𝒫 (Baseβ€˜π‘€) ↦ (((𝑀 sSet ⟨(Scalarβ€˜ndx), (𝑀 β†Ύs 𝑠)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘€)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘€)⟩)))
16 fvex 6888 . . . . . 6 (Baseβ€˜π‘Š) ∈ V
1716pwex 5368 . . . . 5 𝒫 (Baseβ€˜π‘Š) ∈ V
1817mptex 7206 . . . 4 (𝑠 ∈ 𝒫 (Baseβ€˜π‘Š) ↦ (((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑠)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘Š)⟩)) ∈ V
1914, 15, 18fvmpt 6981 . . 3 (π‘Š ∈ V β†’ (subringAlg β€˜π‘Š) = (𝑠 ∈ 𝒫 (Baseβ€˜π‘Š) ↦ (((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑠)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘Š)⟩)))
202, 19syl 17 . 2 ((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) β†’ (subringAlg β€˜π‘Š) = (𝑠 ∈ 𝒫 (Baseβ€˜π‘Š) ↦ (((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑠)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘Š)⟩)))
21 simpr 485 . . . . . . 7 (((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) ∧ 𝑠 = 𝑆) β†’ 𝑠 = 𝑆)
2221oveq2d 7406 . . . . . 6 (((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) ∧ 𝑠 = 𝑆) β†’ (π‘Š β†Ύs 𝑠) = (π‘Š β†Ύs 𝑆))
2322opeq2d 4870 . . . . 5 (((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) ∧ 𝑠 = 𝑆) β†’ ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑠)⟩ = ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑆)⟩)
2423oveq2d 7406 . . . 4 (((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) ∧ 𝑠 = 𝑆) β†’ (π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑠)⟩) = (π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑆)⟩))
2524oveq1d 7405 . . 3 (((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) ∧ 𝑠 = 𝑆) β†’ ((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑠)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩) = ((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑆)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩))
2625oveq1d 7405 . 2 (((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) ∧ 𝑠 = 𝑆) β†’ (((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑠)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘Š)⟩) = (((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑆)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘Š)⟩))
27 simpr 485 . . 3 ((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) β†’ 𝑆 βŠ† (Baseβ€˜π‘Š))
2816elpw2 5335 . . 3 (𝑆 ∈ 𝒫 (Baseβ€˜π‘Š) ↔ 𝑆 βŠ† (Baseβ€˜π‘Š))
2927, 28sylibr 233 . 2 ((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) β†’ 𝑆 ∈ 𝒫 (Baseβ€˜π‘Š))
30 ovexd 7425 . 2 ((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) β†’ (((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑆)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘Š)⟩) ∈ V)
3120, 26, 29, 30fvmptd 6988 1 ((π‘Š ∈ 𝑉 ∧ 𝑆 βŠ† (Baseβ€˜π‘Š)) β†’ ((subringAlg β€˜π‘Š)β€˜π‘†) = (((π‘Š sSet ⟨(Scalarβ€˜ndx), (π‘Š β†Ύs 𝑆)⟩) sSet ⟨( ·𝑠 β€˜ndx), (.rβ€˜π‘Š)⟩) sSet ⟨(Β·π‘–β€˜ndx), (.rβ€˜π‘Š)⟩))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3470   βŠ† wss 3941  π’« cpw 4593  βŸ¨cop 4625   ↦ cmpt 5221  β€˜cfv 6529  (class class class)co 7390   sSet csts 17075  ndxcnx 17105  Basecbs 17123   β†Ύs cress 17152  .rcmulr 17177  Scalarcsca 17179   ·𝑠 cvsca 17180  Β·π‘–cip 17181  subringAlg csra 20725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3430  df-v 3472  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4520  df-pw 4595  df-sn 4620  df-pr 4622  df-op 4626  df-uni 4899  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6481  df-fun 6531  df-fn 6532  df-f 6533  df-f1 6534  df-fo 6535  df-f1o 6536  df-fv 6537  df-ov 7393  df-sra 20729
This theorem is referenced by:  sralem  20734  sralemOLD  20735  srasca  20742  srascaOLD  20743  sravsca  20744  sravscaOLD  20745  sraip  20746  rlmval2  20759
  Copyright terms: Public domain W3C validator