Metamath Proof Explorer

Theorem hdmapglem7a

Description: Lemma for hdmapg . (Contributed by NM, 14-Jun-2015)

Ref Expression
Hypotheses hdmapglem7.h ⊢ H = LHyp ⁡ K
hdmapglem7.e ⊢ E = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W
hdmapglem7.o ⊢ O = ocH ⁡ K ⁡ W
hdmapglem7.u ⊢ U = DVecH ⁡ K ⁡ W
hdmapglem7.v ⊢ V = Base U
hdmapglem7.p ⊢ + ˙ = + U
hdmapglem7.q ⊢ · ˙ = ⋅ U
hdmapglem7.r ⊢ R = Scalar ⁡ U
hdmapglem7.b ⊢ B = Base R
hdmapglem7.a ⊢ ⊕ ˙ = LSSum ⁡ U
hdmapglem7.n ⊢ N = LSpan ⁡ U
hdmapglem7.k ⊢ φ → K ∈ HL ∧ W ∈ H
hdmapglem7.x ⊢ φ → X ∈ V
Assertion hdmapglem7a ⊢ φ → ∃ u ∈ O ⁡ E ∃ k ∈ B X = k · ˙ E + ˙ u

Proof

Step Hyp Ref Expression
1 hdmapglem7.h ⊢ H = LHyp ⁡ K
2 hdmapglem7.e ⊢ E = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W
3 hdmapglem7.o ⊢ O = ocH ⁡ K ⁡ W
4 hdmapglem7.u ⊢ U = DVecH ⁡ K ⁡ W
5 hdmapglem7.v ⊢ V = Base U
6 hdmapglem7.p ⊢ + ˙ = + U
7 hdmapglem7.q ⊢ · ˙ = ⋅ U
8 hdmapglem7.r ⊢ R = Scalar ⁡ U
9 hdmapglem7.b ⊢ B = Base R
10 hdmapglem7.a ⊢ ⊕ ˙ = LSSum ⁡ U
11 hdmapglem7.n ⊢ N = LSpan ⁡ U
12 hdmapglem7.k ⊢ φ → K ∈ HL ∧ W ∈ H
13 hdmapglem7.x ⊢ φ → X ∈ V
14 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
15 1 4 12 dvhlmod ⊢ φ → U ∈ LMod
16 eqid ⊢ Base K = Base K
17 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
18 eqid ⊢ 0 U = 0 U
19 1 16 17 4 5 18 2 12 dvheveccl ⊢ φ → E ∈ V ∖ 0 U
20 19 eldifad ⊢ φ → E ∈ V
21 5 14 11 lspsncl ⊢ U ∈ LMod ∧ E ∈ V → N ⁡ E ∈ LSubSp ⁡ U
22 15 20 21 syl2anc ⊢ φ → N ⁡ E ∈ LSubSp ⁡ U
23 20 snssd ⊢ φ → E ⊆ V
24 1 4 3 5 11 12 23 dochocsp ⊢ φ → O ⁡ N ⁡ E = O ⁡ E
25 24 fveq2d ⊢ φ → O ⁡ O ⁡ N ⁡ E = O ⁡ O ⁡ E
26 1 4 3 5 11 12 20 dochocsn ⊢ φ → O ⁡ O ⁡ E = N ⁡ E
27 25 26 eqtrd ⊢ φ → O ⁡ O ⁡ N ⁡ E = N ⁡ E
28 1 3 4 5 14 10 12 22 27 dochexmid ⊢ φ → N ⁡ E ⊕ ˙ O ⁡ N ⁡ E = V
29 24 oveq2d ⊢ φ → N ⁡ E ⊕ ˙ O ⁡ N ⁡ E = N ⁡ E ⊕ ˙ O ⁡ E
30 28 29 eqtr3d ⊢ φ → V = N ⁡ E ⊕ ˙ O ⁡ E
31 13 30 eleqtrd ⊢ φ → X ∈ N ⁡ E ⊕ ˙ O ⁡ E
32 14 lsssssubg ⊢ U ∈ LMod → LSubSp ⁡ U ⊆ SubGrp ⁡ U
33 15 32 syl ⊢ φ → LSubSp ⁡ U ⊆ SubGrp ⁡ U
34 33 22 sseldd ⊢ φ → N ⁡ E ∈ SubGrp ⁡ U
35 1 4 5 14 3 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ E ⊆ V → O ⁡ E ∈ LSubSp ⁡ U
36 12 23 35 syl2anc ⊢ φ → O ⁡ E ∈ LSubSp ⁡ U
37 33 36 sseldd ⊢ φ → O ⁡ E ∈ SubGrp ⁡ U
38 6 10 lsmelval ⊢ N ⁡ E ∈ SubGrp ⁡ U ∧ O ⁡ E ∈ SubGrp ⁡ U → X ∈ N ⁡ E ⊕ ˙ O ⁡ E ↔ ∃ a ∈ N ⁡ E ∃ u ∈ O ⁡ E X = a + ˙ u
39 34 37 38 syl2anc ⊢ φ → X ∈ N ⁡ E ⊕ ˙ O ⁡ E ↔ ∃ a ∈ N ⁡ E ∃ u ∈ O ⁡ E X = a + ˙ u
40 31 39 mpbid ⊢ φ → ∃ a ∈ N ⁡ E ∃ u ∈ O ⁡ E X = a + ˙ u
41 rexcom ⊢ ∃ a ∈ N ⁡ E ∃ u ∈ O ⁡ E X = a + ˙ u ↔ ∃ u ∈ O ⁡ E ∃ a ∈ N ⁡ E X = a + ˙ u
42 df-rex ⊢ ∃ a ∈ N ⁡ E X = a + ˙ u ↔ ∃ a a ∈ N ⁡ E ∧ X = a + ˙ u
43 8 9 5 7 11 lspsnel ⊢ U ∈ LMod ∧ E ∈ V → a ∈ N ⁡ E ↔ ∃ k ∈ B a = k · ˙ E
44 15 20 43 syl2anc ⊢ φ → a ∈ N ⁡ E ↔ ∃ k ∈ B a = k · ˙ E
45 44 anbi1d ⊢ φ → a ∈ N ⁡ E ∧ X = a + ˙ u ↔ ∃ k ∈ B a = k · ˙ E ∧ X = a + ˙ u
46 r19.41v ⊢ ∃ k ∈ B a = k · ˙ E ∧ X = a + ˙ u ↔ ∃ k ∈ B a = k · ˙ E ∧ X = a + ˙ u
47 45 46 bitr4di ⊢ φ → a ∈ N ⁡ E ∧ X = a + ˙ u ↔ ∃ k ∈ B a = k · ˙ E ∧ X = a + ˙ u
48 47 exbidv ⊢ φ → ∃ a a ∈ N ⁡ E ∧ X = a + ˙ u ↔ ∃ a ∃ k ∈ B a = k · ˙ E ∧ X = a + ˙ u
49 rexcom4 ⊢ ∃ k ∈ B ∃ a a = k · ˙ E ∧ X = a + ˙ u ↔ ∃ a ∃ k ∈ B a = k · ˙ E ∧ X = a + ˙ u
50 ovex ⊢ k · ˙ E ∈ V
51 oveq1 ⊢ a = k · ˙ E → a + ˙ u = k · ˙ E + ˙ u
52 51 eqeq2d ⊢ a = k · ˙ E → X = a + ˙ u ↔ X = k · ˙ E + ˙ u
53 50 52 ceqsexv ⊢ ∃ a a = k · ˙ E ∧ X = a + ˙ u ↔ X = k · ˙ E + ˙ u
54 53 rexbii ⊢ ∃ k ∈ B ∃ a a = k · ˙ E ∧ X = a + ˙ u ↔ ∃ k ∈ B X = k · ˙ E + ˙ u
55 49 54 bitr3i ⊢ ∃ a ∃ k ∈ B a = k · ˙ E ∧ X = a + ˙ u ↔ ∃ k ∈ B X = k · ˙ E + ˙ u
56 48 55 bitrdi ⊢ φ → ∃ a a ∈ N ⁡ E ∧ X = a + ˙ u ↔ ∃ k ∈ B X = k · ˙ E + ˙ u
57 42 56 syl5bb ⊢ φ → ∃ a ∈ N ⁡ E X = a + ˙ u ↔ ∃ k ∈ B X = k · ˙ E + ˙ u
58 57 rexbidv ⊢ φ → ∃ u ∈ O ⁡ E ∃ a ∈ N ⁡ E X = a + ˙ u ↔ ∃ u ∈ O ⁡ E ∃ k ∈ B X = k · ˙ E + ˙ u
59 41 58 syl5bb ⊢ φ → ∃ a ∈ N ⁡ E ∃ u ∈ O ⁡ E X = a + ˙ u ↔ ∃ u ∈ O ⁡ E ∃ k ∈ B X = k · ˙ E + ˙ u
60 40 59 mpbid ⊢ φ → ∃ u ∈ O ⁡ E ∃ k ∈ B X = k · ˙ E + ˙ u