Metamath Proof Explorer

Theorem hdmaprnlem1N

Description: Part of proof of part 12 in Baer p. 49 line 10, Gu' =/= Gs. Our ( N{ v } ) is Baer's T. (Contributed by NM, 26-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 ⊢ ( 𝜑 → ¬ 𝑢 ∈ ( 𝑁 ‘ { 𝑣 } ) )
Assertion hdmaprnlem1N ( 𝜑 → ( 𝐿 ‘ { ( 𝑆 ‘ 𝑢 ) } ) ≠ ( 𝐿 ‘ { 𝑠 } ) )

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 1 2 9 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
16 3 4 15 13 11 14 lspsnne2 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑢 } ) ≠ ( 𝑁 ‘ { 𝑣 } ) )
17 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
18 3 17 4 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑢 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑢 } ) ∈ ( LSubSp ‘ 𝑈 ) )
19 15 13 18 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑢 } ) ∈ ( LSubSp ‘ 𝑈 ) )
20 3 17 4 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑣 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑣 } ) ∈ ( LSubSp ‘ 𝑈 ) )
21 15 11 20 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑣 } ) ∈ ( LSubSp ‘ 𝑈 ) )
22 1 2 17 7 9 19 21 mapd11 ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) = ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) ↔ ( 𝑁 ‘ { 𝑢 } ) = ( 𝑁 ‘ { 𝑣 } ) ) )
23 22 necon3bid ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) ≠ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) ↔ ( 𝑁 ‘ { 𝑢 } ) ≠ ( 𝑁 ‘ { 𝑣 } ) ) )
24 16 23 mpbird ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) ≠ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) )
25 1 2 3 4 5 6 7 8 9 13 hdmap10 ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑢 } ) ) = ( 𝐿 ‘ { ( 𝑆 ‘ 𝑢 ) } ) )
26 24 25 12 3netr3d ⊢ ( 𝜑 → ( 𝐿 ‘ { ( 𝑆 ‘ 𝑢 ) } ) ≠ ( 𝐿 ‘ { 𝑠 } ) )