Metamath Proof Explorer

Theorem lcvfbr

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

Ref Expression
Hypotheses lcvfbr.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lcvfbr.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
lcvfbr.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
Assertion lcvfbr ( 𝜑 → 𝐶 = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } )

Proof

Step Hyp Ref Expression
1 lcvfbr.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lcvfbr.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
3 lcvfbr.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
4 elex ⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
5 fveq2 ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = ( LSubSp ‘ 𝑊 ) )
6 5 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = 𝑆 )
7 6 eleq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ↔ 𝑡 ∈ 𝑆 ) )
8 6 eleq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ↔ 𝑢 ∈ 𝑆 ) )
9 7 8 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ↔ ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) )
10 6 rexeqdv ⊢ ( 𝑤 = 𝑊 → ( ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ↔ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) )
11 10 notbid ⊢ ( 𝑤 = 𝑊 → ( ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ↔ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) )
12 11 anbi2d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ↔ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) )
13 9 12 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) ↔ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) ) )
14 13 opabbidv ⊢ ( 𝑤 = 𝑊 → { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } )
15 df-lcv ⊢ ⋖L = ( 𝑤 ∈ V ↦ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } )
16 1 fvexi ⊢ 𝑆 ∈ V
17 16 16 xpex ⊢ ( 𝑆 × 𝑆 ) ∈ V
18 opabssxp ⊢ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } ⊆ ( 𝑆 × 𝑆 )
19 17 18 ssexi ⊢ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } ∈ V
20 14 15 19 fvmpt ⊢ ( 𝑊 ∈ V → ( ⋖L ‘ 𝑊 ) = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } )
21 3 4 20 3syl ⊢ ( 𝜑 → ( ⋖L ‘ 𝑊 ) = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } )
22 2 21 syl5eq ⊢ ( 𝜑 → 𝐶 = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } )