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 𝑆 = ( LSubSp ‘ 𝑊 )
lcvfbr.c 𝐶 = ( ⋖L𝑊 )
lcvfbr.w ( 𝜑𝑊𝑋 )
lcvfbr.t ( 𝜑𝑇𝑆 )
lcvfbr.u ( 𝜑𝑈𝑆 )
Assertion lcvbr2 ( 𝜑 → ( 𝑇 𝐶 𝑈 ↔ ( 𝑇𝑈 ∧ ∀ 𝑠𝑆 ( ( 𝑇𝑠𝑠𝑈 ) → 𝑠 = 𝑈 ) ) ) )

Proof

Step Hyp Ref Expression
1 lcvfbr.s 𝑆 = ( LSubSp ‘ 𝑊 )
2 lcvfbr.c 𝐶 = ( ⋖L𝑊 )
3 lcvfbr.w ( 𝜑𝑊𝑋 )
4 lcvfbr.t ( 𝜑𝑇𝑆 )
5 lcvfbr.u ( 𝜑𝑈𝑆 )
6 1 2 3 4 5 lcvbr ( 𝜑 → ( 𝑇 𝐶 𝑈 ↔ ( 𝑇𝑈 ∧ ¬ ∃ 𝑠𝑆 ( 𝑇𝑠𝑠𝑈 ) ) ) )
7 iman ( ( ( 𝑇𝑠𝑠𝑈 ) → 𝑠 = 𝑈 ) ↔ ¬ ( ( 𝑇𝑠𝑠𝑈 ) ∧ ¬ 𝑠 = 𝑈 ) )
8 anass ( ( ( 𝑇𝑠𝑠𝑈 ) ∧ ¬ 𝑠 = 𝑈 ) ↔ ( 𝑇𝑠 ∧ ( 𝑠𝑈 ∧ ¬ 𝑠 = 𝑈 ) ) )
9 dfpss2 ( 𝑠𝑈 ↔ ( 𝑠𝑈 ∧ ¬ 𝑠 = 𝑈 ) )
10 9 anbi2i ( ( 𝑇𝑠𝑠𝑈 ) ↔ ( 𝑇𝑠 ∧ ( 𝑠𝑈 ∧ ¬ 𝑠 = 𝑈 ) ) )
11 8 10 bitr4i ( ( ( 𝑇𝑠𝑠𝑈 ) ∧ ¬ 𝑠 = 𝑈 ) ↔ ( 𝑇𝑠𝑠𝑈 ) )
12 7 11 xchbinx ( ( ( 𝑇𝑠𝑠𝑈 ) → 𝑠 = 𝑈 ) ↔ ¬ ( 𝑇𝑠𝑠𝑈 ) )
13 12 ralbii ( ∀ 𝑠𝑆 ( ( 𝑇𝑠𝑠𝑈 ) → 𝑠 = 𝑈 ) ↔ ∀ 𝑠𝑆 ¬ ( 𝑇𝑠𝑠𝑈 ) )
14 ralnex ( ∀ 𝑠𝑆 ¬ ( 𝑇𝑠𝑠𝑈 ) ↔ ¬ ∃ 𝑠𝑆 ( 𝑇𝑠𝑠𝑈 ) )
15 13 14 bitri ( ∀ 𝑠𝑆 ( ( 𝑇𝑠𝑠𝑈 ) → 𝑠 = 𝑈 ) ↔ ¬ ∃ 𝑠𝑆 ( 𝑇𝑠𝑠𝑈 ) )
16 15 anbi2i ( ( 𝑇𝑈 ∧ ∀ 𝑠𝑆 ( ( 𝑇𝑠𝑠𝑈 ) → 𝑠 = 𝑈 ) ) ↔ ( 𝑇𝑈 ∧ ¬ ∃ 𝑠𝑆 ( 𝑇𝑠𝑠𝑈 ) ) )
17 6 16 bitr4di ( 𝜑 → ( 𝑇 𝐶 𝑈 ↔ ( 𝑇𝑈 ∧ ∀ 𝑠𝑆 ( ( 𝑇𝑠𝑠𝑈 ) → 𝑠 = 𝑈 ) ) ) )