This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lindfpropd

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

Ref Expression
Hypotheses lindfpropd.1 ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
lindfpropd.2 ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
lindfpropd.3 ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐾 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) )
lindfpropd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
lindfpropd.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
lindfpropd.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
lindfpropd.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
lindfpropd.l ⊢ ( 𝜑 → 𝐿 ∈ 𝑊 )
lindfpropd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion lindfpropd ( 𝜑 → ( 𝑋 LIndF 𝐾 ↔ 𝑋 LIndF 𝐿 ) )

Proof

Step Hyp Ref Expression
1 lindfpropd.1 ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
2 lindfpropd.2 ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
3 lindfpropd.3 ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐾 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) )
4 lindfpropd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
5 lindfpropd.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
6 lindfpropd.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
7 lindfpropd.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
8 lindfpropd.l ⊢ ( 𝜑 → 𝐿 ∈ 𝑊 )
9 lindfpropd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
10 3 sneqd ⊢ ( 𝜑 → { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } = { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } )
11 2 10 difeq12d ⊢ ( 𝜑 → ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) = ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) )
12 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) → ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) = ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) )
13 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → 𝜑 )
14 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) )
15 14 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) → 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) )
17 16 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) → ( 𝑋 ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) )
18 17 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → ( 𝑋 ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) )
19 6 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∧ ( 𝑋 ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝐾 ) ( 𝑋 ‘ 𝑖 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐿 ) ( 𝑋 ‘ 𝑖 ) ) )
20 13 15 18 19 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → ( 𝑘 ( ·𝑠 ‘ 𝐾 ) ( 𝑋 ‘ 𝑖 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝐿 ) ( 𝑋 ‘ 𝑖 ) ) )
21 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
22 ssidd ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) ⊆ ( Base ‘ 𝐾 ) )
23 eqidd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
24 21 1 22 4 5 6 23 2 7 8 lsppropd ⊢ ( 𝜑 → ( LSpan ‘ 𝐾 ) = ( LSpan ‘ 𝐿 ) )
25 24 fveq1d ⊢ ( 𝜑 → ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) = ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) )
26 25 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) = ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) )
27 20 26 eleq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝐾 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝐿 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) )
28 27 notbid ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ) → ( ¬ ( 𝑘 ( ·𝑠 ‘ 𝐾 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ↔ ¬ ( 𝑘 ( ·𝑠 ‘ 𝐿 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) )
29 12 28 raleqbidva ⊢ ( ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) ∧ 𝑖 ∈ dom 𝑋 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐾 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐿 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) )
30 29 ralbidva ⊢ ( ( 𝜑 ∧ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑖 ∈ dom 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐾 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ↔ ∀ 𝑖 ∈ dom 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐿 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) )
31 30 pm5.32da ⊢ ( 𝜑 → ( ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑖 ∈ dom 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐾 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑖 ∈ dom 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐿 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
32 1 feq3d ⊢ ( 𝜑 → ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ↔ 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐿 ) ) )
33 32 anbi1d ⊢ ( 𝜑 → ( ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑖 ∈ dom 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐿 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐿 ) ∧ ∀ 𝑖 ∈ dom 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐿 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
34 31 33 bitrd ⊢ ( 𝜑 → ( ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑖 ∈ dom 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐾 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐿 ) ∧ ∀ 𝑖 ∈ dom 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐿 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
35 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
36 eqid ⊢ ( ·𝑠 ‘ 𝐾 ) = ( ·𝑠 ‘ 𝐾 )
37 eqid ⊢ ( LSpan ‘ 𝐾 ) = ( LSpan ‘ 𝐾 )
38 eqid ⊢ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐾 )
39 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐾 ) ) = ( Base ‘ ( Scalar ‘ 𝐾 ) )
40 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐾 ) ) = ( 0g ‘ ( Scalar ‘ 𝐾 ) )
41 35 36 37 38 39 40 islindf ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 LIndF 𝐾 ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑖 ∈ dom 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐾 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
42 7 9 41 syl2anc ⊢ ( 𝜑 → ( 𝑋 LIndF 𝐾 ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑖 ∈ dom 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐾 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐾 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐾 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐾 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
43 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
44 eqid ⊢ ( ·𝑠 ‘ 𝐿 ) = ( ·𝑠 ‘ 𝐿 )
45 eqid ⊢ ( LSpan ‘ 𝐿 ) = ( LSpan ‘ 𝐿 )
46 eqid ⊢ ( Scalar ‘ 𝐿 ) = ( Scalar ‘ 𝐿 )
47 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐿 ) ) = ( Base ‘ ( Scalar ‘ 𝐿 ) )
48 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐿 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) )
49 43 44 45 46 47 48 islindf ⊢ ( ( 𝐿 ∈ 𝑊 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 LIndF 𝐿 ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐿 ) ∧ ∀ 𝑖 ∈ dom 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐿 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
50 8 9 49 syl2anc ⊢ ( 𝜑 → ( 𝑋 LIndF 𝐿 ↔ ( 𝑋 : dom 𝑋 ⟶ ( Base ‘ 𝐿 ) ∧ ∀ 𝑖 ∈ dom 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝐿 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝐿 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝐿 ) ( 𝑋 ‘ 𝑖 ) ) ∈ ( ( LSpan ‘ 𝐿 ) ‘ ( 𝑋 “ ( dom 𝑋 ∖ { 𝑖 } ) ) ) ) ) )
51 34 42 50 3bitr4d ⊢ ( 𝜑 → ( 𝑋 LIndF 𝐾 ↔ 𝑋 LIndF 𝐿 ) )