Metamath Proof Explorer


Theorem lclkrlem2h

Description: Lemma for lclkr . Eliminate the ( L( E .+ G ) ) e. J hypothesis. (Contributed by NM, 16-Jan-2015)

Ref Expression
Hypotheses lclkrlem2f.h 𝐻 = ( LHyp ‘ 𝐾 )
lclkrlem2f.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2f.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lclkrlem2f.v 𝑉 = ( Base ‘ 𝑈 )
lclkrlem2f.s 𝑆 = ( Scalar ‘ 𝑈 )
lclkrlem2f.q 𝑄 = ( 0g𝑆 )
lclkrlem2f.z 0 = ( 0g𝑈 )
lclkrlem2f.a = ( LSSum ‘ 𝑈 )
lclkrlem2f.n 𝑁 = ( LSpan ‘ 𝑈 )
lclkrlem2f.f 𝐹 = ( LFnl ‘ 𝑈 )
lclkrlem2f.j 𝐽 = ( LSHyp ‘ 𝑈 )
lclkrlem2f.l 𝐿 = ( LKer ‘ 𝑈 )
lclkrlem2f.d 𝐷 = ( LDual ‘ 𝑈 )
lclkrlem2f.p + = ( +g𝐷 )
lclkrlem2f.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
lclkrlem2f.b ( 𝜑𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2f.e ( 𝜑𝐸𝐹 )
lclkrlem2f.g ( 𝜑𝐺𝐹 )
lclkrlem2f.le ( 𝜑 → ( 𝐿𝐸 ) = ( ‘ { 𝑋 } ) )
lclkrlem2f.lg ( 𝜑 → ( 𝐿𝐺 ) = ( ‘ { 𝑌 } ) )
lclkrlem2f.kb ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 𝑄 )
lclkrlem2f.nx ( 𝜑 → ( ¬ 𝑋 ∈ ( ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ‘ { 𝐵 } ) ) )
lclkrlem2h.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2h.y ( 𝜑𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
lclkrlem2h.ne ( 𝜑 → ( 𝐿𝐸 ) ≠ ( 𝐿𝐺 ) )
Assertion lclkrlem2h ( 𝜑 → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 lclkrlem2f.h 𝐻 = ( LHyp ‘ 𝐾 )
2 lclkrlem2f.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lclkrlem2f.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lclkrlem2f.v 𝑉 = ( Base ‘ 𝑈 )
5 lclkrlem2f.s 𝑆 = ( Scalar ‘ 𝑈 )
6 lclkrlem2f.q 𝑄 = ( 0g𝑆 )
7 lclkrlem2f.z 0 = ( 0g𝑈 )
8 lclkrlem2f.a = ( LSSum ‘ 𝑈 )
9 lclkrlem2f.n 𝑁 = ( LSpan ‘ 𝑈 )
10 lclkrlem2f.f 𝐹 = ( LFnl ‘ 𝑈 )
11 lclkrlem2f.j 𝐽 = ( LSHyp ‘ 𝑈 )
12 lclkrlem2f.l 𝐿 = ( LKer ‘ 𝑈 )
13 lclkrlem2f.d 𝐷 = ( LDual ‘ 𝑈 )
14 lclkrlem2f.p + = ( +g𝐷 )
15 lclkrlem2f.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
16 lclkrlem2f.b ( 𝜑𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
17 lclkrlem2f.e ( 𝜑𝐸𝐹 )
18 lclkrlem2f.g ( 𝜑𝐺𝐹 )
19 lclkrlem2f.le ( 𝜑 → ( 𝐿𝐸 ) = ( ‘ { 𝑋 } ) )
20 lclkrlem2f.lg ( 𝜑 → ( 𝐿𝐺 ) = ( ‘ { 𝑌 } ) )
21 lclkrlem2f.kb ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 𝑄 )
22 lclkrlem2f.nx ( 𝜑 → ( ¬ 𝑋 ∈ ( ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ‘ { 𝐵 } ) ) )
23 lclkrlem2h.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
24 lclkrlem2h.y ( 𝜑𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
25 lclkrlem2h.ne ( 𝜑 → ( 𝐿𝐸 ) ≠ ( 𝐿𝐺 ) )
26 15 adantr ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
27 16 adantr ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
28 17 adantr ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → 𝐸𝐹 )
29 18 adantr ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → 𝐺𝐹 )
30 19 adantr ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( 𝐿𝐸 ) = ( ‘ { 𝑋 } ) )
31 20 adantr ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( 𝐿𝐺 ) = ( ‘ { 𝑌 } ) )
32 21 adantr ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 𝑄 )
33 22 adantr ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( ¬ 𝑋 ∈ ( ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ‘ { 𝐵 } ) ) )
34 23 adantr ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
35 24 adantr ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
36 25 adantr ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( 𝐿𝐸 ) ≠ ( 𝐿𝐺 ) )
37 simpr ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 )
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 26 27 28 29 30 31 32 33 34 35 36 37 lclkrlem2g ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
39 1 3 2 4 15 dochoc1 ( 𝜑 → ( ‘ ( 𝑉 ) ) = 𝑉 )
40 39 adantr ( ( 𝜑 ∧ ¬ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( ‘ ( 𝑉 ) ) = 𝑉 )
41 1 3 15 dvhlvec ( 𝜑𝑈 ∈ LVec )
42 1 3 15 dvhlmod ( 𝜑𝑈 ∈ LMod )
43 10 13 14 42 17 18 ldualvaddcl ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 )
44 4 11 10 12 41 43 lkrshpor ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ∨ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 ) )
45 44 orcanai ( ( 𝜑 ∧ ¬ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) = 𝑉 )
46 45 fveq2d ( ( 𝜑 ∧ ¬ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) = ( 𝑉 ) )
47 46 fveq2d ( ( 𝜑 ∧ ¬ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( ‘ ( 𝑉 ) ) )
48 40 47 45 3eqtr4d ( ( 𝜑 ∧ ¬ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ∈ 𝐽 ) → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
49 38 48 pm2.61dan ( 𝜑 → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )