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

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 df-pss ⊢ ( 𝑇 ⊊ 𝑠 ↔ ( 𝑇 ⊆ 𝑠 ∧ 𝑇 ≠ 𝑠 ) )
9 necom ⊢ ( 𝑇 ≠ 𝑠 ↔ 𝑠 ≠ 𝑇 )
10 9 anbi2i ⊢ ( ( 𝑇 ⊆ 𝑠 ∧ 𝑇 ≠ 𝑠 ) ↔ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ≠ 𝑇 ) )
11 8 10 bitri ⊢ ( 𝑇 ⊊ 𝑠 ↔ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ≠ 𝑇 ) )
12 df-pss ⊢ ( 𝑠 ⊊ 𝑈 ↔ ( 𝑠 ⊆ 𝑈 ∧ 𝑠 ≠ 𝑈 ) )
13 11 12 anbi12i ⊢ ( ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ↔ ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ≠ 𝑇 ) ∧ ( 𝑠 ⊆ 𝑈 ∧ 𝑠 ≠ 𝑈 ) ) )
14 an4 ⊢ ( ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ≠ 𝑇 ) ∧ ( 𝑠 ⊆ 𝑈 ∧ 𝑠 ≠ 𝑈 ) ) ↔ ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ∧ ( 𝑠 ≠ 𝑇 ∧ 𝑠 ≠ 𝑈 ) ) )
15 neanior ⊢ ( ( 𝑠 ≠ 𝑇 ∧ 𝑠 ≠ 𝑈 ) ↔ ¬ ( 𝑠 = 𝑇 ∨ 𝑠 = 𝑈 ) )
16 15 anbi2i ⊢ ( ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ∧ ( 𝑠 ≠ 𝑇 ∧ 𝑠 ≠ 𝑈 ) ) ↔ ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ∧ ¬ ( 𝑠 = 𝑇 ∨ 𝑠 = 𝑈 ) ) )
17 14 16 bitri ⊢ ( ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ≠ 𝑇 ) ∧ ( 𝑠 ⊆ 𝑈 ∧ 𝑠 ≠ 𝑈 ) ) ↔ ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ∧ ¬ ( 𝑠 = 𝑇 ∨ 𝑠 = 𝑈 ) ) )
18 13 17 bitri ⊢ ( ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ↔ ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) ∧ ¬ ( 𝑠 = 𝑇 ∨ 𝑠 = 𝑈 ) ) )
19 7 18 xchbinxr ⊢ ( ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → ( 𝑠 = 𝑇 ∨ 𝑠 = 𝑈 ) ) ↔ ¬ ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) )
20 19 ralbii ⊢ ( ∀ 𝑠 ∈ 𝑆 ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → ( 𝑠 = 𝑇 ∨ 𝑠 = 𝑈 ) ) ↔ ∀ 𝑠 ∈ 𝑆 ¬ ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) )
21 ralnex ⊢ ( ∀ 𝑠 ∈ 𝑆 ¬ ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ↔ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) )
22 20 21 bitri ⊢ ( ∀ 𝑠 ∈ 𝑆 ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → ( 𝑠 = 𝑇 ∨ 𝑠 = 𝑈 ) ) ↔ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) )
23 22 anbi2i ⊢ ( ( 𝑇 ⊊ 𝑈 ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → ( 𝑠 = 𝑇 ∨ 𝑠 = 𝑈 ) ) ) ↔ ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) )
24 6 23 bitr4di ⊢ ( 𝜑 → ( 𝑇 𝐶 𝑈 ↔ ( 𝑇 ⊊ 𝑈 ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → ( 𝑠 = 𝑇 ∨ 𝑠 = 𝑈 ) ) ) ) )