Metamath Proof Explorer


Theorem lcvbr3

Description: The covers relation for a left vector space (or a left module). (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 lcvbr3 φ T C U T U s S T s s U s = T 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 = T s = U ¬ T s s U ¬ s = T s = U
8 df-pss T s T s T s
9 necom T s s T
10 9 anbi2i T s T s T s s T
11 8 10 bitri T s T s s T
12 df-pss s U s U s U
13 11 12 anbi12i T s s U T s s T s U s U
14 an4 T s s T s U s U T s s U s T s U
15 neanior s T s U ¬ s = T s = U
16 15 anbi2i T s s U s T s U T s s U ¬ s = T s = U
17 14 16 bitri T s s T s U s U T s s U ¬ s = T s = U
18 13 17 bitri T s s U T s s U ¬ s = T s = U
19 7 18 xchbinxr T s s U s = T s = U ¬ T s s U
20 19 ralbii s S T s s U s = T s = U s S ¬ T s s U
21 ralnex s S ¬ T s s U ¬ s S T s s U
22 20 21 bitri s S T s s U s = T s = U ¬ s S T s s U
23 22 anbi2i T U s S T s s U s = T s = U T U ¬ s S T s s U
24 6 23 bitr4di φ T C U T U s S T s s U s = T s = U