Metamath Proof Explorer

Theorem lcvntr

Description: The covers relation is not transitive. ( cvntr analog.) (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lcvnbtwn.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lcvnbtwn.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
lcvnbtwn.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
lcvnbtwn.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
lcvnbtwn.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
lcvnbtwn.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lcvnbtwn.d ⊢ ( 𝜑 → 𝑅 𝐶 𝑇 )
lcvntr.p ⊢ ( 𝜑 → 𝑇 𝐶 𝑈 )
Assertion lcvntr ( 𝜑 → ¬ 𝑅 𝐶 𝑈 )

Proof

Step Hyp Ref Expression
1 lcvnbtwn.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lcvnbtwn.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
3 lcvnbtwn.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
4 lcvnbtwn.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
5 lcvnbtwn.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
6 lcvnbtwn.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7 lcvnbtwn.d ⊢ ( 𝜑 → 𝑅 𝐶 𝑇 )
8 lcvntr.p ⊢ ( 𝜑 → 𝑇 𝐶 𝑈 )
9 1 2 3 4 5 7 lcvpss ⊢ ( 𝜑 → 𝑅 ⊊ 𝑇 )
10 1 2 3 5 6 8 lcvpss ⊢ ( 𝜑 → 𝑇 ⊊ 𝑈 )
11 9 10 jca ⊢ ( 𝜑 → ( 𝑅 ⊊ 𝑇 ∧ 𝑇 ⊊ 𝑈 ) )
12 3 adantr ⊢ ( ( 𝜑 ∧ 𝑅 𝐶 𝑈 ) → 𝑊 ∈ 𝑋 )
13 4 adantr ⊢ ( ( 𝜑 ∧ 𝑅 𝐶 𝑈 ) → 𝑅 ∈ 𝑆 )
14 6 adantr ⊢ ( ( 𝜑 ∧ 𝑅 𝐶 𝑈 ) → 𝑈 ∈ 𝑆 )
15 5 adantr ⊢ ( ( 𝜑 ∧ 𝑅 𝐶 𝑈 ) → 𝑇 ∈ 𝑆 )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑅 𝐶 𝑈 ) → 𝑅 𝐶 𝑈 )
17 1 2 12 13 14 15 16 lcvnbtwn ⊢ ( ( 𝜑 ∧ 𝑅 𝐶 𝑈 ) → ¬ ( 𝑅 ⊊ 𝑇 ∧ 𝑇 ⊊ 𝑈 ) )
18 17 ex ⊢ ( 𝜑 → ( 𝑅 𝐶 𝑈 → ¬ ( 𝑅 ⊊ 𝑇 ∧ 𝑇 ⊊ 𝑈 ) ) )
19 11 18 mt2d ⊢ ( 𝜑 → ¬ 𝑅 𝐶 𝑈 )