Metamath Proof Explorer

Theorem lsslinds

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

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

Proof

Step Hyp Ref Expression
1 lsslindf.u ⊢ 𝑈 = ( LSubSp ‘ 𝑊 )
2 lsslindf.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑆 )
3 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4 3 1 lssss ⊢ ( 𝑆 ∈ 𝑈 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
5 2 3 ressbas2 ⊢ ( 𝑆 ⊆ ( Base ‘ 𝑊 ) → 𝑆 = ( Base ‘ 𝑋 ) )
6 4 5 syl ⊢ ( 𝑆 ∈ 𝑈 → 𝑆 = ( Base ‘ 𝑋 ) )
7 6 3ad2ant2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆 ) → 𝑆 = ( Base ‘ 𝑋 ) )
8 7 sseq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆 ) → ( 𝐹 ⊆ 𝑆 ↔ 𝐹 ⊆ ( Base ‘ 𝑋 ) ) )
9 4 3ad2ant2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
10 sstr2 ⊢ ( 𝐹 ⊆ 𝑆 → ( 𝑆 ⊆ ( Base ‘ 𝑊 ) → 𝐹 ⊆ ( Base ‘ 𝑊 ) ) )
11 9 10 mpan9 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ⊆ 𝑆 ) → 𝐹 ⊆ ( Base ‘ 𝑊 ) )
12 simpl3 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆 ) ∧ 𝐹 ⊆ ( Base ‘ 𝑊 ) ) → 𝐹 ⊆ 𝑆 )
13 11 12 impbida ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆 ) → ( 𝐹 ⊆ 𝑆 ↔ 𝐹 ⊆ ( Base ‘ 𝑊 ) ) )
14 8 13 bitr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆 ) → ( 𝐹 ⊆ ( Base ‘ 𝑋 ) ↔ 𝐹 ⊆ ( Base ‘ 𝑊 ) ) )
15 rnresi ⊢ ran ( I ↾ 𝐹 ) = 𝐹
16 15 sseq1i ⊢ ( ran ( I ↾ 𝐹 ) ⊆ 𝑆 ↔ 𝐹 ⊆ 𝑆 )
17 1 2 lsslindf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ ran ( I ↾ 𝐹 ) ⊆ 𝑆 ) → ( ( I ↾ 𝐹 ) LIndF 𝑋 ↔ ( I ↾ 𝐹 ) LIndF 𝑊 ) )
18 16 17 syl3an3br ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆 ) → ( ( I ↾ 𝐹 ) LIndF 𝑋 ↔ ( I ↾ 𝐹 ) LIndF 𝑊 ) )
19 14 18 anbi12d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆 ) → ( ( 𝐹 ⊆ ( Base ‘ 𝑋 ) ∧ ( I ↾ 𝐹 ) LIndF 𝑋 ) ↔ ( 𝐹 ⊆ ( Base ‘ 𝑊 ) ∧ ( I ↾ 𝐹 ) LIndF 𝑊 ) ) )
20 2 ovexi ⊢ 𝑋 ∈ V
21 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
22 21 islinds ⊢ ( 𝑋 ∈ V → ( 𝐹 ∈ ( LIndS ‘ 𝑋 ) ↔ ( 𝐹 ⊆ ( Base ‘ 𝑋 ) ∧ ( I ↾ 𝐹 ) LIndF 𝑋 ) ) )
23 20 22 mp1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆 ) → ( 𝐹 ∈ ( LIndS ‘ 𝑋 ) ↔ ( 𝐹 ⊆ ( Base ‘ 𝑋 ) ∧ ( I ↾ 𝐹 ) LIndF 𝑋 ) ) )
24 3 islinds ⊢ ( 𝑊 ∈ LMod → ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝐹 ⊆ ( Base ‘ 𝑊 ) ∧ ( I ↾ 𝐹 ) LIndF 𝑊 ) ) )
25 24 3ad2ant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆 ) → ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝐹 ⊆ ( Base ‘ 𝑊 ) ∧ ( I ↾ 𝐹 ) LIndF 𝑊 ) ) )
26 19 23 25 3bitr4d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ 𝑈 ∧ 𝐹 ⊆ 𝑆 ) → ( 𝐹 ∈ ( LIndS ‘ 𝑋 ) ↔ 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) )