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 ⊢H=LHyp⁡K
hdmaprnlem1.u ⊢U=DVecH⁡K⁡W
hdmaprnlem1.v ⊢V=BaseU
hdmaprnlem1.n ⊢N=LSpan⁡U
hdmaprnlem1.c ⊢C=LCDual⁡K⁡W
hdmaprnlem1.l ⊢L=LSpan⁡C
hdmaprnlem1.m ⊢M=mapd⁡K⁡W
hdmaprnlem1.s ⊢S=HDMap⁡K⁡W
hdmaprnlem1.k ⊢φ→K∈HL∧W∈H
hdmaprnlem1.se ⊢φ→s∈D∖Q
hdmaprnlem1.ve ⊢φ→v∈V
hdmaprnlem1.e ⊢φ→M⁡N⁡v=L⁡s
hdmaprnlem1.ue ⊢φ→u∈V
hdmaprnlem1.un ⊢φ→¬u∈N⁡v
Assertion hdmaprnlem1N ⊢φ→L⁡S⁡u≠L⁡s

Proof

Step Hyp Ref Expression
1 hdmaprnlem1.h ⊢H=LHyp⁡K
2 hdmaprnlem1.u ⊢U=DVecH⁡K⁡W
3 hdmaprnlem1.v ⊢V=BaseU
4 hdmaprnlem1.n ⊢N=LSpan⁡U
5 hdmaprnlem1.c ⊢C=LCDual⁡K⁡W
6 hdmaprnlem1.l ⊢L=LSpan⁡C
7 hdmaprnlem1.m ⊢M=mapd⁡K⁡W
8 hdmaprnlem1.s ⊢S=HDMap⁡K⁡W
9 hdmaprnlem1.k ⊢φ→K∈HL∧W∈H
10 hdmaprnlem1.se ⊢φ→s∈D∖Q
11 hdmaprnlem1.ve ⊢φ→v∈V
12 hdmaprnlem1.e ⊢φ→M⁡N⁡v=L⁡s
13 hdmaprnlem1.ue ⊢φ→u∈V
14 hdmaprnlem1.un ⊢φ→¬u∈N⁡v
15 1 2 9 dvhlmod ⊢φ→U∈LMod
16 3 4 15 13 11 14 lspsnne2 ⊢φ→N⁡u≠N⁡v
17 eqid ⊢LSubSp⁡U=LSubSp⁡U
18 3 17 4 lspsncl ⊢U∈LMod∧u∈V→N⁡u∈LSubSp⁡U
19 15 13 18 syl2anc ⊢φ→N⁡u∈LSubSp⁡U
20 3 17 4 lspsncl ⊢U∈LMod∧v∈V→N⁡v∈LSubSp⁡U
21 15 11 20 syl2anc ⊢φ→N⁡v∈LSubSp⁡U
22 1 2 17 7 9 19 21 mapd11 ⊢φ→M⁡N⁡u=M⁡N⁡v↔N⁡u=N⁡v
23 22 necon3bid ⊢φ→M⁡N⁡u≠M⁡N⁡v↔N⁡u≠N⁡v
24 16 23 mpbird ⊢φ→M⁡N⁡u≠M⁡N⁡v
25 1 2 3 4 5 6 7 8 9 13 hdmap10 ⊢φ→M⁡N⁡u=L⁡S⁡u
26 24 25 12 3netr3d ⊢φ→L⁡S⁡u≠L⁡s