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 ⊢ U = LSubSp ⁡ W
lsslindf.x ⊢ X = W ↾ 𝑠 S
Assertion lsslinds ⊢ W ∈ LMod ∧ S ∈ U ∧ F ⊆ S → F ∈ LIndS ⁡ X ↔ F ∈ LIndS ⁡ W

Proof

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