Metamath Proof Explorer

Theorem lmictra

Description: Module isomorphism is transitive. (Contributed by AV, 10-Mar-2019)

Ref Expression
Assertion lmictra 
|- ( ( R ~=m S /\ S ~=m T ) -> R ~=m T )

Proof

Step Hyp Ref Expression
1 brlmic 
 |-  ( R ~=m S <-> ( R LMIso S ) =/= (/) )
2 brlmic 
 |-  ( S ~=m T <-> ( S LMIso T ) =/= (/) )
3 n0 
 |-  ( ( R LMIso S ) =/= (/) <-> E. g g e. ( R LMIso S ) )
4 n0 
 |-  ( ( S LMIso T ) =/= (/) <-> E. f f e. ( S LMIso T ) )
5 lmimco 
 |-  ( ( f e. ( S LMIso T ) /\ g e. ( R LMIso S ) ) -> ( f o. g ) e. ( R LMIso T ) )
6 brlmici 
 |-  ( ( f o. g ) e. ( R LMIso T ) -> R ~=m T )
7 5 6 syl 
 |-  ( ( f e. ( S LMIso T ) /\ g e. ( R LMIso S ) ) -> R ~=m T )
8 7 ex 
 |-  ( f e. ( S LMIso T ) -> ( g e. ( R LMIso S ) -> R ~=m T ) )
9 8 exlimiv 
 |-  ( E. f f e. ( S LMIso T ) -> ( g e. ( R LMIso S ) -> R ~=m T ) )
10 9 com12 
 |-  ( g e. ( R LMIso S ) -> ( E. f f e. ( S LMIso T ) -> R ~=m T ) )
11 10 exlimiv 
 |-  ( E. g g e. ( R LMIso S ) -> ( E. f f e. ( S LMIso T ) -> R ~=m T ) )
12 11 imp 
 |-  ( ( E. g g e. ( R LMIso S ) /\ E. f f e. ( S LMIso T ) ) -> R ~=m T )
13 3 4 12 syl2anb 
 |-  ( ( ( R LMIso S ) =/= (/) /\ ( S LMIso T ) =/= (/) ) -> R ~=m T )
14 1 2 13 syl2anb 
 |-  ( ( R ~=m S /\ S ~=m T ) -> R ~=m T )