Metamath Proof Explorer


Theorem hdmap1eulem

Description: Lemma for hdmap1eu . TODO: combine with hdmap1eu or at least share some hypotheses. (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmap1eulem.h 𝐻 = ( LHyp ‘ 𝐾 )
hdmap1eulem.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmap1eulem.v 𝑉 = ( Base ‘ 𝑈 )
hdmap1eulem.s = ( -g𝑈 )
hdmap1eulem.o 0 = ( 0g𝑈 )
hdmap1eulem.n 𝑁 = ( LSpan ‘ 𝑈 )
hdmap1eulem.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmap1eulem.d 𝐷 = ( Base ‘ 𝐶 )
hdmap1eulem.r 𝑅 = ( -g𝐶 )
hdmap1eulem.q 𝑄 = ( 0g𝐶 )
hdmap1eulem.j 𝐽 = ( LSpan ‘ 𝐶 )
hdmap1eulem.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
hdmap1eulem.i 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
hdmap1eulem.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hdmap1eulem.mn ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐹 } ) )
hdmap1eulem.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
hdmap1eulem.f ( 𝜑𝐹𝐷 )
hdmap1eulem.y ( 𝜑𝑇𝑉 )
hdmap1eulem.l 𝐿 = ( 𝑥 ∈ V ↦ if ( ( 2nd𝑥 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ) ) ) )
Assertion hdmap1eulem ( 𝜑 → ∃! 𝑦𝐷𝑧𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 hdmap1eulem.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmap1eulem.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmap1eulem.v 𝑉 = ( Base ‘ 𝑈 )
4 hdmap1eulem.s = ( -g𝑈 )
5 hdmap1eulem.o 0 = ( 0g𝑈 )
6 hdmap1eulem.n 𝑁 = ( LSpan ‘ 𝑈 )
7 hdmap1eulem.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
8 hdmap1eulem.d 𝐷 = ( Base ‘ 𝐶 )
9 hdmap1eulem.r 𝑅 = ( -g𝐶 )
10 hdmap1eulem.q 𝑄 = ( 0g𝐶 )
11 hdmap1eulem.j 𝐽 = ( LSpan ‘ 𝐶 )
12 hdmap1eulem.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
13 hdmap1eulem.i 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
14 hdmap1eulem.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
15 hdmap1eulem.mn ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐹 } ) )
16 hdmap1eulem.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
17 hdmap1eulem.f ( 𝜑𝐹𝐷 )
18 hdmap1eulem.y ( 𝜑𝑇𝑉 )
19 hdmap1eulem.l 𝐿 = ( 𝑥 ∈ V ↦ if ( ( 2nd𝑥 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ) ) ) )
20 1 2 3 4 5 6 7 8 9 10 11 12 19 14 17 15 16 18 mapdh9a ( 𝜑 → ∃! 𝑦𝐷𝑧𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐿 ‘ ⟨ 𝑧 , ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) )
21 14 ad2antrr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
22 16 ad2antrr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
23 17 ad2antrr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) → 𝐹𝐷 )
24 simplr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) → 𝑧𝑉 )
25 1 2 3 4 5 6 7 8 9 10 11 12 13 21 22 23 24 19 hdmap1valc ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) = ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) )
26 25 oteq2d ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) → ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ = ⟨ 𝑧 , ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ )
27 26 fveq2d ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) → ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) )
28 elun1 ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) → 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) )
29 28 con3i ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) )
30 14 ad2antrr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
31 eqid ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
32 1 2 14 dvhlmod ( 𝜑𝑈 ∈ LMod )
33 32 ad2antrr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑈 ∈ LMod )
34 16 eldifad ( 𝜑𝑋𝑉 )
35 34 ad2antrr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑋𝑉 )
36 3 31 6 lspsncl ( ( 𝑈 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
37 33 35 36 syl2anc ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
38 simplr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑧𝑉 )
39 simpr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) )
40 5 31 33 37 38 39 lssneln0 ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑧 ∈ ( 𝑉 ∖ { 0 } ) )
41 17 ad2antrr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → 𝐹𝐷 )
42 15 ad2antrr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { 𝐹 } ) )
43 16 ad2antrr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
44 3 6 33 38 35 39 lspsnne2 ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) )
45 44 necomd ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑧 } ) )
46 10 19 1 12 2 3 4 5 6 7 8 9 11 30 41 42 43 38 45 mapdhcl ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) ∈ 𝐷 )
47 18 ad2antrr ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → 𝑇𝑉 )
48 1 2 3 4 5 6 7 8 9 10 11 12 13 30 40 46 47 19 hdmap1valc ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) = ( 𝐿 ‘ ⟨ 𝑧 , ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) )
49 29 48 sylan2 ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) → ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) = ( 𝐿 ‘ ⟨ 𝑧 , ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) )
50 27 49 eqtrd ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) → ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) = ( 𝐿 ‘ ⟨ 𝑧 , ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) )
51 50 eqeq2d ( ( ( 𝜑𝑧𝑉 ) ∧ ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) → ( 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) ↔ 𝑦 = ( 𝐿 ‘ ⟨ 𝑧 , ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) )
52 51 pm5.74da ( ( 𝜑𝑧𝑉 ) → ( ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ↔ ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐿 ‘ ⟨ 𝑧 , ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) )
53 52 ralbidva ( 𝜑 → ( ∀ 𝑧𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ↔ ∀ 𝑧𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐿 ‘ ⟨ 𝑧 , ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) )
54 53 reubidv ( 𝜑 → ( ∃! 𝑦𝐷𝑧𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ↔ ∃! 𝑦𝐷𝑧𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐿 ‘ ⟨ 𝑧 , ( 𝐿 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) )
55 20 54 mpbird ( 𝜑 → ∃! 𝑦𝐷𝑧𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) )