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 = Base U
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 = Base U
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