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 ⊢BaseU=BaseU
9 eqid ⊢LSpan⁡U=LSpan⁡U
10 eqid ⊢0U=0U
11 8 9 10 5 islsat ⊢U∈LVec→Q∈L↔∃v∈BaseU∖0UQ=LSpan⁡U⁡v
12 7 11 syl ⊢K∈HL∧W∈H→Q∈L↔∃v∈BaseU∖0UQ=LSpan⁡U⁡v
13 12 biimpa ⊢K∈HL∧W∈H∧Q∈L→∃v∈BaseU∖0UQ=LSpan⁡U⁡v
14 eldifsn ⊢v∈BaseU∖0U↔v∈BaseU∧v≠0U
15 1 2 3 8 10 9 4 dihlspsnat ⊢K∈HL∧W∈H∧v∈BaseU∧v≠0U→I-1⁡LSpan⁡U⁡v∈A
16 15 3expb ⊢K∈HL∧W∈H∧v∈BaseU∧v≠0U→I-1⁡LSpan⁡U⁡v∈A
17 14 16 sylan2b ⊢K∈HL∧W∈H∧v∈BaseU∖0U→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∈BaseU∖0U→Q=LSpan⁡U⁡v→I-1⁡Q∈A
21 20 rexlimdva ⊢K∈HL∧W∈H→∃v∈BaseU∖0UQ=LSpan⁡U⁡v→I-1⁡Q∈A
22 21 adantr ⊢K∈HL∧W∈H∧Q∈L→∃v∈BaseU∖0UQ=LSpan⁡U⁡v→I-1⁡Q∈A
23 13 22 mpd ⊢K∈HL∧W∈H∧Q∈L→I-1⁡Q∈A