Metamath Proof Explorer

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