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	⊢ ( 𝜑 → ( 𝑇 𝐶 𝑈 ↔ ( 𝑇 ⊊ 𝑈 ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊆ 𝑈 ) → 𝑠 = 𝑈 ) ) ) )