Metamath Proof Explorer


Theorem lcvbr2

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

Ref Expression
Hypotheses lcvfbr.s S = LSubSp W
lcvfbr.c C = L W
lcvfbr.w φ W X
lcvfbr.t φ T S
lcvfbr.u φ U S
Assertion lcvbr2 φ T C U T U s S T s s U 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 lcvfbr.t φ T S
5 lcvfbr.u φ U S
6 1 2 3 4 5 lcvbr φ T C U T U ¬ s S T s s U
7 iman T s s U s = U ¬ T s s U ¬ s = U
8 anass T s s U ¬ s = U T s s U ¬ s = U
9 dfpss2 s U s U ¬ s = U
10 9 anbi2i T s s U T s s U ¬ s = U
11 8 10 bitr4i T s s U ¬ s = U T s s U
12 7 11 xchbinx T s s U s = U ¬ T s s U
13 12 ralbii s S T s s U s = U s S ¬ T s s U
14 ralnex s S ¬ T s s U ¬ s S T s s U
15 13 14 bitri s S T s s U s = U ¬ s S T s s U
16 15 anbi2i T U s S T s s U s = U T U ¬ s S T s s U
17 6 16 bitr4di φ T C U T U s S T s s U s = U