Metamath Proof Explorer

Theorem lindspropd

Description: Property deduction for linearly independent sets. (Contributed by Thierry Arnoux, 16-Jul-2023)

Ref Expression
Hypotheses lindfpropd.1 
|- ( ph -> ( Base ` K ) = ( Base ` L ) )
lindfpropd.2 
|- ( ph -> ( Base ` ( Scalar ` K ) ) = ( Base ` ( Scalar ` L ) ) )
lindfpropd.3 
|- ( ph -> ( 0g ` ( Scalar ` K ) ) = ( 0g ` ( Scalar ` L ) ) )
lindfpropd.4 
|- ( ( ph /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
lindfpropd.5 
|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` K ) ) /\ y e. ( Base ` K ) ) ) -> ( x ( .s ` K ) y ) e. ( Base ` K ) )
lindfpropd.6 
|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` K ) ) /\ y e. ( Base ` K ) ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
lindfpropd.k 
|- ( ph -> K e. V )
lindfpropd.l 
|- ( ph -> L e. W )
Assertion lindspropd 
|- ( ph -> ( LIndS ` K ) = ( LIndS ` L ) )

Proof

Step Hyp Ref Expression
1 lindfpropd.1 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
2 lindfpropd.2 
 |-  ( ph -> ( Base ` ( Scalar ` K ) ) = ( Base ` ( Scalar ` L ) ) )
3 lindfpropd.3 
 |-  ( ph -> ( 0g ` ( Scalar ` K ) ) = ( 0g ` ( Scalar ` L ) ) )
4 lindfpropd.4 
 |-  ( ( ph /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
5 lindfpropd.5 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` K ) ) /\ y e. ( Base ` K ) ) ) -> ( x ( .s ` K ) y ) e. ( Base ` K ) )
6 lindfpropd.6 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` K ) ) /\ y e. ( Base ` K ) ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
7 lindfpropd.k 
 |-  ( ph -> K e. V )
8 lindfpropd.l 
 |-  ( ph -> L e. W )
9 1 sseq2d 
 |-  ( ph -> ( z C_ ( Base ` K ) <-> z C_ ( Base ` L ) ) )
10 vex 
 |-  z e. _V
11 10 a1i 
 |-  ( ph -> z e. _V )
12 11 resiexd 
 |-  ( ph -> ( _I |` z ) e. _V )
13 1 2 3 4 5 6 7 8 12 lindfpropd 
 |-  ( ph -> ( ( _I |` z ) LIndF K <-> ( _I |` z ) LIndF L ) )
14 9 13 anbi12d 
 |-  ( ph -> ( ( z C_ ( Base ` K ) /\ ( _I |` z ) LIndF K ) <-> ( z C_ ( Base ` L ) /\ ( _I |` z ) LIndF L ) ) )
15 eqid 
 |-  ( Base ` K ) = ( Base ` K )
16 15 islinds 
 |-  ( K e. V -> ( z e. ( LIndS ` K ) <-> ( z C_ ( Base ` K ) /\ ( _I |` z ) LIndF K ) ) )
17 7 16 syl 
 |-  ( ph -> ( z e. ( LIndS ` K ) <-> ( z C_ ( Base ` K ) /\ ( _I |` z ) LIndF K ) ) )
18 eqid 
 |-  ( Base ` L ) = ( Base ` L )
19 18 islinds 
 |-  ( L e. W -> ( z e. ( LIndS ` L ) <-> ( z C_ ( Base ` L ) /\ ( _I |` z ) LIndF L ) ) )
20 8 19 syl 
 |-  ( ph -> ( z e. ( LIndS ` L ) <-> ( z C_ ( Base ` L ) /\ ( _I |` z ) LIndF L ) ) )
21 14 17 20 3bitr4d 
 |-  ( ph -> ( z e. ( LIndS ` K ) <-> z e. ( LIndS ` L ) ) )
22 21 eqrdv 
 |-  ( ph -> ( LIndS ` K ) = ( LIndS ` L ) )