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 = Base U
dihatexv2.o ⊢ 0 ˙ = 0 U
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 = Base U
5 dihatexv2.o ⊢ 0 ˙ = 0 U
6 dihatexv2.n ⊢ N = LSpan ⁡ U
7 dihatexv2.i ⊢ I = DIsoH ⁡ K ⁡ W
8 dihatexv2.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 eqid ⊢ Base K = Base K
10 9 1 atbase ⊢ Q ∈ A → Q ∈ Base K
11 10 anim2i ⊢ φ ∧ Q ∈ A → φ ∧ Q ∈ Base K
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 ∈ Base K
17 12 15 16 syl2anc ⊢ φ ∧ x ∈ V ∖ 0 ˙ → I -1 ⁡ N ⁡ x ∈ Base K
18 eleq1a ⊢ I -1 ⁡ N ⁡ x ∈ Base K → Q = I -1 ⁡ N ⁡ x → Q ∈ Base K
19 17 18 syl ⊢ φ ∧ x ∈ V ∖ 0 ˙ → Q = I -1 ⁡ N ⁡ x → Q ∈ Base K
20 19 rexlimdva ⊢ φ → ∃ x ∈ V ∖ 0 ˙ Q = I -1 ⁡ N ⁡ x → Q ∈ Base K
21 20 imdistani ⊢ φ ∧ ∃ x ∈ V ∖ 0 ˙ Q = I -1 ⁡ N ⁡ x → φ ∧ Q ∈ Base K
22 8 adantr ⊢ φ ∧ Q ∈ Base K → K ∈ HL ∧ W ∈ H
23 simpr ⊢ φ ∧ Q ∈ Base K → Q ∈ Base K
24 9 1 2 3 4 5 6 7 22 23 dihatexv ⊢ φ ∧ Q ∈ Base K → Q ∈ A ↔ ∃ x ∈ V ∖ 0 ˙ I ⁡ Q = N ⁡ x
25 22 adantr ⊢ φ ∧ Q ∈ Base K ∧ x ∈ V ∖ 0 ˙ → K ∈ HL ∧ W ∈ H
26 22 13 14 syl2an ⊢ φ ∧ Q ∈ Base K ∧ 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 ∈ Base K ∧ x ∈ V ∖ 0 ˙ → I ⁡ I -1 ⁡ N ⁡ x = N ⁡ x
29 28 eqeq2d ⊢ φ ∧ Q ∈ Base K ∧ x ∈ V ∖ 0 ˙ → I ⁡ Q = I ⁡ I -1 ⁡ N ⁡ x ↔ I ⁡ Q = N ⁡ x
30 simplr ⊢ φ ∧ Q ∈ Base K ∧ x ∈ V ∖ 0 ˙ → Q ∈ Base K
31 25 26 16 syl2anc ⊢ φ ∧ Q ∈ Base K ∧ x ∈ V ∖ 0 ˙ → I -1 ⁡ N ⁡ x ∈ Base K
32 9 2 7 dih11 ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ Base K ∧ I -1 ⁡ N ⁡ x ∈ Base K → I ⁡ Q = I ⁡ I -1 ⁡ N ⁡ x ↔ Q = I -1 ⁡ N ⁡ x
33 25 30 31 32 syl3anc ⊢ φ ∧ Q ∈ Base K ∧ x ∈ V ∖ 0 ˙ → I ⁡ Q = I ⁡ I -1 ⁡ N ⁡ x ↔ Q = I -1 ⁡ N ⁡ x
34 29 33 bitr3d ⊢ φ ∧ Q ∈ Base K ∧ x ∈ V ∖ 0 ˙ → I ⁡ Q = N ⁡ x ↔ Q = I -1 ⁡ N ⁡ x
35 34 rexbidva ⊢ φ ∧ Q ∈ Base K → ∃ x ∈ V ∖ 0 ˙ I ⁡ Q = N ⁡ x ↔ ∃ x ∈ V ∖ 0 ˙ Q = I -1 ⁡ N ⁡ x
36 24 35 bitrd ⊢ φ ∧ Q ∈ Base K → 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