Metamath Proof Explorer

Theorem lindfpropd

Description: Property deduction for linearly independent families. (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 )
lindfpropd.x 
|- ( ph -> X e. A )
Assertion lindfpropd 
|- ( ph -> ( X LIndF K <-> X LIndF 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 lindfpropd.x 
 |-  ( ph -> X e. A )
10 3 sneqd 
 |-  ( ph -> { ( 0g ` ( Scalar ` K ) ) } = { ( 0g ` ( Scalar ` L ) ) } )
11 2 10 difeq12d 
 |-  ( ph -> ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) = ( ( Base ` ( Scalar ` L ) ) \ { ( 0g ` ( Scalar ` L ) ) } ) )
12 11 ad2antrr 
 |-  ( ( ( ph /\ X : dom X --> ( Base ` K ) ) /\ i e. dom X ) -> ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) = ( ( Base ` ( Scalar ` L ) ) \ { ( 0g ` ( Scalar ` L ) ) } ) )
13 simplll 
 |-  ( ( ( ( ph /\ X : dom X --> ( Base ` K ) ) /\ i e. dom X ) /\ k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) ) -> ph )
14 simpr 
 |-  ( ( ( ( ph /\ X : dom X --> ( Base ` K ) ) /\ i e. dom X ) /\ k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) ) -> k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) )
15 14 eldifad 
 |-  ( ( ( ( ph /\ X : dom X --> ( Base ` K ) ) /\ i e. dom X ) /\ k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) ) -> k e. ( Base ` ( Scalar ` K ) ) )
16 simpr 
 |-  ( ( ph /\ X : dom X --> ( Base ` K ) ) -> X : dom X --> ( Base ` K ) )
17 16 ffvelrnda 
 |-  ( ( ( ph /\ X : dom X --> ( Base ` K ) ) /\ i e. dom X ) -> ( X ` i ) e. ( Base ` K ) )
18 17 adantr 
 |-  ( ( ( ( ph /\ X : dom X --> ( Base ` K ) ) /\ i e. dom X ) /\ k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) ) -> ( X ` i ) e. ( Base ` K ) )
19 6 oveqrspc2v 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` K ) ) /\ ( X ` i ) e. ( Base ` K ) ) ) -> ( k ( .s ` K ) ( X ` i ) ) = ( k ( .s ` L ) ( X ` i ) ) )
20 13 15 18 19 syl12anc 
 |-  ( ( ( ( ph /\ X : dom X --> ( Base ` K ) ) /\ i e. dom X ) /\ k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) ) -> ( k ( .s ` K ) ( X ` i ) ) = ( k ( .s ` L ) ( X ` i ) ) )
21 eqidd 
 |-  ( ph -> ( Base ` K ) = ( Base ` K ) )
22 ssidd 
 |-  ( ph -> ( Base ` K ) C_ ( Base ` K ) )
23 eqidd 
 |-  ( ph -> ( Base ` ( Scalar ` K ) ) = ( Base ` ( Scalar ` K ) ) )
24 21 1 22 4 5 6 23 2 7 8 lsppropd 
 |-  ( ph -> ( LSpan ` K ) = ( LSpan ` L ) )
25 24 fveq1d 
 |-  ( ph -> ( ( LSpan ` K ) ` ( X " ( dom X \ { i } ) ) ) = ( ( LSpan ` L ) ` ( X " ( dom X \ { i } ) ) ) )
26 25 ad3antrrr 
 |-  ( ( ( ( ph /\ X : dom X --> ( Base ` K ) ) /\ i e. dom X ) /\ k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) ) -> ( ( LSpan ` K ) ` ( X " ( dom X \ { i } ) ) ) = ( ( LSpan ` L ) ` ( X " ( dom X \ { i } ) ) ) )
27 20 26 eleq12d 
 |-  ( ( ( ( ph /\ X : dom X --> ( Base ` K ) ) /\ i e. dom X ) /\ k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) ) -> ( ( k ( .s ` K ) ( X ` i ) ) e. ( ( LSpan ` K ) ` ( X " ( dom X \ { i } ) ) ) <-> ( k ( .s ` L ) ( X ` i ) ) e. ( ( LSpan ` L ) ` ( X " ( dom X \ { i } ) ) ) ) )
28 27 notbid 
 |-  ( ( ( ( ph /\ X : dom X --> ( Base ` K ) ) /\ i e. dom X ) /\ k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) ) -> ( -. ( k ( .s ` K ) ( X ` i ) ) e. ( ( LSpan ` K ) ` ( X " ( dom X \ { i } ) ) ) <-> -. ( k ( .s ` L ) ( X ` i ) ) e. ( ( LSpan ` L ) ` ( X " ( dom X \ { i } ) ) ) ) )
29 12 28 raleqbidva 
 |-  ( ( ( ph /\ X : dom X --> ( Base ` K ) ) /\ i e. dom X ) -> ( A. k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) -. ( k ( .s ` K ) ( X ` i ) ) e. ( ( LSpan ` K ) ` ( X " ( dom X \ { i } ) ) ) <-> A. k e. ( ( Base ` ( Scalar ` L ) ) \ { ( 0g ` ( Scalar ` L ) ) } ) -. ( k ( .s ` L ) ( X ` i ) ) e. ( ( LSpan ` L ) ` ( X " ( dom X \ { i } ) ) ) ) )
