Metamath Proof Explorer

Theorem hdmapeq0

Description: Part of proof of part 12 in Baer p. 49 line 3. (Contributed by NM, 22-May-2015)

Ref Expression
Hypotheses hdmap12a.h ⊢ H = LHyp ⁡ K
hdmap12a.u ⊢ U = DVecH ⁡ K ⁡ W
hdmap12a.v ⊢ V = Base U
hdmap12a.o ⊢ 0 ˙ = 0 U
hdmap12a.c ⊢ C = LCDual ⁡ K ⁡ W
hdmap12a.q ⊢ Q = 0 C
hdmap12a.s ⊢ S = HDMap ⁡ K ⁡ W
hdmap12a.k ⊢ φ → K ∈ HL ∧ W ∈ H
hdmap12a.x ⊢ φ → T ∈ V
Assertion hdmapeq0 ⊢ φ → S ⁡ T = Q ↔ T = 0 ˙

Proof

Step Hyp Ref Expression
1 hdmap12a.h ⊢ H = LHyp ⁡ K
2 hdmap12a.u ⊢ U = DVecH ⁡ K ⁡ W
3 hdmap12a.v ⊢ V = Base U
4 hdmap12a.o ⊢ 0 ˙ = 0 U
5 hdmap12a.c ⊢ C = LCDual ⁡ K ⁡ W
6 hdmap12a.q ⊢ Q = 0 C
7 hdmap12a.s ⊢ S = HDMap ⁡ K ⁡ W
8 hdmap12a.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 hdmap12a.x ⊢ φ → T ∈ V
10 eqid ⊢ LSpan ⁡ U = LSpan ⁡ U
11 eqid ⊢ LSpan ⁡ C = LSpan ⁡ C
12 eqid ⊢ mapd ⁡ K ⁡ W = mapd ⁡ K ⁡ W
13 1 2 3 10 5 11 12 7 8 9 hdmap10 ⊢ φ → mapd ⁡ K ⁡ W ⁡ LSpan ⁡ U ⁡ T = LSpan ⁡ C ⁡ S ⁡ T
14 1 12 2 4 5 6 8 mapd0 ⊢ φ → mapd ⁡ K ⁡ W ⁡ 0 ˙ = Q
15 13 14 eqeq12d ⊢ φ → mapd ⁡ K ⁡ W ⁡ LSpan ⁡ U ⁡ T = mapd ⁡ K ⁡ W ⁡ 0 ˙ ↔ LSpan ⁡ C ⁡ S ⁡ T = Q
16 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
17 1 2 8 dvhlmod ⊢ φ → U ∈ LMod
18 3 16 10 lspsncl ⊢ U ∈ LMod ∧ T ∈ V → LSpan ⁡ U ⁡ T ∈ LSubSp ⁡ U
19 17 9 18 syl2anc ⊢ φ → LSpan ⁡ U ⁡ T ∈ LSubSp ⁡ U
20 4 16 lsssn0 ⊢ U ∈ LMod → 0 ˙ ∈ LSubSp ⁡ U
21 17 20 syl ⊢ φ → 0 ˙ ∈ LSubSp ⁡ U
22 1 2 16 12 8 19 21 mapd11 ⊢ φ → mapd ⁡ K ⁡ W ⁡ LSpan ⁡ U ⁡ T = mapd ⁡ K ⁡ W ⁡ 0 ˙ ↔ LSpan ⁡ U ⁡ T = 0 ˙
23 1 5 8 lcdlmod ⊢ φ → C ∈ LMod
24 eqid ⊢ Base C = Base C
25 1 2 3 5 24 7 8 9 hdmapcl ⊢ φ → S ⁡ T ∈ Base C
26 24 6 11 lspsneq0 ⊢ C ∈ LMod ∧ S ⁡ T ∈ Base C → LSpan ⁡ C ⁡ S ⁡ T = Q ↔ S ⁡ T = Q
27 23 25 26 syl2anc ⊢ φ → LSpan ⁡ C ⁡ S ⁡ T = Q ↔ S ⁡ T = Q
28 15 22 27 3bitr3rd ⊢ φ → S ⁡ T = Q ↔ LSpan ⁡ U ⁡ T = 0 ˙
29 3 4 10 lspsneq0 ⊢ U ∈ LMod ∧ T ∈ V → LSpan ⁡ U ⁡ T = 0 ˙ ↔ T = 0 ˙
30 17 9 29 syl2anc ⊢ φ → LSpan ⁡ U ⁡ T = 0 ˙ ↔ T = 0 ˙
31 28 30 bitrd ⊢ φ → S ⁡ T = Q ↔ T = 0 ˙