Metamath Proof Explorer


Theorem lcvfbr

Description: The covers relation for a left vector space (or a left module). (Contributed by NM, 7-Jan-2015)

Ref Expression
Hypotheses lcvfbr.s S = LSubSp W
lcvfbr.c C = L W
lcvfbr.w φ W X
Assertion lcvfbr φ C = t u | t S u S t u ¬ s S t s s u

Proof

Step Hyp Ref Expression
1 lcvfbr.s S = LSubSp W
2 lcvfbr.c C = L W
3 lcvfbr.w φ W X
4 elex W X W V
5 fveq2 w = W LSubSp w = LSubSp W
6 5 1 eqtr4di w = W LSubSp w = S
7 6 eleq2d w = W t LSubSp w t S
8 6 eleq2d w = W u LSubSp w u S
9 7 8 anbi12d w = W t LSubSp w u LSubSp w t S u S
10 6 rexeqdv w = W s LSubSp w t s s u s S t s s u
11 10 notbid w = W ¬ s LSubSp w t s s u ¬ s S t s s u
12 11 anbi2d w = W t u ¬ s LSubSp w t s s u t u ¬ s S t s s u
13 9 12 anbi12d w = W t LSubSp w u LSubSp w t u ¬ s LSubSp w t s s u t S u S t u ¬ s S t s s u
14 13 opabbidv w = W t u | t LSubSp w u LSubSp w t u ¬ s LSubSp w t s s u = t u | t S u S t u ¬ s S t s s u
15 df-lcv L = w V t u | t LSubSp w u LSubSp w t u ¬ s LSubSp w t s s u
16 1 fvexi S V
17 16 16 xpex S × S V
18 opabssxp t u | t S u S t u ¬ s S t s s u S × S
19 17 18 ssexi t u | t S u S t u ¬ s S t s s u V
20 14 15 19 fvmpt W V L W = t u | t S u S t u ¬ s S t s s u
21 3 4 20 3syl φ L W = t u | t S u S t u ¬ s S t s s u
22 2 21 syl5eq φ C = t u | t S u S t u ¬ s S t s s u