Theorem lcvbr

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

	Ref	Expression
Hypotheses	lcvfbr.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lcvfbr.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
	lcvfbr.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
	lcvfbr.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
	lcvfbr.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
Assertion	lcvbr	⊢ ( 𝜑 → ( 𝑇 𝐶 𝑈 ↔ ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcvfbr.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lcvfbr.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
3		lcvfbr.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
4		lcvfbr.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
5		lcvfbr.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6		eleq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ∈ 𝑆 ↔ 𝑇 ∈ 𝑆 ) )
7	6	anbi1d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ↔ ( 𝑇 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) )
8		psseq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ⊊ 𝑢 ↔ 𝑇 ⊊ 𝑢 ) )
9		psseq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ⊊ 𝑠 ↔ 𝑇 ⊊ 𝑠 ) )
10	9	anbi1d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ↔ ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) )
11	10	rexbidv	⊢ ( 𝑡 = 𝑇 → ( ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ↔ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) )
12	11	notbid	⊢ ( 𝑡 = 𝑇 → ( ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ↔ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) )
13	8 12	anbi12d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ↔ ( 𝑇 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) )
14	7 13	anbi12d	⊢ ( 𝑡 = 𝑇 → ( ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) ↔ ( ( 𝑇 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑇 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) ) )
15		eleq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 ∈ 𝑆 ↔ 𝑈 ∈ 𝑆 ) )
16	15	anbi2d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑇 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ↔ ( 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ) )
17		psseq2	⊢ ( 𝑢 = 𝑈 → ( 𝑇 ⊊ 𝑢 ↔ 𝑇 ⊊ 𝑈 ) )
18		psseq2	⊢ ( 𝑢 = 𝑈 → ( 𝑠 ⊊ 𝑢 ↔ 𝑠 ⊊ 𝑈 ) )
19	18	anbi2d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ↔ ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) )
20	19	rexbidv	⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ↔ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) )
21	20	notbid	⊢ ( 𝑢 = 𝑈 → ( ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ↔ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) )
22	17 21	anbi12d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑇 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ↔ ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) ) )
23	16 22	anbi12d	⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑇 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑇 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) ↔ ( ( 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) ) ) )
24		eqid	⊢ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) }
25	14 23 24	brabg	⊢ ( ( 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } 𝑈 ↔ ( ( 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) ) ) )
26	4 5 25	syl2anc	⊢ ( 𝜑 → ( 𝑇 { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } 𝑈 ↔ ( ( 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) ) ) )
27	1 2 3	lcvfbr	⊢ ( 𝜑 → 𝐶 = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } )
28	27	breqd	⊢ ( 𝜑 → ( 𝑇 𝐶 𝑈 ↔ 𝑇 { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } 𝑈 ) )
29	4 5	jca	⊢ ( 𝜑 → ( 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) )
30	29	biantrurd	⊢ ( 𝜑 → ( ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) ↔ ( ( 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) ) ) )
31	26 28 30	3bitr4d	⊢ ( 𝜑 → ( 𝑇 𝐶 𝑈 ↔ ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) ) )