Theorem lsslindf

Description: Linear independence is unchanged by working in a subspace. (Contributed by Stefan O'Rear, 24-Feb-2015) (Revised by Stefan O'Rear, 6-May-2015)

	Ref	Expression
Hypotheses	lsslindf.u	⊢ 𝑈 = ( LSubSp ‘ 𝑊 )
	lsslindf.x	⊢ 𝑋 = ( 𝑊 ↾s 𝑆 )
Assertion	lsslindf	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) → ( 𝐹 LIndF 𝑋 ↔ 𝐹 LIndF 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		lsslindf.u	⊢ 𝑈 = ( LSubSp ‘ 𝑊 )
2		lsslindf.x	⊢ 𝑋 = ( 𝑊 ↾s 𝑆 )
3		rellindf	⊢ Rel LIndF
4	3	brrelex1i	⊢ ( 𝐹 LIndF 𝑋 → 𝐹 ∈ V )
5	4	a1i	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) → ( 𝐹 LIndF 𝑋 → 𝐹 ∈ V ) )
6	3	brrelex1i	⊢ ( 𝐹 LIndF 𝑊 → 𝐹 ∈ V )
7	6	a1i	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) → ( 𝐹 LIndF 𝑊 → 𝐹 ∈ V ) )
8		simpr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑋 ) ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑋 ) )
9		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10	2 9	ressbasss	⊢ ( Base ‘ 𝑋 ) ⊆ ( Base ‘ 𝑊 )
11		fss	⊢ ( ( 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑋 ) ∧ ( Base ‘ 𝑋 ) ⊆ ( Base ‘ 𝑊 ) ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) )
12	8 10 11	sylancl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑋 ) ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) )
13		ffn	⊢ ( 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) → 𝐹 Fn dom 𝐹 )
14	13	adantl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) ) → 𝐹 Fn dom 𝐹 )
15		simp3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) → ran 𝐹 ⊆ 𝑆 )
16	9 1	lssss	⊢ ( 𝑆 ∈ 𝑈 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
17	16	3ad2ant2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
18	2 9	ressbas2	⊢ ( 𝑆 ⊆ ( Base ‘ 𝑊 ) → 𝑆 = ( Base ‘ 𝑋 ) )
19	17 18	syl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) → 𝑆 = ( Base ‘ 𝑋 ) )
20	15 19	sseqtrd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) → ran 𝐹 ⊆ ( Base ‘ 𝑋 ) )
21	20	adantr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) ) → ran 𝐹 ⊆ ( Base ‘ 𝑋 ) )
22		df-f	⊢ ( 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑋 ) ↔ ( 𝐹 Fn dom 𝐹 ∧ ran 𝐹 ⊆ ( Base ‘ 𝑋 ) ) )
23	14 21 22	sylanbrc	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑋 ) )
24	12 23	impbida	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) → ( 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑋 ) ↔ 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) ) )
25	24	adantr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑋 ) ↔ 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) ) )
26		simpl2	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → 𝑆 ∈ 𝑈 )
27		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
28	2 27	resssca	⊢ ( 𝑆 ∈ 𝑈 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
29	28	eqcomd	⊢ ( 𝑆 ∈ 𝑈 → ( Scalar ‘ 𝑋 ) = ( Scalar ‘ 𝑊 ) )
30	26 29	syl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( Scalar ‘ 𝑋 ) = ( Scalar ‘ 𝑊 ) )
31	30	fveq2d	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( Base ‘ ( Scalar ‘ 𝑋 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
32	30	fveq2d	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( 0g ‘ ( Scalar ‘ 𝑋 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
33	32	sneqd	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → { ( 0g ‘ ( Scalar ‘ 𝑋 ) ) } = { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
34	31 33	difeq12d	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑋 ) ) } ) = ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
35		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
36	2 35	ressvsca	⊢ ( 𝑆 ∈ 𝑈 → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑋 ) )
37	36	eqcomd	⊢ ( 𝑆 ∈ 𝑈 → ( ·𝑠 ‘ 𝑋 ) = ( ·𝑠 ‘ 𝑊 ) )
38	26 37	syl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( ·𝑠 ‘ 𝑋 ) = ( ·𝑠 ‘ 𝑊 ) )
39	38	oveqd	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( 𝑘 ( ·𝑠 ‘ 𝑋 ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) )
40		simpl1	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → 𝑊 ∈ LMod )
41		imassrn	⊢ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ⊆ ran 𝐹
42		simpl3	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ran 𝐹 ⊆ 𝑆 )
43	41 42	sstrid	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ⊆ 𝑆 )
44		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
45		eqid	⊢ ( LSpan ‘ 𝑋 ) = ( LSpan ‘ 𝑋 )
46	2 44 45 1	lsslsp	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ⊆ 𝑆 ) → ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) = ( ( LSpan ‘ 𝑋 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) )
47	40 26 43 46	syl3anc	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) = ( ( LSpan ‘ 𝑋 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) )
48	47	eqcomd	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( ( LSpan ‘ 𝑋 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) = ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) )
49	39 48	eleq12d	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑋 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑋 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
50	49	notbid	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( ¬ ( 𝑘 ( ·𝑠 ‘ 𝑋 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑋 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
51	34 50	raleqbidv	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑋 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑋 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑋 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
52	51	ralbidv	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑋 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑋 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑋 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
53	25 52	anbi12d	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( ( 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑋 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑋 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑋 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ↔ ( 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
54	2	ovexi	⊢ 𝑋 ∈ V
55	54	a1i	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) → 𝑋 ∈ V )
56		eqid	⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
57		eqid	⊢ ( ·𝑠 ‘ 𝑋 ) = ( ·𝑠 ‘ 𝑋 )
58		eqid	⊢ ( Scalar ‘ 𝑋 ) = ( Scalar ‘ 𝑋 )
59		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑋 ) ) = ( Base ‘ ( Scalar ‘ 𝑋 ) )
60		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑋 ) ) = ( 0g ‘ ( Scalar ‘ 𝑋 ) )
61	56 57 45 58 59 60	islindf	⊢ ( ( 𝑋 ∈ V ∧ 𝐹 ∈ V ) → ( 𝐹 LIndF 𝑋 ↔ ( 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑋 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑋 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑋 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
62	55 61	sylan	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( 𝐹 LIndF 𝑋 ↔ ( 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑋 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑋 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑋 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
63		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
64		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
65	9 35 44 27 63 64	islindf	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 ∈ V ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
66	65	3ad2antl1	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
67	53 62 66	3bitr4d	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ∈ V ) → ( 𝐹 LIndF 𝑋 ↔ 𝐹 LIndF 𝑊 ) )
68	67	ex	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) → ( 𝐹 ∈ V → ( 𝐹 LIndF 𝑋 ↔ 𝐹 LIndF 𝑊 ) ) )
69	5 7 68	pm5.21ndd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝑆 ) → ( 𝐹 LIndF 𝑋 ↔ 𝐹 LIndF 𝑊 ) )