Metamath Proof Explorer

Theorem dihatexv2

Description: There is a nonzero vector that maps to every lattice atom. (Contributed by NM, 17-Aug-2014)

Ref Expression
Hypotheses dihatexv2.a ⊢A=Atoms⁡K
dihatexv2.h ⊢H=LHyp⁡K
dihatexv2.u ⊢U=DVecH⁡K⁡W
dihatexv2.v ⊢V=BaseU
dihatexv2.o ⊢0˙=0U
dihatexv2.n ⊢N=LSpan⁡U
dihatexv2.i ⊢I=DIsoH⁡K⁡W
dihatexv2.k ⊢φ→K∈HL∧W∈H
Assertion dihatexv2 ⊢φ→Q∈A↔∃x∈V∖0˙Q=I-1⁡N⁡x

Proof

Step Hyp Ref Expression
1 dihatexv2.a ⊢A=Atoms⁡K
2 dihatexv2.h ⊢H=LHyp⁡K
3 dihatexv2.u ⊢U=DVecH⁡K⁡W
4 dihatexv2.v ⊢V=BaseU
5 dihatexv2.o ⊢0˙=0U
6 dihatexv2.n ⊢N=LSpan⁡U
7 dihatexv2.i ⊢I=DIsoH⁡K⁡W
8 dihatexv2.k ⊢φ→K∈HL∧W∈H
9 eqid ⊢BaseK=BaseK
10 9 1 atbase ⊢Q∈A→Q∈BaseK
11 10 anim2i ⊢φ∧Q∈A→φ∧Q∈BaseK
12 8 adantr ⊢φ∧x∈V∖0˙→K∈HL∧W∈H
13 eldifi ⊢x∈V∖0˙→x∈V
14 2 3 4 6 7 dihlsprn ⊢K∈HL∧W∈H∧x∈V→N⁡x∈ran⁡I
15 8 13 14 syl2an ⊢φ∧x∈V∖0˙→N⁡x∈ran⁡I
16 9 2 7 dihcnvcl ⊢K∈HL∧W∈H∧N⁡x∈ran⁡I→I-1⁡N⁡x∈BaseK
17 12 15 16 syl2anc ⊢φ∧x∈V∖0˙→I-1⁡N⁡x∈BaseK
18 eleq1a ⊢I-1⁡N⁡x∈BaseK→Q=I-1⁡N⁡x→Q∈BaseK
19 17 18 syl ⊢φ∧x∈V∖0˙→Q=I-1⁡N⁡x→Q∈BaseK
20 19 rexlimdva ⊢φ→∃x∈V∖0˙Q=I-1⁡N⁡x→Q∈BaseK
21 20 imdistani ⊢φ∧∃x∈V∖0˙Q=I-1⁡N⁡x→φ∧Q∈BaseK
22 8 adantr ⊢φ∧Q∈BaseK→K∈HL∧W∈H
23 simpr ⊢φ∧Q∈BaseK→Q∈BaseK
24 9 1 2 3 4 5 6 7 22 23 dihatexv ⊢φ∧Q∈BaseK→Q∈A↔∃x∈V∖0˙I⁡Q=N⁡x
25 22 adantr ⊢φ∧Q∈BaseK∧x∈V∖0˙→K∈HL∧W∈H
26 22 13 14 syl2an ⊢φ∧Q∈BaseK∧x∈V∖0˙→N⁡x∈ran⁡I
27 2 7 dihcnvid2 ⊢K∈HL∧W∈H∧N⁡x∈ran⁡I→I⁡I-1⁡N⁡x=N⁡x
28 25 26 27 syl2anc ⊢φ∧Q∈BaseK∧x∈V∖0˙→I⁡I-1⁡N⁡x=N⁡x
29 28 eqeq2d ⊢φ∧Q∈BaseK∧x∈V∖0˙→I⁡Q=I⁡I-1⁡N⁡x↔I⁡Q=N⁡x
30 simplr ⊢φ∧Q∈BaseK∧x∈V∖0˙→Q∈BaseK
31 25 26 16 syl2anc ⊢φ∧Q∈BaseK∧x∈V∖0˙→I-1⁡N⁡x∈BaseK
32 9 2 7 dih11 ⊢K∈HL∧W∈H∧Q∈BaseK∧I-1⁡N⁡x∈BaseK→I⁡Q=I⁡I-1⁡N⁡x↔Q=I-1⁡N⁡x
33 25 30 31 32 syl3anc ⊢φ∧Q∈BaseK∧x∈V∖0˙→I⁡Q=I⁡I-1⁡N⁡x↔Q=I-1⁡N⁡x
34 29 33 bitr3d ⊢φ∧Q∈BaseK∧x∈V∖0˙→I⁡Q=N⁡x↔Q=I-1⁡N⁡x
35 34 rexbidva ⊢φ∧Q∈BaseK→∃x∈V∖0˙I⁡Q=N⁡x↔∃x∈V∖0˙Q=I-1⁡N⁡x
36 24 35 bitrd ⊢φ∧Q∈BaseK→Q∈A↔∃x∈V∖0˙Q=I-1⁡N⁡x
37 11 21 36 pm5.21nd ⊢φ→Q∈A↔∃x∈V∖0˙Q=I-1⁡N⁡x