Metamath Proof Explorer

Theorem dihlatat

Description: The reverse isomorphism H of a 1-dim subspace is an atom. (Contributed by NM, 28-Apr-2014)

Ref Expression
Hypotheses dihlatat.a ⊢ A = Atoms ⁡ K
dihlatat.h ⊢ H = LHyp ⁡ K
dihlatat.u ⊢ U = DVecH ⁡ K ⁡ W
dihlatat.i ⊢ I = DIsoH ⁡ K ⁡ W
dihlatat.l ⊢ L = LSAtoms ⁡ U
Assertion dihlatat ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ L → I -1 ⁡ Q ∈ A

Proof

Step Hyp Ref Expression
1 dihlatat.a ⊢ A = Atoms ⁡ K
2 dihlatat.h ⊢ H = LHyp ⁡ K
3 dihlatat.u ⊢ U = DVecH ⁡ K ⁡ W
4 dihlatat.i ⊢ I = DIsoH ⁡ K ⁡ W
5 dihlatat.l ⊢ L = LSAtoms ⁡ U
6 id ⊢ K ∈ HL ∧ W ∈ H → K ∈ HL ∧ W ∈ H
7 2 3 6 dvhlvec ⊢ K ∈ HL ∧ W ∈ H → U ∈ LVec
8 eqid ⊢ Base U = Base U
9 eqid ⊢ LSpan ⁡ U = LSpan ⁡ U
10 eqid ⊢ 0 U = 0 U
11 8 9 10 5 islsat ⊢ U ∈ LVec → Q ∈ L ↔ ∃ v ∈ Base U ∖ 0 U Q = LSpan ⁡ U ⁡ v
12 7 11 syl ⊢ K ∈ HL ∧ W ∈ H → Q ∈ L ↔ ∃ v ∈ Base U ∖ 0 U Q = LSpan ⁡ U ⁡ v
13 12 biimpa ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ L → ∃ v ∈ Base U ∖ 0 U Q = LSpan ⁡ U ⁡ v
14 eldifsn ⊢ v ∈ Base U ∖ 0 U ↔ v ∈ Base U ∧ v ≠ 0 U
15 1 2 3 8 10 9 4 dihlspsnat ⊢ K ∈ HL ∧ W ∈ H ∧ v ∈ Base U ∧ v ≠ 0 U → I -1 ⁡ LSpan ⁡ U ⁡ v ∈ A
16 15 3expb ⊢ K ∈ HL ∧ W ∈ H ∧ v ∈ Base U ∧ v ≠ 0 U → I -1 ⁡ LSpan ⁡ U ⁡ v ∈ A
17 14 16 sylan2b ⊢ K ∈ HL ∧ W ∈ H ∧ v ∈ Base U ∖ 0 U → I -1 ⁡ LSpan ⁡ U ⁡ v ∈ A
18 fveq2 ⊢ Q = LSpan ⁡ U ⁡ v → I -1 ⁡ Q = I -1 ⁡ LSpan ⁡ U ⁡ v
19 18 eleq1d ⊢ Q = LSpan ⁡ U ⁡ v → I -1 ⁡ Q ∈ A ↔ I -1 ⁡ LSpan ⁡ U ⁡ v ∈ A
20 17 19 syl5ibrcom ⊢ K ∈ HL ∧ W ∈ H ∧ v ∈ Base U ∖ 0 U → Q = LSpan ⁡ U ⁡ v → I -1 ⁡ Q ∈ A
21 20 rexlimdva ⊢ K ∈ HL ∧ W ∈ H → ∃ v ∈ Base U ∖ 0 U Q = LSpan ⁡ U ⁡ v → I -1 ⁡ Q ∈ A
22 21 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ L → ∃ v ∈ Base U ∖ 0 U Q = LSpan ⁡ U ⁡ v → I -1 ⁡ Q ∈ A
23 13 22 mpd ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ L → I -1 ⁡ Q ∈ A