Metamath Proof Explorer

Theorem islinds3

Description: A subset is linearly independent iff it is a basis of its span. (Contributed by Stefan O'Rear, 25-Feb-2015)

Ref Expression
Hypotheses islinds3.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
islinds3.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
islinds3.x ⊢ 𝑋 = ( 𝑊 ↾s ( 𝐾 ‘ 𝑌 ) )
islinds3.j ⊢ 𝐽 = ( LBasis ‘ 𝑋 )
Assertion islinds3 ( 𝑊 ∈ LMod → ( 𝑌 ∈ ( LIndS ‘ 𝑊 ) ↔ 𝑌 ∈ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 islinds3.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 islinds3.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
3 islinds3.x ⊢ 𝑋 = ( 𝑊 ↾s ( 𝐾 ‘ 𝑌 ) )
4 islinds3.j ⊢ 𝐽 = ( LBasis ‘ 𝑋 )
5 1 linds1 ⊢ ( 𝑌 ∈ ( LIndS ‘ 𝑊 ) → 𝑌 ⊆ 𝐵 )
6 5 a1i ⊢ ( 𝑊 ∈ LMod → ( 𝑌 ∈ ( LIndS ‘ 𝑊 ) → 𝑌 ⊆ 𝐵 ) )
7 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
8 7 linds1 ⊢ ( 𝑌 ∈ ( LIndS ‘ 𝑋 ) → 𝑌 ⊆ ( Base ‘ 𝑋 ) )
9 3 1 ressbasss ⊢ ( Base ‘ 𝑋 ) ⊆ 𝐵
10 8 9 sstrdi ⊢ ( 𝑌 ∈ ( LIndS ‘ 𝑋 ) → 𝑌 ⊆ 𝐵 )
11 10 adantr ⊢ ( ( 𝑌 ∈ ( LIndS ‘ 𝑋 ) ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑌 ) = ( Base ‘ 𝑋 ) ) → 𝑌 ⊆ 𝐵 )
12 11 a1i ⊢ ( 𝑊 ∈ LMod → ( ( 𝑌 ∈ ( LIndS ‘ 𝑋 ) ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑌 ) = ( Base ‘ 𝑋 ) ) → 𝑌 ⊆ 𝐵 ) )
13 simpl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ⊆ 𝐵 ) → 𝑊 ∈ LMod )
14 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
15 1 14 2 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝑊 ) )
16 1 2 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ⊆ 𝐵 ) → 𝑌 ⊆ ( 𝐾 ‘ 𝑌 ) )
17 eqid ⊢ ( LSpan ‘ 𝑋 ) = ( LSpan ‘ 𝑋 )
18 3 2 17 14 lsslsp ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐾 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑌 ⊆ ( 𝐾 ‘ 𝑌 ) ) → ( 𝐾 ‘ 𝑌 ) = ( ( LSpan ‘ 𝑋 ) ‘ 𝑌 ) )
19 13 15 16 18 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝑌 ) = ( ( LSpan ‘ 𝑋 ) ‘ 𝑌 ) )
20 1 2 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝑌 ) ⊆ 𝐵 )
21 3 1 ressbas2 ⊢ ( ( 𝐾 ‘ 𝑌 ) ⊆ 𝐵 → ( 𝐾 ‘ 𝑌 ) = ( Base ‘ 𝑋 ) )
22 20 21 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝑌 ) = ( Base ‘ 𝑋 ) )
23 19 22 eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ⊆ 𝐵 ) → ( ( LSpan ‘ 𝑋 ) ‘ 𝑌 ) = ( Base ‘ 𝑋 ) )
24 23 biantrud ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ⊆ 𝐵 ) → ( 𝑌 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑌 ∈ ( LIndS ‘ 𝑊 ) ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑌 ) = ( Base ‘ 𝑋 ) ) ) )
25 14 3 lsslinds ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐾 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑌 ⊆ ( 𝐾 ‘ 𝑌 ) ) → ( 𝑌 ∈ ( LIndS ‘ 𝑋 ) ↔ 𝑌 ∈ ( LIndS ‘ 𝑊 ) ) )
26 13 15 16 25 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ⊆ 𝐵 ) → ( 𝑌 ∈ ( LIndS ‘ 𝑋 ) ↔ 𝑌 ∈ ( LIndS ‘ 𝑊 ) ) )
27 26 bicomd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ⊆ 𝐵 ) → ( 𝑌 ∈ ( LIndS ‘ 𝑊 ) ↔ 𝑌 ∈ ( LIndS ‘ 𝑋 ) ) )
28 27 anbi1d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ⊆ 𝐵 ) → ( ( 𝑌 ∈ ( LIndS ‘ 𝑊 ) ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑌 ) = ( Base ‘ 𝑋 ) ) ↔ ( 𝑌 ∈ ( LIndS ‘ 𝑋 ) ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑌 ) = ( Base ‘ 𝑋 ) ) ) )
29 24 28 bitrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ⊆ 𝐵 ) → ( 𝑌 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑌 ∈ ( LIndS ‘ 𝑋 ) ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑌 ) = ( Base ‘ 𝑋 ) ) ) )
30 29 ex ⊢ ( 𝑊 ∈ LMod → ( 𝑌 ⊆ 𝐵 → ( 𝑌 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑌 ∈ ( LIndS ‘ 𝑋 ) ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑌 ) = ( Base ‘ 𝑋 ) ) ) ) )
31 6 12 30 pm5.21ndd ⊢ ( 𝑊 ∈ LMod → ( 𝑌 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑌 ∈ ( LIndS ‘ 𝑋 ) ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑌 ) = ( Base ‘ 𝑋 ) ) ) )
32 7 4 17 islbs4 ⊢ ( 𝑌 ∈ 𝐽 ↔ ( 𝑌 ∈ ( LIndS ‘ 𝑋 ) ∧ ( ( LSpan ‘ 𝑋 ) ‘ 𝑌 ) = ( Base ‘ 𝑋 ) ) )
33 31 32 bitr4di ⊢ ( 𝑊 ∈ LMod → ( 𝑌 ∈ ( LIndS ‘ 𝑊 ) ↔ 𝑌 ∈ 𝐽 ) )