Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mendval Structured version   Visualization version   GIF version

Theorem mendval 37269
Description: Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
Hypotheses
Ref Expression
mendval.b 𝐵 = (𝑀 LMHom 𝑀)
mendval.p + = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥𝑓 (+g𝑀)𝑦))
mendval.t × = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥𝑦))
mendval.s 𝑆 = (Scalar‘𝑀)
mendval.v · = (𝑥 ∈ (Base‘𝑆), 𝑦𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 ( ·𝑠𝑀)𝑦))
Assertion
Ref Expression
mendval (𝑀𝑋 → (MEndo‘𝑀) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝑀,𝑦
Allowed substitution hints:   + (𝑥,𝑦)   𝑆(𝑥,𝑦)   · (𝑥,𝑦)   × (𝑥,𝑦)   𝑋(𝑥,𝑦)

Proof of Theorem mendval
Dummy variables 𝑚 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3201 . 2 (𝑀𝑋𝑀 ∈ V)
2 oveq12 6619 . . . . . . 7 ((𝑚 = 𝑀𝑚 = 𝑀) → (𝑚 LMHom 𝑚) = (𝑀 LMHom 𝑀))
32anidms 676 . . . . . 6 (𝑚 = 𝑀 → (𝑚 LMHom 𝑚) = (𝑀 LMHom 𝑀))
4 mendval.b . . . . . 6 𝐵 = (𝑀 LMHom 𝑀)
53, 4syl6eqr 2673 . . . . 5 (𝑚 = 𝑀 → (𝑚 LMHom 𝑚) = 𝐵)
65csbeq1d 3525 . . . 4 (𝑚 = 𝑀(𝑚 LMHom 𝑚) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩}) = 𝐵 / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩}))
7 ovex 6638 . . . . . 6 (𝑚 LMHom 𝑚) ∈ V
85, 7syl6eqelr 2707 . . . . 5 (𝑚 = 𝑀𝐵 ∈ V)
9 simpr 477 . . . . . . . 8 ((𝑚 = 𝑀𝑏 = 𝐵) → 𝑏 = 𝐵)
109opeq2d 4382 . . . . . . 7 ((𝑚 = 𝑀𝑏 = 𝐵) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
11 fveq2 6153 . . . . . . . . . . . 12 (𝑚 = 𝑀 → (+g𝑚) = (+g𝑀))
12 ofeq 6859 . . . . . . . . . . . 12 ((+g𝑚) = (+g𝑀) → ∘𝑓 (+g𝑚) = ∘𝑓 (+g𝑀))
1311, 12syl 17 . . . . . . . . . . 11 (𝑚 = 𝑀 → ∘𝑓 (+g𝑚) = ∘𝑓 (+g𝑀))
1413oveqdr 6634 . . . . . . . . . 10 ((𝑚 = 𝑀𝑏 = 𝐵) → (𝑥𝑓 (+g𝑚)𝑦) = (𝑥𝑓 (+g𝑀)𝑦))
159, 9, 14mpt2eq123dv 6677 . . . . . . . . 9 ((𝑚 = 𝑀𝑏 = 𝐵) → (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦)) = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥𝑓 (+g𝑀)𝑦)))
16 mendval.p . . . . . . . . 9 + = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥𝑓 (+g𝑀)𝑦))
1715, 16syl6eqr 2673 . . . . . . . 8 ((𝑚 = 𝑀𝑏 = 𝐵) → (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦)) = + )
1817opeq2d 4382 . . . . . . 7 ((𝑚 = 𝑀𝑏 = 𝐵) → ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩ = ⟨(+g‘ndx), + ⟩)
19 eqidd 2622 . . . . . . . . . 10 ((𝑚 = 𝑀𝑏 = 𝐵) → (𝑥𝑦) = (𝑥𝑦))
209, 9, 19mpt2eq123dv 6677 . . . . . . . . 9 ((𝑚 = 𝑀𝑏 = 𝐵) → (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦)) = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥𝑦)))
21 mendval.t . . . . . . . . 9 × = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥𝑦))
2220, 21syl6eqr 2673 . . . . . . . 8 ((𝑚 = 𝑀𝑏 = 𝐵) → (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦)) = × )
2322opeq2d 4382 . . . . . . 7 ((𝑚 = 𝑀𝑏 = 𝐵) → ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩ = ⟨(.r‘ndx), × ⟩)
2410, 18, 23tpeq123d 4258 . . . . . 6 ((𝑚 = 𝑀𝑏 = 𝐵) → {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩})
25 fveq2 6153 . . . . . . . . . 10 (𝑚 = 𝑀 → (Scalar‘𝑚) = (Scalar‘𝑀))
2625adantr 481 . . . . . . . . 9 ((𝑚 = 𝑀𝑏 = 𝐵) → (Scalar‘𝑚) = (Scalar‘𝑀))
27 mendval.s . . . . . . . . 9 𝑆 = (Scalar‘𝑀)
2826, 27syl6eqr 2673 . . . . . . . 8 ((𝑚 = 𝑀𝑏 = 𝐵) → (Scalar‘𝑚) = 𝑆)
2928opeq2d 4382 . . . . . . 7 ((𝑚 = 𝑀𝑏 = 𝐵) → ⟨(Scalar‘ndx), (Scalar‘𝑚)⟩ = ⟨(Scalar‘ndx), 𝑆⟩)
3028fveq2d 6157 . . . . . . . . . 10 ((𝑚 = 𝑀𝑏 = 𝐵) → (Base‘(Scalar‘𝑚)) = (Base‘𝑆))
31 fveq2 6153 . . . . . . . . . . . . 13 (𝑚 = 𝑀 → ( ·𝑠𝑚) = ( ·𝑠𝑀))
3231adantr 481 . . . . . . . . . . . 12 ((𝑚 = 𝑀𝑏 = 𝐵) → ( ·𝑠𝑚) = ( ·𝑠𝑀))
33 ofeq 6859 . . . . . . . . . . . 12 (( ·𝑠𝑚) = ( ·𝑠𝑀) → ∘𝑓 ( ·𝑠𝑚) = ∘𝑓 ( ·𝑠𝑀))
3432, 33syl 17 . . . . . . . . . . 11 ((𝑚 = 𝑀𝑏 = 𝐵) → ∘𝑓 ( ·𝑠𝑚) = ∘𝑓 ( ·𝑠𝑀))
35 fveq2 6153 . . . . . . . . . . . . 13 (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀))
3635adantr 481 . . . . . . . . . . . 12 ((𝑚 = 𝑀𝑏 = 𝐵) → (Base‘𝑚) = (Base‘𝑀))
3736xpeq1d 5103 . . . . . . . . . . 11 ((𝑚 = 𝑀𝑏 = 𝐵) → ((Base‘𝑚) × {𝑥}) = ((Base‘𝑀) × {𝑥}))
38 eqidd 2622 . . . . . . . . . . 11 ((𝑚 = 𝑀𝑏 = 𝐵) → 𝑦 = 𝑦)
3934, 37, 38oveq123d 6631 . . . . . . . . . 10 ((𝑚 = 𝑀𝑏 = 𝐵) → (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦) = (((Base‘𝑀) × {𝑥}) ∘𝑓 ( ·𝑠𝑀)𝑦))
4030, 9, 39mpt2eq123dv 6677 . . . . . . . . 9 ((𝑚 = 𝑀𝑏 = 𝐵) → (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦)) = (𝑥 ∈ (Base‘𝑆), 𝑦𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 ( ·𝑠𝑀)𝑦)))
41 mendval.v . . . . . . . . 9 · = (𝑥 ∈ (Base‘𝑆), 𝑦𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 ( ·𝑠𝑀)𝑦))
4240, 41syl6eqr 2673 . . . . . . . 8 ((𝑚 = 𝑀𝑏 = 𝐵) → (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦)) = · )
4342opeq2d 4382 . . . . . . 7 ((𝑚 = 𝑀𝑏 = 𝐵) → ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩ = ⟨( ·𝑠 ‘ndx), · ⟩)
4429, 43preq12d 4251 . . . . . 6 ((𝑚 = 𝑀𝑏 = 𝐵) → {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩} = {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩})
4524, 44uneq12d 3751 . . . . 5 ((𝑚 = 𝑀𝑏 = 𝐵) → ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))
468, 45csbied 3545 . . . 4 (𝑚 = 𝑀𝐵 / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))
476, 46eqtrd 2655 . . 3 (𝑚 = 𝑀(𝑚 LMHom 𝑚) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))
48 df-mend 37262 . . 3 MEndo = (𝑚 ∈ V ↦ (𝑚 LMHom 𝑚) / 𝑏({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑓 (+g𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠𝑚)𝑦))⟩}))
49 tpex 6917 . . . 4 {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
50 prex 4875 . . . 4 {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩} ∈ V
5149, 50unex 6916 . . 3 ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}) ∈ V
5247, 48, 51fvmpt 6244 . 2 (𝑀 ∈ V → (MEndo‘𝑀) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))
531, 52syl 17 1 (𝑀𝑋 → (MEndo‘𝑀) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  Vcvv 3189  csb 3518  cun 3557  {csn 4153  {cpr 4155  {ctp 4157  cop 4159   × cxp 5077  ccom 5083  cfv 5852  (class class class)co 6610  cmpt2 6612  𝑓 cof 6855  ndxcnx 15789  Basecbs 15792  +gcplusg 15873  .rcmulr 15874  Scalarcsca 15876   ·𝑠 cvsca 15877   LMHom clmhm 18951  MEndocmend 37261
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-iota 5815  df-fun 5854  df-fv 5860  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-mend 37262
This theorem is referenced by:  mendbas  37270  mendplusgfval  37271  mendmulrfval  37273  mendsca  37275  mendvscafval  37276
  Copyright terms: Public domain W3C validator