Metamath Proof Explorer

Theorem djhcvat42

Description: A covering property. ( cvrat42 analog.) (Contributed by NM, 17-Aug-2014)

Ref Expression
Hypotheses djhcvat42.h ⊢ H = LHyp ⁡ K
djhcvat42.u ⊢ U = DVecH ⁡ K ⁡ W
djhcvat42.v ⊢ V = Base U
djhcvat42.o ⊢ 0 ˙ = 0 U
djhcvat42.n ⊢ N = LSpan ⁡ U
djhcvat42.i ⊢ I = DIsoH ⁡ K ⁡ W
djhcvat42.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
djhcvat42.k ⊢ φ → K ∈ HL ∧ W ∈ H
djhcvat42.s ⊢ φ → S ∈ ran ⁡ I
djhcvat42.x ⊢ φ → X ∈ V ∖ 0 ˙
djhcvat42.y ⊢ φ → Y ∈ V ∖ 0 ˙
Assertion djhcvat42 ⊢ φ → S ≠ 0 ˙ ∧ N ⁡ X ⊆ S ∨ ˙ N ⁡ Y → ∃ z ∈ V ∖ 0 ˙ N ⁡ z ⊆ S ∧ N ⁡ X ⊆ N ⁡ z ∨ ˙ N ⁡ Y

Proof

