Metamath Proof Explorer

Theorem dochsatshp

Description: The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 27-Jul-2014) (Revised by Mario Carneiro, 1-Oct-2014)

Ref Expression
Hypotheses dochsatshp.h ⊢ H = LHyp ⁡ K
dochsatshp.u ⊢ U = DVecH ⁡ K ⁡ W
dochsatshp.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochsatshp.a ⊢ A = LSAtoms ⁡ U
dochsatshp.y ⊢ Y = LSHyp ⁡ U
dochsatshp.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochsatshp.q ⊢ φ → Q ∈ A
Assertion dochsatshp ⊢ φ → ⊥ ˙ ⁡ Q ∈ Y

Proof

Step Hyp Ref Expression
1 dochsatshp.h ⊢ H = LHyp ⁡ K
2 dochsatshp.u ⊢ U = DVecH ⁡ K ⁡ W
3 dochsatshp.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
4 dochsatshp.a ⊢ A = LSAtoms ⁡ U
5 dochsatshp.y ⊢ Y = LSHyp ⁡ U
6 dochsatshp.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 dochsatshp.q ⊢ φ → Q ∈ A
8 eqid ⊢ Base U = Base U
9 1 2 6 dvhlmod ⊢ φ → U ∈ LMod
10 8 4 9 7 lsatssv ⊢ φ → Q ⊆ Base U
11 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
12 1 2 8 11 3 dochlss ⊢ K ∈ HL ∧ W ∈ H ∧ Q ⊆ Base U → ⊥ ˙ ⁡ Q ∈ LSubSp ⁡ U
13 6 10 12 syl2anc ⊢ φ → ⊥ ˙ ⁡ Q ∈ LSubSp ⁡ U
14 eqid ⊢ 0 U = 0 U
15 14 4 9 7 lsatn0 ⊢ φ → Q ≠ 0 U
16 1 2 3 8 14 doch0 ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ ⁡ 0 U = Base U
17 6 16 syl ⊢ φ → ⊥ ˙ ⁡ 0 U = Base U
18 17 eqeq2d ⊢ φ → ⊥ ˙ ⁡ Q = ⊥ ˙ ⁡ 0 U ↔ ⊥ ˙ ⁡ Q = Base U
19 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
20 1 2 19 4 dih1dimat ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A → Q ∈ ran ⁡ DIsoH ⁡ K ⁡ W
21 6 7 20 syl2anc ⊢ φ → Q ∈ ran ⁡ DIsoH ⁡ K ⁡ W
22 1 19 2 14 dih0rn ⊢ K ∈ HL ∧ W ∈ H → 0 U ∈ ran ⁡ DIsoH ⁡ K ⁡ W
23 6 22 syl ⊢ φ → 0 U ∈ ran ⁡ DIsoH ⁡ K ⁡ W
24 1 19 3 6 21 23 doch11 ⊢ φ → ⊥ ˙ ⁡ Q = ⊥ ˙ ⁡ 0 U ↔ Q = 0 U
25 18 24 bitr3d ⊢ φ → ⊥ ˙ ⁡ Q = Base U ↔ Q = 0 U
26 25 necon3bid ⊢ φ → ⊥ ˙ ⁡ Q ≠ Base U ↔ Q ≠ 0 U
27 15 26 mpbird ⊢ φ → ⊥ ˙ ⁡ Q ≠ Base U
28 eqid ⊢ LSpan ⁡ U = LSpan ⁡ U
29 8 28 14 4 islsat ⊢ U ∈ LMod → Q ∈ A ↔ ∃ v ∈ Base U ∖ 0 U Q = LSpan ⁡ U ⁡ v
30 9 29 syl ⊢ φ → Q ∈ A ↔ ∃ v ∈ Base U ∖ 0 U Q = LSpan ⁡ U ⁡ v
31 7 30 mpbid ⊢ φ → ∃ v ∈ Base U ∖ 0 U Q = LSpan ⁡ U ⁡ v
32 eldifi ⊢ v ∈ Base U ∖ 0 U → v ∈ Base U
33 32 adantr ⊢ v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → v ∈ Base U
34 33 a1i ⊢ φ → v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → v ∈ Base U
35 11 28 lspid ⊢ U ∈ LMod ∧ ⊥ ˙ ⁡ Q ∈ LSubSp ⁡ U → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q = ⊥ ˙ ⁡ Q
36 9 13 35 syl2anc ⊢ φ → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q = ⊥ ˙ ⁡ Q
37 36 uneq1d ⊢ φ → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ LSpan ⁡ U ⁡ v = ⊥ ˙ ⁡ Q ∪ LSpan ⁡ U ⁡ v
38 37 fveq2d ⊢ φ → LSpan ⁡ U ⁡ LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ LSpan ⁡ U ⁡ v = LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ LSpan ⁡ U ⁡ v
39 38 adantr ⊢ φ ∧ v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → LSpan ⁡ U ⁡ LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ LSpan ⁡ U ⁡ v = LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ LSpan ⁡ U ⁡ v
40 9 adantr ⊢ φ ∧ v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → U ∈ LMod
41 8 11 lssss ⊢ ⊥ ˙ ⁡ Q ∈ LSubSp ⁡ U → ⊥ ˙ ⁡ Q ⊆ Base U
42 13 41 syl ⊢ φ → ⊥ ˙ ⁡ Q ⊆ Base U
43 42 adantr ⊢ φ ∧ v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → ⊥ ˙ ⁡ Q ⊆ Base U
44 32 snssd ⊢ v ∈ Base U ∖ 0 U → v ⊆ Base U
45 44 adantr ⊢ v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → v ⊆ Base U
46 45 adantl ⊢ φ ∧ v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → v ⊆ Base U
47 8 28 lspun ⊢ U ∈ LMod ∧ ⊥ ˙ ⁡ Q ⊆ Base U ∧ v ⊆ Base U → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ v = LSpan ⁡ U ⁡ LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ LSpan ⁡ U ⁡ v
48 40 43 46 47 syl3anc ⊢ φ ∧ v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ v = LSpan ⁡ U ⁡ LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ LSpan ⁡ U ⁡ v
49 uneq2 ⊢ Q = LSpan ⁡ U ⁡ v → ⊥ ˙ ⁡ Q ∪ Q = ⊥ ˙ ⁡ Q ∪ LSpan ⁡ U ⁡ v
50 49 fveq2d ⊢ Q = LSpan ⁡ U ⁡ v → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ Q = LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ LSpan ⁡ U ⁡ v
51 50 adantl ⊢ v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ Q = LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ LSpan ⁡ U ⁡ v
52 51 adantl ⊢ φ ∧ v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ Q = LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ LSpan ⁡ U ⁡ v
53 39 48 52 3eqtr4d ⊢ φ ∧ v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ v = LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ Q
54 eqid ⊢ joinH ⁡ K ⁡ W = joinH ⁡ K ⁡ W
55 eqid ⊢ LSSum ⁡ U = LSSum ⁡ U
56 1 19 2 8 3 dochcl ⊢ K ∈ HL ∧ W ∈ H ∧ Q ⊆ Base U → ⊥ ˙ ⁡ Q ∈ ran ⁡ DIsoH ⁡ K ⁡ W
57 6 10 56 syl2anc ⊢ φ → ⊥ ˙ ⁡ Q ∈ ran ⁡ DIsoH ⁡ K ⁡ W
58 1 19 54 2 55 4 6 57 7 dihjat2 ⊢ φ → ⊥ ˙ ⁡ Q joinH ⁡ K ⁡ W Q = ⊥ ˙ ⁡ Q LSSum ⁡ U Q
59 1 2 8 54 6 42 10 djhcom ⊢ φ → ⊥ ˙ ⁡ Q joinH ⁡ K ⁡ W Q = Q joinH ⁡ K ⁡ W ⊥ ˙ ⁡ Q
60 11 4 9 7 lsatlssel ⊢ φ → Q ∈ LSubSp ⁡ U
61 11 28 55 lsmsp ⊢ U ∈ LMod ∧ ⊥ ˙ ⁡ Q ∈ LSubSp ⁡ U ∧ Q ∈ LSubSp ⁡ U → ⊥ ˙ ⁡ Q LSSum ⁡ U Q = LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ Q
62 9 13 60 61 syl3anc ⊢ φ → ⊥ ˙ ⁡ Q LSSum ⁡ U Q = LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ Q
63 58 59 62 3eqtr3rd ⊢ φ → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ Q = Q joinH ⁡ K ⁡ W ⊥ ˙ ⁡ Q
64 1 2 8 3 54 djhexmid ⊢ K ∈ HL ∧ W ∈ H ∧ Q ⊆ Base U → Q joinH ⁡ K ⁡ W ⊥ ˙ ⁡ Q = Base U
65 6 10 64 syl2anc ⊢ φ → Q joinH ⁡ K ⁡ W ⊥ ˙ ⁡ Q = Base U
66 63 65 eqtrd ⊢ φ → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ Q = Base U
67 66 adantr ⊢ φ ∧ v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ Q = Base U
68 53 67 eqtrd ⊢ φ ∧ v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ v = Base U
69 68 ex ⊢ φ → v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ v = Base U
70 34 69 jcad ⊢ φ → v ∈ Base U ∖ 0 U ∧ Q = LSpan ⁡ U ⁡ v → v ∈ Base U ∧ LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ v = Base U
71 70 reximdv2 ⊢ φ → ∃ v ∈ Base U ∖ 0 U Q = LSpan ⁡ U ⁡ v → ∃ v ∈ Base U LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ v = Base U
72 31 71 mpd ⊢ φ → ∃ v ∈ Base U LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ v = Base U
73 1 2 6 dvhlvec ⊢ φ → U ∈ LVec
74 8 28 11 5 islshp ⊢ U ∈ LVec → ⊥ ˙ ⁡ Q ∈ Y ↔ ⊥ ˙ ⁡ Q ∈ LSubSp ⁡ U ∧ ⊥ ˙ ⁡ Q ≠ Base U ∧ ∃ v ∈ Base U LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ v = Base U
75 73 74 syl ⊢ φ → ⊥ ˙ ⁡ Q ∈ Y ↔ ⊥ ˙ ⁡ Q ∈ LSubSp ⁡ U ∧ ⊥ ˙ ⁡ Q ≠ Base U ∧ ∃ v ∈ Base U LSpan ⁡ U ⁡ ⊥ ˙ ⁡ Q ∪ v = Base U
76 13 27 72 75 mpbir3and ⊢ φ → ⊥ ˙ ⁡ Q ∈ Y