This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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