Step Hyp Ref Expression
1 djhcvat42.h ⊢ H = LHyp ⁡ K
2 djhcvat42.u ⊢ U = DVecH ⁡ K ⁡ W
3 djhcvat42.v ⊢ V = Base U
4 djhcvat42.o ⊢ 0 ˙ = 0 U
5 djhcvat42.n ⊢ N = LSpan ⁡ U
6 djhcvat42.i ⊢ I = DIsoH ⁡ K ⁡ W
7 djhcvat42.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
8 djhcvat42.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 djhcvat42.s ⊢ φ → S ∈ ran ⁡ I
10 djhcvat42.x ⊢ φ → X ∈ V ∖ 0 ˙
11 djhcvat42.y ⊢ φ → Y ∈ V ∖ 0 ˙
12 8 simpld ⊢ φ → K ∈ HL
13 eqid ⊢ Base K = Base K
14 13 1 6 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ ran ⁡ I → I -1 ⁡ S ∈ Base K
15 8 9 14 syl2anc ⊢ φ → I -1 ⁡ S ∈ Base K
16 10 eldifad ⊢ φ → X ∈ V
17 eldifsni ⊢ X ∈ V ∖ 0 ˙ → X ≠ 0 ˙
18 10 17 syl ⊢ φ → X ≠ 0 ˙
19 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
20 19 1 2 3 4 5 6 dihlspsnat ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ V ∧ X ≠ 0 ˙ → I -1 ⁡ N ⁡ X ∈ Atoms ⁡ K
21 8 16 18 20 syl3anc ⊢ φ → I -1 ⁡ N ⁡ X ∈ Atoms ⁡ K
22 11 eldifad ⊢ φ → Y ∈ V
23 eldifsni ⊢ Y ∈ V ∖ 0 ˙ → Y ≠ 0 ˙
24 11 23 syl ⊢ φ → Y ≠ 0 ˙
25 19 1 2 3 4 5 6 dihlspsnat ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ V ∧ Y ≠ 0 ˙ → I -1 ⁡ N ⁡ Y ∈ Atoms ⁡ K
26 8 22 24 25 syl3anc ⊢ φ → I -1 ⁡ N ⁡ Y ∈ Atoms ⁡ K
27 eqid ⊢ ≤ K = ≤ K
28 eqid ⊢ join ⁡ K = join ⁡ K
29 eqid ⊢ 0. ⁡ K = 0. ⁡ K
30 13 27 28 29 19 cvrat42 ⊢ K ∈ HL ∧ I -1 ⁡ S ∈ Base K ∧ I -1 ⁡ N ⁡ X ∈ Atoms ⁡ K ∧ I -1 ⁡ N ⁡ Y ∈ Atoms ⁡ K → I -1 ⁡ S ≠ 0. ⁡ K ∧ I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ S join ⁡ K I -1 ⁡ N ⁡ Y → ∃ r ∈ Atoms ⁡ K r ≤ K I -1 ⁡ S ∧ I -1 ⁡ N ⁡ X ≤ K r join ⁡ K I -1 ⁡ N ⁡ Y
31 12 15 21 26 30 syl13anc ⊢ φ → I -1 ⁡ S ≠ 0. ⁡ K ∧ I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ S join ⁡ K I -1 ⁡ N ⁡ Y → ∃ r ∈ Atoms ⁡ K r ≤ K I -1 ⁡ S ∧ I -1 ⁡ N ⁡ X ≤ K r join ⁡ K I -1 ⁡ N ⁡ Y
32 1 29 6 2 3 4 5 8 9 dih0sb ⊢ φ → S = 0 ˙ ↔ I -1 ⁡ S = 0. ⁡ K
33 32 necon3bid ⊢ φ → S ≠ 0 ˙ ↔ I -1 ⁡ S ≠ 0. ⁡ K
34 1 2 3 5 6 dihlsprn ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ V → N ⁡ X ∈ ran ⁡ I
35 8 16 34 syl2anc ⊢ φ → N ⁡ X ∈ ran ⁡ I
36 1 2 6 3 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ ran ⁡ I → S ⊆ V
37 8 9 36 syl2anc ⊢ φ → S ⊆ V
38 1 2 3 5 6 dihlsprn ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ V → N ⁡ Y ∈ ran ⁡ I
39 8 22 38 syl2anc ⊢ φ → N ⁡ Y ∈ ran ⁡ I
40 1 2 6 3 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ N ⁡ Y ∈ ran ⁡ I → N ⁡ Y ⊆ V
41 8 39 40 syl2anc ⊢ φ → N ⁡ Y ⊆ V
42 1 6 2 3 7 djhcl ⊢ K ∈ HL ∧ W ∈ H ∧ S ⊆ V ∧ N ⁡ Y ⊆ V → S ∨ ˙ N ⁡ Y ∈ ran ⁡ I
43 8 37 41 42 syl12anc ⊢ φ → S ∨ ˙ N ⁡ Y ∈ ran ⁡ I
44 27 1 6 8 35 43 dihcnvord ⊢ φ → I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ S ∨ ˙ N ⁡ Y ↔ N ⁡ X ⊆ S ∨ ˙ N ⁡ Y
45 28 1 6 7 8 9 39 djhj ⊢ φ → I -1 ⁡ S ∨ ˙ N ⁡ Y = I -1 ⁡ S join ⁡ K I -1 ⁡ N ⁡ Y
46 45 breq2d ⊢ φ → I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ S ∨ ˙ N ⁡ Y ↔ I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ S join ⁡ K I -1 ⁡ N ⁡ Y
47 44 46 bitr3d ⊢ φ → N ⁡ X ⊆ S ∨ ˙ N ⁡ Y ↔ I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ S join ⁡ K I -1 ⁡ N ⁡ Y
48 33 47 anbi12d ⊢ φ → S ≠ 0 ˙ ∧ N ⁡ X ⊆ S ∨ ˙ N ⁡ Y ↔ I -1 ⁡ S ≠ 0. ⁡ K ∧ I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ S join ⁡ K I -1 ⁡ N ⁡ Y
49 8 adantr ⊢ φ ∧ z ∈ V ∖ 0 ˙ → K ∈ HL ∧ W ∈ H
50 eldifi ⊢ z ∈ V ∖ 0 ˙ → z ∈ V
51 50 adantl ⊢ φ ∧ z ∈ V ∖ 0 ˙ → z ∈ V
52 eldifsni ⊢ z ∈ V ∖ 0 ˙ → z ≠ 0 ˙
53 52 adantl ⊢ φ ∧ z ∈ V ∖ 0 ˙ → z ≠ 0 ˙
54 19 1 2 3 4 5 6 dihlspsnat ⊢ K ∈ HL ∧ W ∈ H ∧ z ∈ V ∧ z ≠ 0 ˙ → I -1 ⁡ N ⁡ z ∈ Atoms ⁡ K
55 49 51 53 54 syl3anc ⊢ φ ∧ z ∈ V ∖ 0 ˙ → I -1 ⁡ N ⁡ z ∈ Atoms ⁡ K
56 19 1 2 3 4 5 6 8 dihatexv2 ⊢ φ → r ∈ Atoms ⁡ K ↔ ∃ z ∈ V ∖ 0 ˙ r = I -1 ⁡ N ⁡ z
57 breq1 ⊢ r = I -1 ⁡ N ⁡ z → r ≤ K I -1 ⁡ S ↔ I -1 ⁡ N ⁡ z ≤ K I -1 ⁡ S
58 oveq1 ⊢ r = I -1 ⁡ N ⁡ z → r join ⁡ K I -1 ⁡ N ⁡ Y = I -1 ⁡ N ⁡ z join ⁡ K I -1 ⁡ N ⁡ Y
59 58 breq2d ⊢ r = I -1 ⁡ N ⁡ z → I -1 ⁡ N ⁡ X ≤ K r join ⁡ K I -1 ⁡ N ⁡ Y ↔ I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ N ⁡ z join ⁡ K I -1 ⁡ N ⁡ Y
60 57 59 anbi12d ⊢ r = I -1 ⁡ N ⁡ z → r ≤ K I -1 ⁡ S ∧ I -1 ⁡ N ⁡ X ≤ K r join ⁡ K I -1 ⁡ N ⁡ Y ↔ I -1 ⁡ N ⁡ z ≤ K I -1 ⁡ S ∧ I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ N ⁡ z join ⁡ K I -1 ⁡ N ⁡ Y
61 60 adantl ⊢ φ ∧ r = I -1 ⁡ N ⁡ z → r ≤ K I -1 ⁡ S ∧ I -1 ⁡ N ⁡ X ≤ K r join ⁡ K I -1 ⁡ N ⁡ Y ↔ I -1 ⁡ N ⁡ z ≤ K I -1 ⁡ S ∧ I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ N ⁡ z join ⁡ K I -1 ⁡ N ⁡ Y
62 55 56 61 rexxfr2d ⊢ φ → ∃ r ∈ Atoms ⁡ K r ≤ K I -1 ⁡ S ∧ I -1 ⁡ N ⁡ X ≤ K r join ⁡ K I -1 ⁡ N ⁡ Y ↔ ∃ z ∈ V ∖ 0 ˙ I -1 ⁡ N ⁡ z ≤ K I -1 ⁡ S ∧ I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ N ⁡ z join ⁡ K I -1 ⁡ N ⁡ Y
63 1 2 3 5 6 dihlsprn ⊢ K ∈ HL ∧ W ∈ H ∧ z ∈ V → N ⁡ z ∈ ran ⁡ I
64 49 51 63 syl2anc ⊢ φ ∧ z ∈ V ∖ 0 ˙ → N ⁡ z ∈ ran ⁡ I
65 9 adantr ⊢ φ ∧ z ∈ V ∖ 0 ˙ → S ∈ ran ⁡ I
66 27 1 6 49 64 65 dihcnvord ⊢ φ ∧ z ∈ V ∖ 0 ˙ → I -1 ⁡ N ⁡ z ≤ K I -1 ⁡ S ↔ N ⁡ z ⊆ S
67 39 adantr ⊢ φ ∧ z ∈ V ∖ 0 ˙ → N ⁡ Y ∈ ran ⁡ I
68 28 1 6 7 49 64 67 djhj ⊢ φ ∧ z ∈ V ∖ 0 ˙ → I -1 ⁡ N ⁡ z ∨ ˙ N ⁡ Y = I -1 ⁡ N ⁡ z join ⁡ K I -1 ⁡ N ⁡ Y
69 68 breq2d ⊢ φ ∧ z ∈ V ∖ 0 ˙ → I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ N ⁡ z ∨ ˙ N ⁡ Y ↔ I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ N ⁡ z join ⁡ K I -1 ⁡ N ⁡ Y
70 16 adantr ⊢ φ ∧ z ∈ V ∖ 0 ˙ → X ∈ V
71 49 70 34 syl2anc ⊢ φ ∧ z ∈ V ∖ 0 ˙ → N ⁡ X ∈ ran ⁡ I
72 1 2 6 3 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ N ⁡ z ∈ ran ⁡ I → N ⁡ z ⊆ V
73 49 64 72 syl2anc ⊢ φ ∧ z ∈ V ∖ 0 ˙ → N ⁡ z ⊆ V
74 41 adantr ⊢ φ ∧ z ∈ V ∖ 0 ˙ → N ⁡ Y ⊆ V
75 1 6 2 3 7 djhcl ⊢ K ∈ HL ∧ W ∈ H ∧ N ⁡ z ⊆ V ∧ N ⁡ Y ⊆ V → N ⁡ z ∨ ˙ N ⁡ Y ∈ ran ⁡ I
76 49 73 74 75 syl12anc ⊢ φ ∧ z ∈ V ∖ 0 ˙ → N ⁡ z ∨ ˙ N ⁡ Y ∈ ran ⁡ I
77 27 1 6 49 71 76 dihcnvord ⊢ φ ∧ z ∈ V ∖ 0 ˙ → I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ N ⁡ z ∨ ˙ N ⁡ Y ↔ N ⁡ X ⊆ N ⁡ z ∨ ˙ N ⁡ Y
78 69 77 bitr3d ⊢ φ ∧ z ∈ V ∖ 0 ˙ → I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ N ⁡ z join ⁡ K I -1 ⁡ N ⁡ Y ↔ N ⁡ X ⊆ N ⁡ z ∨ ˙ N ⁡ Y
79 66 78 anbi12d ⊢ φ ∧ z ∈ V ∖ 0 ˙ → I -1 ⁡ N ⁡ z ≤ K I -1 ⁡ S ∧ I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ N ⁡ z join ⁡ K I -1 ⁡ N ⁡ Y ↔ N ⁡ z ⊆ S ∧ N ⁡ X ⊆ N ⁡ z ∨ ˙ N ⁡ Y
80 79 rexbidva ⊢ φ → ∃ z ∈ V ∖ 0 ˙ I -1 ⁡ N ⁡ z ≤ K I -1 ⁡ S ∧ I -1 ⁡ N ⁡ X ≤ K I -1 ⁡ N ⁡ z join ⁡ K I -1 ⁡ N ⁡ Y ↔ ∃ z ∈ V ∖ 0 ˙ N ⁡ z ⊆ S ∧ N ⁡ X ⊆ N ⁡ z ∨ ˙ N ⁡ Y
81 62 80 bitr2d ⊢ φ → ∃ z ∈ V ∖ 0 ˙ N ⁡ z ⊆ S ∧ N ⁡ X ⊆ N ⁡ z ∨ ˙ N ⁡ Y ↔ ∃ r ∈ Atoms ⁡ K r ≤ K I -1 ⁡ S ∧ I -1 ⁡ N ⁡ X ≤ K r join ⁡ K I -1 ⁡ N ⁡ Y
82 31 48 81 3imtr4d ⊢ φ → S ≠ 0 ˙ ∧ N ⁡ X ⊆ S ∨ ˙ N ⁡ Y → ∃ z ∈ V ∖ 0 ˙ N ⁡ z ⊆ S ∧ N ⁡ X ⊆ N ⁡ z ∨ ˙ N ⁡ Y