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

Theorem lmhmco 19791
Description: The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015.)
Assertion
Ref Expression
lmhmco ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹𝐺) ∈ (𝑀 LMHom 𝑂))

Proof of Theorem lmhmco
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2820 . 2 (Base‘𝑀) = (Base‘𝑀)
2 eqid 2820 . 2 ( ·𝑠𝑀) = ( ·𝑠𝑀)
3 eqid 2820 . 2 ( ·𝑠𝑂) = ( ·𝑠𝑂)
4 eqid 2820 . 2 (Scalar‘𝑀) = (Scalar‘𝑀)
5 eqid 2820 . 2 (Scalar‘𝑂) = (Scalar‘𝑂)
6 eqid 2820 . 2 (Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀))
7 lmhmlmod1 19781 . . 3 (𝐺 ∈ (𝑀 LMHom 𝑁) → 𝑀 ∈ LMod)
87adantl 484 . 2 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝑀 ∈ LMod)
9 lmhmlmod2 19780 . . 3 (𝐹 ∈ (𝑁 LMHom 𝑂) → 𝑂 ∈ LMod)
109adantr 483 . 2 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝑂 ∈ LMod)
11 eqid 2820 . . . 4 (Scalar‘𝑁) = (Scalar‘𝑁)
1211, 5lmhmsca 19778 . . 3 (𝐹 ∈ (𝑁 LMHom 𝑂) → (Scalar‘𝑂) = (Scalar‘𝑁))
134, 11lmhmsca 19778 . . 3 (𝐺 ∈ (𝑀 LMHom 𝑁) → (Scalar‘𝑁) = (Scalar‘𝑀))
1412, 13sylan9eq 2875 . 2 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (Scalar‘𝑂) = (Scalar‘𝑀))
15 lmghm 19779 . . 3 (𝐹 ∈ (𝑁 LMHom 𝑂) → 𝐹 ∈ (𝑁 GrpHom 𝑂))
16 lmghm 19779 . . 3 (𝐺 ∈ (𝑀 LMHom 𝑁) → 𝐺 ∈ (𝑀 GrpHom 𝑁))
17 ghmco 18357 . . 3 ((𝐹 ∈ (𝑁 GrpHom 𝑂) ∧ 𝐺 ∈ (𝑀 GrpHom 𝑁)) → (𝐹𝐺) ∈ (𝑀 GrpHom 𝑂))
1815, 16, 17syl2an 597 . 2 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹𝐺) ∈ (𝑀 GrpHom 𝑂))
19 simplr 767 . . . . . 6 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝐺 ∈ (𝑀 LMHom 𝑁))
20 simprl 769 . . . . . 6 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝑥 ∈ (Base‘(Scalar‘𝑀)))
21 simprr 771 . . . . . 6 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝑦 ∈ (Base‘𝑀))
22 eqid 2820 . . . . . . 7 ( ·𝑠𝑁) = ( ·𝑠𝑁)
234, 6, 1, 2, 22lmhmlin 19783 . . . . . 6 ((𝐺 ∈ (𝑀 LMHom 𝑁) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝐺‘(𝑥( ·𝑠𝑀)𝑦)) = (𝑥( ·𝑠𝑁)(𝐺𝑦)))
2419, 20, 21, 23syl3anc 1367 . . . . 5 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐺‘(𝑥( ·𝑠𝑀)𝑦)) = (𝑥( ·𝑠𝑁)(𝐺𝑦)))
2524fveq2d 6650 . . . 4 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐹‘(𝐺‘(𝑥( ·𝑠𝑀)𝑦))) = (𝐹‘(𝑥( ·𝑠𝑁)(𝐺𝑦))))
26 simpll 765 . . . . 5 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝐹 ∈ (𝑁 LMHom 𝑂))
2713fveq2d 6650 . . . . . . 7 (𝐺 ∈ (𝑀 LMHom 𝑁) → (Base‘(Scalar‘𝑁)) = (Base‘(Scalar‘𝑀)))
2827ad2antlr 725 . . . . . 6 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (Base‘(Scalar‘𝑁)) = (Base‘(Scalar‘𝑀)))
2920, 28eleqtrrd 2914 . . . . 5 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝑥 ∈ (Base‘(Scalar‘𝑁)))
30 eqid 2820 . . . . . . . . 9 (Base‘𝑁) = (Base‘𝑁)
311, 30lmhmf 19782 . . . . . . . 8 (𝐺 ∈ (𝑀 LMHom 𝑁) → 𝐺:(Base‘𝑀)⟶(Base‘𝑁))
3231adantl 484 . . . . . . 7 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝐺:(Base‘𝑀)⟶(Base‘𝑁))
3332ffvelrnda 6827 . . . . . 6 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝐺𝑦) ∈ (Base‘𝑁))
3433adantrl 714 . . . . 5 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐺𝑦) ∈ (Base‘𝑁))
35 eqid 2820 . . . . . 6 (Base‘(Scalar‘𝑁)) = (Base‘(Scalar‘𝑁))
3611, 35, 30, 22, 3lmhmlin 19783 . . . . 5 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑁)) ∧ (𝐺𝑦) ∈ (Base‘𝑁)) → (𝐹‘(𝑥( ·𝑠𝑁)(𝐺𝑦))) = (𝑥( ·𝑠𝑂)(𝐹‘(𝐺𝑦))))
3726, 29, 34, 36syl3anc 1367 . . . 4 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐹‘(𝑥( ·𝑠𝑁)(𝐺𝑦))) = (𝑥( ·𝑠𝑂)(𝐹‘(𝐺𝑦))))
3825, 37eqtrd 2855 . . 3 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐹‘(𝐺‘(𝑥( ·𝑠𝑀)𝑦))) = (𝑥( ·𝑠𝑂)(𝐹‘(𝐺𝑦))))
3932ffnd 6491 . . . 4 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝐺 Fn (Base‘𝑀))
407ad2antlr 725 . . . . 5 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝑀 ∈ LMod)
411, 4, 2, 6lmodvscl 19627 . . . . 5 ((𝑀 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝑥( ·𝑠𝑀)𝑦) ∈ (Base‘𝑀))
4240, 20, 21, 41syl3anc 1367 . . . 4 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝑥( ·𝑠𝑀)𝑦) ∈ (Base‘𝑀))
43 fvco2 6734 . . . 4 ((𝐺 Fn (Base‘𝑀) ∧ (𝑥( ·𝑠𝑀)𝑦) ∈ (Base‘𝑀)) → ((𝐹𝐺)‘(𝑥( ·𝑠𝑀)𝑦)) = (𝐹‘(𝐺‘(𝑥( ·𝑠𝑀)𝑦))))
4439, 42, 43syl2an2r 683 . . 3 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → ((𝐹𝐺)‘(𝑥( ·𝑠𝑀)𝑦)) = (𝐹‘(𝐺‘(𝑥( ·𝑠𝑀)𝑦))))
45 fvco2 6734 . . . . 5 ((𝐺 Fn (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀)) → ((𝐹𝐺)‘𝑦) = (𝐹‘(𝐺𝑦)))
4639, 21, 45syl2an2r 683 . . . 4 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → ((𝐹𝐺)‘𝑦) = (𝐹‘(𝐺𝑦)))
4746oveq2d 7149 . . 3 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝑥( ·𝑠𝑂)((𝐹𝐺)‘𝑦)) = (𝑥( ·𝑠𝑂)(𝐹‘(𝐺𝑦))))
4838, 44, 473eqtr4d 2865 . 2 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → ((𝐹𝐺)‘(𝑥( ·𝑠𝑀)𝑦)) = (𝑥( ·𝑠𝑂)((𝐹𝐺)‘𝑦)))
491, 2, 3, 4, 5, 6, 8, 10, 14, 18, 48islmhmd 19787 1 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹𝐺) ∈ (𝑀 LMHom 𝑂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398   = wceq 1537  wcel 2114  ccom 5535   Fn wfn 6326  wf 6327  cfv 6331  (class class class)co 7133  Basecbs 16462  Scalarcsca 16547   ·𝑠 cvsca 16548   GrpHom cghm 18334  LModclmod 19610   LMHom clmhm 19767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5436  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-map 8386  df-0g 16694  df-mgm 17831  df-sgrp 17880  df-mnd 17891  df-mhm 17935  df-grp 18085  df-ghm 18335  df-lmod 19612  df-lmhm 19770
This theorem is referenced by:  lmimco  20964  nmhmco  23341  mendring  39929
  Copyright terms: Public domain W3C validator