Metamath Proof Explorer


Theorem lclkrlem2l

Description: Lemma for lclkr . Eliminate the X =/= .0. , Y =/= .0. hypotheses. (Contributed by NM, 18-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 ( 𝜑 → ( ¬ 𝑋 ∈ ( ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ‘ { 𝐵 } ) ) )
lclkrlem2l.x ( 𝜑𝑋𝑉 )
lclkrlem2l.y ( 𝜑𝑌𝑉 )
Assertion lclkrlem2l ( 𝜑 → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )

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 lclkrlem2l.x ( 𝜑𝑋𝑉 )
24 lclkrlem2l.y ( 𝜑𝑌𝑉 )
25 15 adantr ( ( 𝜑𝑋 = 0 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
26 16 adantr ( ( 𝜑𝑋 = 0 ) → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
27 17 adantr ( ( 𝜑𝑋 = 0 ) → 𝐸𝐹 )
28 18 adantr ( ( 𝜑𝑋 = 0 ) → 𝐺𝐹 )
29 19 adantr ( ( 𝜑𝑋 = 0 ) → ( 𝐿𝐸 ) = ( ‘ { 𝑋 } ) )
30 20 adantr ( ( 𝜑𝑋 = 0 ) → ( 𝐿𝐺 ) = ( ‘ { 𝑌 } ) )
31 21 adantr ( ( 𝜑𝑋 = 0 ) → ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 𝑄 )
32 22 adantr ( ( 𝜑𝑋 = 0 ) → ( ¬ 𝑋 ∈ ( ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ‘ { 𝐵 } ) ) )
33 simpr ( ( 𝜑𝑋 = 0 ) → 𝑋 = 0 )
34 24 adantr ( ( 𝜑𝑋 = 0 ) → 𝑌𝑉 )
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 25 26 27 28 29 30 31 32 33 34 lclkrlem2k ( ( 𝜑𝑋 = 0 ) → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
36 15 adantr ( ( 𝜑𝑌 = 0 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
37 16 adantr ( ( 𝜑𝑌 = 0 ) → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
38 17 adantr ( ( 𝜑𝑌 = 0 ) → 𝐸𝐹 )
39 18 adantr ( ( 𝜑𝑌 = 0 ) → 𝐺𝐹 )
40 19 adantr ( ( 𝜑𝑌 = 0 ) → ( 𝐿𝐸 ) = ( ‘ { 𝑋 } ) )
41 20 adantr ( ( 𝜑𝑌 = 0 ) → ( 𝐿𝐺 ) = ( ‘ { 𝑌 } ) )
42 21 adantr ( ( 𝜑𝑌 = 0 ) → ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 𝑄 )
43 22 adantr ( ( 𝜑𝑌 = 0 ) → ( ¬ 𝑋 ∈ ( ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ‘ { 𝐵 } ) ) )
44 23 adantr ( ( 𝜑𝑌 = 0 ) → 𝑋𝑉 )
45 simpr ( ( 𝜑𝑌 = 0 ) → 𝑌 = 0 )
46 1 2 3 4 5 6 7 8 9 10 11 12 13 14 36 37 38 39 40 41 42 43 44 45 lclkrlem2j ( ( 𝜑𝑌 = 0 ) → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
47 15 adantr ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
48 16 adantr ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → 𝐵 ∈ ( 𝑉 ∖ { 0 } ) )
49 17 adantr ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → 𝐸𝐹 )
50 18 adantr ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → 𝐺𝐹 )
51 19 adantr ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → ( 𝐿𝐸 ) = ( ‘ { 𝑋 } ) )
52 20 adantr ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → ( 𝐿𝐺 ) = ( ‘ { 𝑌 } ) )
53 21 adantr ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 𝑄 )
54 22 adantr ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → ( ¬ 𝑋 ∈ ( ‘ { 𝐵 } ) ∨ ¬ 𝑌 ∈ ( ‘ { 𝐵 } ) ) )
55 23 adantr ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → 𝑋𝑉 )
56 simprl ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → 𝑋0 )
57 eldifsn ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑋𝑉𝑋0 ) )
58 55 56 57 sylanbrc ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
59 24 adantr ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → 𝑌𝑉 )
60 simprr ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → 𝑌0 )
61 eldifsn ( 𝑌 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑌𝑉𝑌0 ) )
62 59 60 61 sylanbrc ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
63 1 2 3 4 5 6 7 8 9 10 11 12 13 14 47 48 49 50 51 52 53 54 58 62 lclkrlem2i ( ( 𝜑 ∧ ( 𝑋0𝑌0 ) ) → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
64 35 46 63 pm2.61da2ne ( 𝜑 → ( ‘ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )