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 𝐿 ) )