Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmhmf1o Structured version   Unicode version

Theorem lmhmf1o 17819
 Description: A bijective module homomorphism is also converse homomorphic. (Contributed by Stefan O'Rear, 25-Jan-2015.)
Hypotheses
Ref Expression
lmhmf1o.x
lmhmf1o.y
Assertion
Ref Expression
lmhmf1o LMHom LMHom

Proof of Theorem lmhmf1o
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lmhmf1o.y . . 3
2 eqid 2457 . . 3
3 eqid 2457 . . 3
4 eqid 2457 . . 3 Scalar Scalar
5 eqid 2457 . . 3 Scalar Scalar
6 eqid 2457 . . 3 Scalar Scalar
7 lmhmlmod2 17805 . . . 4 LMHom
87adantr 465 . . 3 LMHom
9 lmhmlmod1 17806 . . . 4 LMHom
109adantr 465 . . 3 LMHom
115, 4lmhmsca 17803 . . . . 5 LMHom Scalar Scalar
1211eqcomd 2465 . . . 4 LMHom Scalar Scalar
1312adantr 465 . . 3 LMHom Scalar Scalar
14 lmghm 17804 . . . . 5 LMHom
15 lmhmf1o.x . . . . . 6
1615, 1ghmf1o 16423 . . . . 5
1714, 16syl 16 . . . 4 LMHom
1817biimpa 484 . . 3 LMHom
19 simpll 753 . . . . . 6 LMHom Scalar LMHom
2013fveq2d 5876 . . . . . . . . 9 LMHom Scalar Scalar
2120eleq2d 2527 . . . . . . . 8 LMHom Scalar Scalar
2221biimpar 485 . . . . . . 7 LMHom Scalar Scalar
2322adantrr 716 . . . . . 6 LMHom Scalar Scalar
24 f1ocnv 5834 . . . . . . . . . 10
25 f1of 5822 . . . . . . . . . 10
2624, 25syl 16 . . . . . . . . 9
2726adantl 466 . . . . . . . 8 LMHom
2827ffvelrnda 6032 . . . . . . 7 LMHom
2928adantrl 715 . . . . . 6 LMHom Scalar
30 eqid 2457 . . . . . . 7 Scalar Scalar
315, 30, 15, 3, 2lmhmlin 17808 . . . . . 6 LMHom Scalar
3219, 23, 29, 31syl3anc 1228 . . . . 5 LMHom Scalar
33 f1ocnvfv2 6184 . . . . . . 7
3433ad2ant2l 745 . . . . . 6 LMHom Scalar
3534oveq2d 6312 . . . . 5 LMHom Scalar
3632, 35eqtrd 2498 . . . 4 LMHom Scalar
37 simplr 755 . . . . 5 LMHom Scalar
3810adantr 465 . . . . . 6 LMHom Scalar
3915, 5, 3, 30lmodvscl 17656 . . . . . 6 Scalar
4038, 23, 29, 39syl3anc 1228 . . . . 5 LMHom Scalar
41 f1ocnvfv 6185 . . . . 5
4237, 40, 41syl2anc 661 . . . 4 LMHom Scalar
4336, 42mpd 15 . . 3 LMHom Scalar
441, 2, 3, 4, 5, 6, 8, 10, 13, 18, 43islmhmd 17812 . 2 LMHom LMHom
4515, 1lmhmf 17807 . . . . 5 LMHom
46 ffn 5737 . . . . 5
4745, 46syl 16 . . . 4 LMHom
4847adantr 465 . . 3 LMHom LMHom
491, 15lmhmf 17807 . . . . 5 LMHom
5049adantl 466 . . . 4 LMHom LMHom
51 ffn 5737 . . . 4
5250, 51syl 16 . . 3 LMHom LMHom
53 dff1o4 5830 . . 3
5448, 52, 53sylanbrc 664 . 2 LMHom LMHom
5544, 54impbida 832 1 LMHom LMHom
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1395   wcel 1819  ccnv 5007   wfn 5589  wf 5590  wf1o 5593  cfv 5594  (class class class)co 6296  cbs 14644  Scalarcsca 14715  cvsca 14716   cghm 16391  clmod 17639   LMHom clmhm 17792 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-mgm 15999  df-sgrp 16038  df-mnd 16048  df-grp 16184  df-ghm 16392  df-lmod 17641  df-lmhm 17795 This theorem is referenced by:  islmim2  17839
 Copyright terms: Public domain W3C validator