30 29 ralbidva 
 |-  ( ( ph /\ X : dom X --> ( Base ` K ) ) -> ( A. i e. dom X A. k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) -. ( k ( .s ` K ) ( X ` i ) ) e. ( ( LSpan ` K ) ` ( X " ( dom X \ { i } ) ) ) <-> A. i e. dom X A. k e. ( ( Base ` ( Scalar ` L ) ) \ { ( 0g ` ( Scalar ` L ) ) } ) -. ( k ( .s ` L ) ( X ` i ) ) e. ( ( LSpan ` L ) ` ( X " ( dom X \ { i } ) ) ) ) )
31 30 pm5.32da 
 |-  ( ph -> ( ( X : dom X --> ( Base ` K ) /\ A. i e. dom X A. k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) -. ( k ( .s ` K ) ( X ` i ) ) e. ( ( LSpan ` K ) ` ( X " ( dom X \ { i } ) ) ) ) <-> ( X : dom X --> ( Base ` K ) /\ A. i e. dom X A. k e. ( ( Base ` ( Scalar ` L ) ) \ { ( 0g ` ( Scalar ` L ) ) } ) -. ( k ( .s ` L ) ( X ` i ) ) e. ( ( LSpan ` L ) ` ( X " ( dom X \ { i } ) ) ) ) ) )
32 1 feq3d 
 |-  ( ph -> ( X : dom X --> ( Base ` K ) <-> X : dom X --> ( Base ` L ) ) )
33 32 anbi1d 
 |-  ( ph -> ( ( X : dom X --> ( Base ` K ) /\ A. i e. dom X A. k e. ( ( Base ` ( Scalar ` L ) ) \ { ( 0g ` ( Scalar ` L ) ) } ) -. ( k ( .s ` L ) ( X ` i ) ) e. ( ( LSpan ` L ) ` ( X " ( dom X \ { i } ) ) ) ) <-> ( X : dom X --> ( Base ` L ) /\ A. i e. dom X A. k e. ( ( Base ` ( Scalar ` L ) ) \ { ( 0g ` ( Scalar ` L ) ) } ) -. ( k ( .s ` L ) ( X ` i ) ) e. ( ( LSpan ` L ) ` ( X " ( dom X \ { i } ) ) ) ) ) )
34 31 33 bitrd 
 |-  ( ph -> ( ( X : dom X --> ( Base ` K ) /\ A. i e. dom X A. k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) -. ( k ( .s ` K ) ( X ` i ) ) e. ( ( LSpan ` K ) ` ( X " ( dom X \ { i } ) ) ) ) <-> ( X : dom X --> ( Base ` L ) /\ A. i e. dom X A. k e. ( ( Base ` ( Scalar ` L ) ) \ { ( 0g ` ( Scalar ` L ) ) } ) -. ( k ( .s ` L ) ( X ` i ) ) e. ( ( LSpan ` L ) ` ( X " ( dom X \ { i } ) ) ) ) ) )
35 eqid 
 |-  ( Base ` K ) = ( Base ` K )
36 eqid 
 |-  ( .s ` K ) = ( .s ` K )
37 eqid 
 |-  ( LSpan ` K ) = ( LSpan ` K )
38 eqid 
 |-  ( Scalar ` K ) = ( Scalar ` K )
39 eqid 
 |-  ( Base ` ( Scalar ` K ) ) = ( Base ` ( Scalar ` K ) )
40 eqid 
 |-  ( 0g ` ( Scalar ` K ) ) = ( 0g ` ( Scalar ` K ) )
41 35 36 37 38 39 40 islindf 
 |-  ( ( K e. V /\ X e. A ) -> ( X LIndF K <-> ( X : dom X --> ( Base ` K ) /\ A. i e. dom X A. k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) -. ( k ( .s ` K ) ( X ` i ) ) e. ( ( LSpan ` K ) ` ( X " ( dom X \ { i } ) ) ) ) ) )
42 7 9 41 syl2anc 
 |-  ( ph -> ( X LIndF K <-> ( X : dom X --> ( Base ` K ) /\ A. i e. dom X A. k e. ( ( Base ` ( Scalar ` K ) ) \ { ( 0g ` ( Scalar ` K ) ) } ) -. ( k ( .s ` K ) ( X ` i ) ) e. ( ( LSpan ` K ) ` ( X " ( dom X \ { i } ) ) ) ) ) )
43 eqid 
 |-  ( Base ` L ) = ( Base ` L )
44 eqid 
 |-  ( .s ` L ) = ( .s ` L )
45 eqid 
 |-  ( LSpan ` L ) = ( LSpan ` L )
46 eqid 
 |-  ( Scalar ` L ) = ( Scalar ` L )
47 eqid 
 |-  ( Base ` ( Scalar ` L ) ) = ( Base ` ( Scalar ` L ) )
48 eqid 
 |-  ( 0g ` ( Scalar ` L ) ) = ( 0g ` ( Scalar ` L ) )
49 43 44 45 46 47 48 islindf 
 |-  ( ( L e. W /\ X e. A ) -> ( X LIndF L <-> ( X : dom X --> ( Base ` L ) /\ A. i e. dom X A. k e. ( ( Base ` ( Scalar ` L ) ) \ { ( 0g ` ( Scalar ` L ) ) } ) -. ( k ( .s ` L ) ( X ` i ) ) e. ( ( LSpan ` L ) ` ( X " ( dom X \ { i } ) ) ) ) ) )
50 8 9 49 syl2anc 
 |-  ( ph -> ( X LIndF L <-> ( X : dom X --> ( Base ` L ) /\ A. i e. dom X A. k e. ( ( Base ` ( Scalar ` L ) ) \ { ( 0g ` ( Scalar ` L ) ) } ) -. ( k ( .s ` L ) ( X ` i ) ) e. ( ( LSpan ` L ) ` ( X " ( dom X \ { i } ) ) ) ) ) )
51 34 42 50 3bitr4d 
 |-  ( ph -> ( X LIndF K <-> X LIndF L ) )