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

Theorem lmhmco 20605
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 2732 . 2 (Base‘𝑀) = (Base‘𝑀)
2 eqid 2732 . 2 ( ·𝑠𝑀) = ( ·𝑠𝑀)
3 eqid 2732 . 2 ( ·𝑠𝑂) = ( ·𝑠𝑂)
4 eqid 2732 . 2 (Scalar‘𝑀) = (Scalar‘𝑀)
5 eqid 2732 . 2 (Scalar‘𝑂) = (Scalar‘𝑂)
6 eqid 2732 . 2 (Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀))
7 lmhmlmod1 20595 . . 3 (𝐺 ∈ (𝑀 LMHom 𝑁) → 𝑀 ∈ LMod)
87adantl 482 . 2 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝑀 ∈ LMod)
9 lmhmlmod2 20594 . . 3 (𝐹 ∈ (𝑁 LMHom 𝑂) → 𝑂 ∈ LMod)
109adantr 481 . 2 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝑂 ∈ LMod)
11 eqid 2732 . . . 4 (Scalar‘𝑁) = (Scalar‘𝑁)
1211, 5lmhmsca 20592 . . 3 (𝐹 ∈ (𝑁 LMHom 𝑂) → (Scalar‘𝑂) = (Scalar‘𝑁))
134, 11lmhmsca 20592 . . 3 (𝐺 ∈ (𝑀 LMHom 𝑁) → (Scalar‘𝑁) = (Scalar‘𝑀))
1412, 13sylan9eq 2792 . 2 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (Scalar‘𝑂) = (Scalar‘𝑀))
15 lmghm 20593 . . 3 (𝐹 ∈ (𝑁 LMHom 𝑂) → 𝐹 ∈ (𝑁 GrpHom 𝑂))
16 lmghm 20593 . . 3 (𝐺 ∈ (𝑀 LMHom 𝑁) → 𝐺 ∈ (𝑀 GrpHom 𝑁))
17 ghmco 19080 . . 3 ((𝐹 ∈ (𝑁 GrpHom 𝑂) ∧ 𝐺 ∈ (𝑀 GrpHom 𝑁)) → (𝐹𝐺) ∈ (𝑀 GrpHom 𝑂))
1815, 16, 17syl2an 596 . 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 2732 . . . . . . 7 ( ·𝑠𝑁) = ( ·𝑠𝑁)
234, 6, 1, 2, 22lmhmlin 20597 . . . . . 6 ((𝐺 ∈ (𝑀 LMHom 𝑁) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝐺‘(𝑥( ·𝑠𝑀)𝑦)) = (𝑥( ·𝑠𝑁)(𝐺𝑦)))
2419, 20, 21, 23syl3anc 1371 . . . . 5 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐺‘(𝑥( ·𝑠𝑀)𝑦)) = (𝑥( ·𝑠𝑁)(𝐺𝑦)))
2524fveq2d 6883 . . . 4 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐹‘(𝐺‘(𝑥( ·𝑠𝑀)𝑦))) = (𝐹‘(𝑥( ·𝑠𝑁)(𝐺𝑦))))
26 simpll 765 . . . . 5 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝐹 ∈ (𝑁 LMHom 𝑂))
2713fveq2d 6883 . . . . . . 7 (𝐺 ∈ (𝑀 LMHom 𝑁) → (Base‘(Scalar‘𝑁)) = (Base‘(Scalar‘𝑀)))
2827ad2antlr 725 . . . . . 6 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (Base‘(Scalar‘𝑁)) = (Base‘(Scalar‘𝑀)))
2920, 28eleqtrrd 2836 . . . . 5 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝑥 ∈ (Base‘(Scalar‘𝑁)))
30 eqid 2732 . . . . . . . . 9 (Base‘𝑁) = (Base‘𝑁)
311, 30lmhmf 20596 . . . . . . . 8 (𝐺 ∈ (𝑀 LMHom 𝑁) → 𝐺:(Base‘𝑀)⟶(Base‘𝑁))
3231adantl 482 . . . . . . 7 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝐺:(Base‘𝑀)⟶(Base‘𝑁))
3332ffvelcdmda 7072 . . . . . 6 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝐺𝑦) ∈ (Base‘𝑁))
3433adantrl 714 . . . . 5 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐺𝑦) ∈ (Base‘𝑁))
35 eqid 2732 . . . . . 6 (Base‘(Scalar‘𝑁)) = (Base‘(Scalar‘𝑁))
3611, 35, 30, 22, 3lmhmlin 20597 . . . . 5 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑁)) ∧ (𝐺𝑦) ∈ (Base‘𝑁)) → (𝐹‘(𝑥( ·𝑠𝑁)(𝐺𝑦))) = (𝑥( ·𝑠𝑂)(𝐹‘(𝐺𝑦))))
3726, 29, 34, 36syl3anc 1371 . . . 4 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐹‘(𝑥( ·𝑠𝑁)(𝐺𝑦))) = (𝑥( ·𝑠𝑂)(𝐹‘(𝐺𝑦))))
3825, 37eqtrd 2772 . . 3 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝐹‘(𝐺‘(𝑥( ·𝑠𝑀)𝑦))) = (𝑥( ·𝑠𝑂)(𝐹‘(𝐺𝑦))))
3932ffnd 6706 . . . 4 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → 𝐺 Fn (Base‘𝑀))
407ad2antlr 725 . . . . 5 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → 𝑀 ∈ LMod)
411, 4, 2, 6lmodvscl 20440 . . . . 5 ((𝑀 ∈ LMod ∧ 𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀)) → (𝑥( ·𝑠𝑀)𝑦) ∈ (Base‘𝑀))
4240, 20, 21, 41syl3anc 1371 . . . 4 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝑥( ·𝑠𝑀)𝑦) ∈ (Base‘𝑀))
43 fvco2 6975 . . . 4 ((𝐺 Fn (Base‘𝑀) ∧ (𝑥( ·𝑠𝑀)𝑦) ∈ (Base‘𝑀)) → ((𝐹𝐺)‘(𝑥( ·𝑠𝑀)𝑦)) = (𝐹‘(𝐺‘(𝑥( ·𝑠𝑀)𝑦))))
4439, 42, 43syl2an2r 683 . . 3 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → ((𝐹𝐺)‘(𝑥( ·𝑠𝑀)𝑦)) = (𝐹‘(𝐺‘(𝑥( ·𝑠𝑀)𝑦))))
45 fvco2 6975 . . . . 5 ((𝐺 Fn (Base‘𝑀) ∧ 𝑦 ∈ (Base‘𝑀)) → ((𝐹𝐺)‘𝑦) = (𝐹‘(𝐺𝑦)))
4639, 21, 45syl2an2r 683 . . . 4 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → ((𝐹𝐺)‘𝑦) = (𝐹‘(𝐺𝑦)))
4746oveq2d 7410 . . 3 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → (𝑥( ·𝑠𝑂)((𝐹𝐺)‘𝑦)) = (𝑥( ·𝑠𝑂)(𝐹‘(𝐺𝑦))))
4838, 44, 473eqtr4d 2782 . 2 (((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑀)) ∧ 𝑦 ∈ (Base‘𝑀))) → ((𝐹𝐺)‘(𝑥( ·𝑠𝑀)𝑦)) = (𝑥( ·𝑠𝑂)((𝐹𝐺)‘𝑦)))
491, 2, 3, 4, 5, 6, 8, 10, 14, 18, 48islmhmd 20601 1 ((𝐹 ∈ (𝑁 LMHom 𝑂) ∧ 𝐺 ∈ (𝑀 LMHom 𝑁)) → (𝐹𝐺) ∈ (𝑀 LMHom 𝑂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  ccom 5674   Fn wfn 6528  wf 6529  cfv 6533  (class class class)co 7394  Basecbs 17128  Scalarcsca 17184   ·𝑠 cvsca 17185   GrpHom cghm 19057  LModclmod 20422   LMHom clmhm 20581
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 2703  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5568  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7350  df-ov 7397  df-oprab 7398  df-mpo 7399  df-map 8807  df-0g 17371  df-mgm 18545  df-sgrp 18594  df-mnd 18605  df-mhm 18649  df-grp 18799  df-ghm 19058  df-lmod 20424  df-lmhm 20584
This theorem is referenced by:  lmimco  21334  nmhmco  24204  mendring  41769
  Copyright terms: Public domain W3C validator