Metamath Proof Explorer

Theorem hdmaprnlem9N

Description: Part of proof of part 12 in Baer p. 49 line 21, s=S(t). TODO: we seem to be going back and forth with mapd11 and mapdcnv11N . Use better hypotheses and/or theorems? (Contributed by NM, 27-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hdmaprnlem1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmaprnlem1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmaprnlem1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmaprnlem1.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
hdmaprnlem1.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmaprnlem1.l ⊢ 𝐿 = ( LSpan ‘ 𝐶 )
hdmaprnlem1.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
hdmaprnlem1.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmaprnlem1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmaprnlem1.se ⊢ ( 𝜑 → 𝑠 ∈ ( 𝐷 ∖ { 𝑄 } ) )
hdmaprnlem1.ve ⊢ ( 𝜑 → 𝑣 ∈ 𝑉 )
hdmaprnlem1.e ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )
hdmaprnlem1.ue ⊢ ( 𝜑 → 𝑢 ∈ 𝑉 )
hdmaprnlem1.un ⊢ ( 𝜑 → ¬ 𝑢 ∈ ( 𝑁 ‘ { 𝑣 } ) )
hdmaprnlem1.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
hdmaprnlem1.q ⊢ 𝑄 = ( 0g ‘ 𝐶 )
hdmaprnlem1.o ⊢ 0 = ( 0g ‘ 𝑈 )
hdmaprnlem1.a ⊢ ✚ = ( +g ‘ 𝐶 )
hdmaprnlem1.t2 ⊢ ( 𝜑 → 𝑡 ∈ ( ( 𝑁 ‘ { 𝑣 } ) ∖ { 0 } ) )
hdmaprnlem1.p ⊢ + = ( +g ‘ 𝑈 )
hdmaprnlem1.pt ⊢ ( 𝜑 → ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) = ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑢 + 𝑡 ) } ) ) )
Assertion hdmaprnlem9N ( 𝜑 → 𝑠 = ( 𝑆 ‘ 𝑡 ) )

Proof

Step Hyp Ref Expression
1 hdmaprnlem1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmaprnlem1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmaprnlem1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmaprnlem1.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5 hdmaprnlem1.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6 hdmaprnlem1.l ⊢ 𝐿 = ( LSpan ‘ 𝐶 )
7 hdmaprnlem1.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
8 hdmaprnlem1.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
9 hdmaprnlem1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 hdmaprnlem1.se ⊢ ( 𝜑 → 𝑠 ∈ ( 𝐷 ∖ { 𝑄 } ) )
11 hdmaprnlem1.ve ⊢ ( 𝜑 → 𝑣 ∈ 𝑉 )
12 hdmaprnlem1.e ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )
13 hdmaprnlem1.ue ⊢ ( 𝜑 → 𝑢 ∈ 𝑉 )
14 hdmaprnlem1.un ⊢ ( 𝜑 → ¬ 𝑢 ∈ ( 𝑁 ‘ { 𝑣 } ) )
15 hdmaprnlem1.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
16 hdmaprnlem1.q ⊢ 𝑄 = ( 0g ‘ 𝐶 )
17 hdmaprnlem1.o ⊢ 0 = ( 0g ‘ 𝑈 )
18 hdmaprnlem1.a ⊢ ✚ = ( +g ‘ 𝐶 )
19 hdmaprnlem1.t2 ⊢ ( 𝜑 → 𝑡 ∈ ( ( 𝑁 ‘ { 𝑣 } ) ∖ { 0 } ) )
20 hdmaprnlem1.p ⊢ + = ( +g ‘ 𝑈 )
21 hdmaprnlem1.pt ⊢ ( 𝜑 → ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) = ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑢 + 𝑡 ) } ) ) )
22 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 hdmaprnlem7N ⊢ ( 𝜑 → ( 𝑠 ( -g ‘ 𝐶 ) ( 𝑆 ‘ 𝑡 ) ) ∈ ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) )
23 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 hdmaprnlem8N ⊢ ( 𝜑 → ( 𝑠 ( -g ‘ 𝐶 ) ( 𝑆 ‘ 𝑡 ) ) ∈ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑡 } ) ) )
24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 hdmaprnlem4N ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑡 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )
25 23 24 eleqtrd ⊢ ( 𝜑 → ( 𝑠 ( -g ‘ 𝐶 ) ( 𝑆 ‘ 𝑡 ) ) ∈ ( 𝐿 ‘ { 𝑠 } ) )
26 22 25 elind ⊢ ( 𝜑 → ( 𝑠 ( -g ‘ 𝐶 ) ( 𝑆 ‘ 𝑡 ) ) ∈ ( ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) ∩ ( 𝐿 ‘ { 𝑠 } ) ) )
27 1 5 9 lcdlvec ⊢ ( 𝜑 → 𝐶 ∈ LVec )
28 1 5 9 lcdlmod ⊢ ( 𝜑 → 𝐶 ∈ LMod )
29 1 2 3 5 15 8 9 13 hdmapcl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑢 ) ∈ 𝐷 )
30 10 eldifad ⊢ ( 𝜑 → 𝑠 ∈ 𝐷 )
31 15 18 lmodvacl ⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑆 ‘ 𝑢 ) ∈ 𝐷 ∧ 𝑠 ∈ 𝐷 ) → ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) ∈ 𝐷 )
32 28 29 30 31 syl3anc ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) ∈ 𝐷 )
33 eqid ⊢ ( LSubSp ‘ 𝐶 ) = ( LSubSp ‘ 𝐶 )
34 15 33 6 lspsncl ⊢ ( ( 𝐶 ∈ LMod ∧ 𝑠 ∈ 𝐷 ) → ( 𝐿 ‘ { 𝑠 } ) ∈ ( LSubSp ‘ 𝐶 ) )
35 28 30 34 syl2anc ⊢ ( 𝜑 → ( 𝐿 ‘ { 𝑠 } ) ∈ ( LSubSp ‘ 𝐶 ) )
36 1 7 5 33 9 mapdrn2 ⊢ ( 𝜑 → ran 𝑀 = ( LSubSp ‘ 𝐶 ) )
37 35 36 eleqtrrd ⊢ ( 𝜑 → ( 𝐿 ‘ { 𝑠 } ) ∈ ran 𝑀 )
38 1 7 9 37 mapdcnvid2 ⊢ ( 𝜑 → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) ) = ( 𝐿 ‘ { 𝑠 } ) )
39 12 38 eqtr4d ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) ) )
40 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
41 1 2 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
42 3 40 4 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑣 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑣 } ) ∈ ( LSubSp ‘ 𝑈 ) )
43 41 11 42 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑣 } ) ∈ ( LSubSp ‘ 𝑈 ) )
44 1 7 2 40 9 37 mapdcnvcl ⊢ ( 𝜑 → ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
45 1 2 40 7 9 43 44 mapd11 ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) ) ↔ ( 𝑁 ‘ { 𝑣 } ) = ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) ) )
46 39 45 mpbid ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑣 } ) = ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) )
47 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 hdmaprnlem3N ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑣 } ) ≠ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) ) )
48 46 47 eqnetrrd ⊢ ( 𝜑 → ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) ≠ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) ) )
49 15 33 6 lspsncl ⊢ ( ( 𝐶 ∈ LMod ∧ ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) ∈ 𝐷 ) → ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) ∈ ( LSubSp ‘ 𝐶 ) )
50 28 32 49 syl2anc ⊢ ( 𝜑 → ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) ∈ ( LSubSp ‘ 𝐶 ) )
51 50 36 eleqtrrd ⊢ ( 𝜑 → ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) ∈ ran 𝑀 )
52 1 7 9 37 51 mapdcnv11N ⊢ ( 𝜑 → ( ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) = ( ◡ 𝑀 ‘ ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) ) ↔ ( 𝐿 ‘ { 𝑠 } ) = ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) ) )
53 52 necon3bid ⊢ ( 𝜑 → ( ( ◡ 𝑀 ‘ ( 𝐿 ‘ { 𝑠 } ) ) ≠ ( ◡ 𝑀 ‘ ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) ) ↔ ( 𝐿 ‘ { 𝑠 } ) ≠ ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) ) )
54 48 53 mpbid ⊢ ( 𝜑 → ( 𝐿 ‘ { 𝑠 } ) ≠ ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) )
55 54 necomd ⊢ ( 𝜑 → ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) ≠ ( 𝐿 ‘ { 𝑠 } ) )
56 15 16 6 27 32 30 55 lspdisj2 ⊢ ( 𝜑 → ( ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) ∩ ( 𝐿 ‘ { 𝑠 } ) ) = { 𝑄 } )
57 26 56 eleqtrd ⊢ ( 𝜑 → ( 𝑠 ( -g ‘ 𝐶 ) ( 𝑆 ‘ 𝑡 ) ) ∈ { 𝑄 } )
58 elsni ⊢ ( ( 𝑠 ( -g ‘ 𝐶 ) ( 𝑆 ‘ 𝑡 ) ) ∈ { 𝑄 } → ( 𝑠 ( -g ‘ 𝐶 ) ( 𝑆 ‘ 𝑡 ) ) = 𝑄 )
59 57 58 syl ⊢ ( 𝜑 → ( 𝑠 ( -g ‘ 𝐶 ) ( 𝑆 ‘ 𝑡 ) ) = 𝑄 )
60 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 hdmaprnlem4tN ⊢ ( 𝜑 → 𝑡 ∈ 𝑉 )
61 1 2 3 5 15 8 9 60 hdmapcl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑡 ) ∈ 𝐷 )
62 eqid ⊢ ( -g ‘ 𝐶 ) = ( -g ‘ 𝐶 )
63 15 16 62 lmodsubeq0 ⊢ ( ( 𝐶 ∈ LMod ∧ 𝑠 ∈ 𝐷 ∧ ( 𝑆 ‘ 𝑡 ) ∈ 𝐷 ) → ( ( 𝑠 ( -g ‘ 𝐶 ) ( 𝑆 ‘ 𝑡 ) ) = 𝑄 ↔ 𝑠 = ( 𝑆 ‘ 𝑡 ) ) )
64 28 30 61 63 syl3anc ⊢ ( 𝜑 → ( ( 𝑠 ( -g ‘ 𝐶 ) ( 𝑆 ‘ 𝑡 ) ) = 𝑄 ↔ 𝑠 = ( 𝑆 ‘ 𝑡 ) ) )
65 59 64 mpbid ⊢ ( 𝜑 → 𝑠 = ( 𝑆 ‘ 𝑡 ) )