Metamath Proof Explorer

Theorem lmiclbs

Description: Having a basis is an isomorphism invariant. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Hypotheses lmimlbs.j 
|- J = ( LBasis ` S )
lmimlbs.k 
|- K = ( LBasis ` T )
Assertion lmiclbs 
|- ( S ~=m T -> ( J =/= (/) -> K =/= (/) ) )

Proof

Step Hyp Ref Expression
1 lmimlbs.j 
 |-  J = ( LBasis ` S )
2 lmimlbs.k 
 |-  K = ( LBasis ` T )
3 brlmic 
 |-  ( S ~=m T <-> ( S LMIso T ) =/= (/) )
4 n0 
 |-  ( ( S LMIso T ) =/= (/) <-> E. f f e. ( S LMIso T ) )
5 3 4 bitri 
 |-  ( S ~=m T <-> E. f f e. ( S LMIso T ) )
6 n0 
 |-  ( J =/= (/) <-> E. b b e. J )
7 1 2 lmimlbs 
 |-  ( ( f e. ( S LMIso T ) /\ b e. J ) -> ( f " b ) e. K )
8 7 ne0d 
 |-  ( ( f e. ( S LMIso T ) /\ b e. J ) -> K =/= (/) )
9 8 ex 
 |-  ( f e. ( S LMIso T ) -> ( b e. J -> K =/= (/) ) )
10 9 exlimdv 
 |-  ( f e. ( S LMIso T ) -> ( E. b b e. J -> K =/= (/) ) )
11 6 10 syl5bi 
 |-  ( f e. ( S LMIso T ) -> ( J =/= (/) -> K =/= (/) ) )
12 11 exlimiv 
 |-  ( E. f f e. ( S LMIso T ) -> ( J =/= (/) -> K =/= (/) ) )
13 5 12 sylbi 
 |-  ( S ~=m T -> ( J =/= (/) -> K =/= (/) ) )