Metamath Proof Explorer


Theorem hdmaprnlem3uN

Description: Part of proof of part 12 in Baer p. 49. (Contributed by NM, 29-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𝐶 )
Assertion hdmaprnlem3uN ( 𝜑 → ( 𝑁 ‘ { 𝑢 } ) ≠ ( 𝑀 ‘ ( 𝐿 ‘ { ( ( 𝑆𝑢 ) 𝑠 ) } ) ) )

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 eqid ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
20 1 2 9 dvhlmod ( 𝜑𝑈 ∈ LMod )
21 3 19 4 lspsncl ( ( 𝑈 ∈ LMod ∧ 𝑢𝑉 ) → ( 𝑁 ‘ { 𝑢 } ) ∈ ( LSubSp ‘ 𝑈 ) )
22 20 13 21 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑢 } ) ∈ ( LSubSp ‘ 𝑈 ) )
23 1 7 2 19 9 22 mapdcnvid1N ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) ) = ( 𝑁 ‘ { 𝑢 } ) )
24 1 2 3 4 5 6 7 8 9 13 hdmap10 ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) = ( 𝐿 ‘ { ( 𝑆𝑢 ) } ) )
25 1 5 9 lcdlvec ( 𝜑𝐶 ∈ LVec )
26 1 2 3 5 15 8 9 13 hdmapcl ( 𝜑 → ( 𝑆𝑢 ) ∈ 𝐷 )
27 1 2 3 4 5 6 7 8 9 10 11 12 13 14 hdmaprnlem1N ( 𝜑 → ( 𝐿 ‘ { ( 𝑆𝑢 ) } ) ≠ ( 𝐿 ‘ { 𝑠 } ) )
28 15 18 16 6 25 26 10 27 lspindp3 ( 𝜑 → ( 𝐿 ‘ { ( 𝑆𝑢 ) } ) ≠ ( 𝐿 ‘ { ( ( 𝑆𝑢 ) 𝑠 ) } ) )
29 24 28 eqnetrd ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) ≠ ( 𝐿 ‘ { ( ( 𝑆𝑢 ) 𝑠 ) } ) )
30 1 7 2 19 9 22 mapdcl ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) ∈ ran 𝑀 )
31 1 5 9 lcdlmod ( 𝜑𝐶 ∈ LMod )
32 10 eldifad ( 𝜑𝑠𝐷 )
33 15 18 lmodvacl ( ( 𝐶 ∈ LMod ∧ ( 𝑆𝑢 ) ∈ 𝐷𝑠𝐷 ) → ( ( 𝑆𝑢 ) 𝑠 ) ∈ 𝐷 )
34 31 26 32 33 syl3anc ( 𝜑 → ( ( 𝑆𝑢 ) 𝑠 ) ∈ 𝐷 )
35 eqid ( LSubSp ‘ 𝐶 ) = ( LSubSp ‘ 𝐶 )
36 15 35 6 lspsncl ( ( 𝐶 ∈ LMod ∧ ( ( 𝑆𝑢 ) 𝑠 ) ∈ 𝐷 ) → ( 𝐿 ‘ { ( ( 𝑆𝑢 ) 𝑠 ) } ) ∈ ( LSubSp ‘ 𝐶 ) )
37 31 34 36 syl2anc ( 𝜑 → ( 𝐿 ‘ { ( ( 𝑆𝑢 ) 𝑠 ) } ) ∈ ( LSubSp ‘ 𝐶 ) )
38 1 7 5 35 9 mapdrn2 ( 𝜑 → ran 𝑀 = ( LSubSp ‘ 𝐶 ) )
39 37 38 eleqtrrd ( 𝜑 → ( 𝐿 ‘ { ( ( 𝑆𝑢 ) 𝑠 ) } ) ∈ ran 𝑀 )
40 1 7 9 30 39 mapdcnv11N ( 𝜑 → ( ( 𝑀 ‘ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) ) = ( 𝑀 ‘ ( 𝐿 ‘ { ( ( 𝑆𝑢 ) 𝑠 ) } ) ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) = ( 𝐿 ‘ { ( ( 𝑆𝑢 ) 𝑠 ) } ) ) )
41 40 necon3bid ( 𝜑 → ( ( 𝑀 ‘ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) ) ≠ ( 𝑀 ‘ ( 𝐿 ‘ { ( ( 𝑆𝑢 ) 𝑠 ) } ) ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) ≠ ( 𝐿 ‘ { ( ( 𝑆𝑢 ) 𝑠 ) } ) ) )
42 29 41 mpbird ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) ) ≠ ( 𝑀 ‘ ( 𝐿 ‘ { ( ( 𝑆𝑢 ) 𝑠 ) } ) ) )
43 23 42 eqnetrrd ( 𝜑 → ( 𝑁 ‘ { 𝑢 } ) ≠ ( 𝑀 ‘ ( 𝐿 ‘ { ( ( 𝑆𝑢 ) 𝑠 ) } ) ) )