Metamath Proof Explorer

Theorem lclkrlem2n

Description: Lemma for lclkr . (Contributed by NM, 12-Jan-2015)

Ref Expression
Hypotheses lclkrlem2m.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
lclkrlem2m.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
lclkrlem2m.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
lclkrlem2m.q ⊢ × = ( .r ‘ 𝑆 )
lclkrlem2m.z ⊢ 0 = ( 0g ‘ 𝑆 )
lclkrlem2m.i ⊢ 𝐼 = ( invr ‘ 𝑆 )
lclkrlem2m.m ⊢ − = ( -g ‘ 𝑈 )
lclkrlem2m.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
lclkrlem2m.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
lclkrlem2m.p ⊢ + = ( +g ‘ 𝐷 )
lclkrlem2m.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lclkrlem2m.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lclkrlem2m.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
lclkrlem2m.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lclkrlem2n.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
lclkrlem2n.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
lclkrlem2n.w ⊢ ( 𝜑 → 𝑈 ∈ LVec )
lclkrlem2n.j ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = 0 )
lclkrlem2n.k ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = 0 )
Assertion lclkrlem2n ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 lclkrlem2m.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
2 lclkrlem2m.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
3 lclkrlem2m.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
4 lclkrlem2m.q ⊢ × = ( .r ‘ 𝑆 )
5 lclkrlem2m.z ⊢ 0 = ( 0g ‘ 𝑆 )
6 lclkrlem2m.i ⊢ 𝐼 = ( invr ‘ 𝑆 )
7 lclkrlem2m.m ⊢ − = ( -g ‘ 𝑈 )
8 lclkrlem2m.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
9 lclkrlem2m.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
10 lclkrlem2m.p ⊢ + = ( +g ‘ 𝐷 )
11 lclkrlem2m.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
12 lclkrlem2m.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
13 lclkrlem2m.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
14 lclkrlem2m.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
15 lclkrlem2n.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
16 lclkrlem2n.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
17 lclkrlem2n.w ⊢ ( 𝜑 → 𝑈 ∈ LVec )
18 lclkrlem2n.j ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = 0 )
19 lclkrlem2n.k ⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = 0 )
20 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
21 lveclmod ⊢ ( 𝑈 ∈ LVec → 𝑈 ∈ LMod )
22 17 21 syl ⊢ ( 𝜑 → 𝑈 ∈ LMod )
23 8 9 10 22 13 14 ldualvaddcl ⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 )
24 8 16 20 lkrlss ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ) → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
25 22 23 24 syl2anc ⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
26 1 3 5 8 16 17 23 11 ellkr2 ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ↔ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) = 0 ) )
27 18 26 mpbird ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
28 1 3 5 8 16 17 23 12 ellkr2 ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ↔ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) = 0 ) )
29 19 28 mpbird ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
30 20 15 22 25 27 29 lspprss ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )