Metamath Proof Explorer


Theorem lcvexch

Description: Subspaces satisfy the exchange axiom. Lemma 7.5 of MaedaMaeda p. 31. ( cvexchi analog.) TODO: combine some lemmas. (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lcvexch.s 𝑆 = ( LSubSp ‘ 𝑊 )
lcvexch.p = ( LSSum ‘ 𝑊 )
lcvexch.c 𝐶 = ( ⋖L𝑊 )
lcvexch.w ( 𝜑𝑊 ∈ LMod )
lcvexch.t ( 𝜑𝑇𝑆 )
lcvexch.u ( 𝜑𝑈𝑆 )
Assertion lcvexch ( 𝜑 → ( ( 𝑇𝑈 ) 𝐶 𝑈𝑇 𝐶 ( 𝑇 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 lcvexch.s 𝑆 = ( LSubSp ‘ 𝑊 )
2 lcvexch.p = ( LSSum ‘ 𝑊 )
3 lcvexch.c 𝐶 = ( ⋖L𝑊 )
4 lcvexch.w ( 𝜑𝑊 ∈ LMod )
5 lcvexch.t ( 𝜑𝑇𝑆 )
6 lcvexch.u ( 𝜑𝑈𝑆 )
7 4 adantr ( ( 𝜑 ∧ ( 𝑇𝑈 ) 𝐶 𝑈 ) → 𝑊 ∈ LMod )
8 5 adantr ( ( 𝜑 ∧ ( 𝑇𝑈 ) 𝐶 𝑈 ) → 𝑇𝑆 )
9 6 adantr ( ( 𝜑 ∧ ( 𝑇𝑈 ) 𝐶 𝑈 ) → 𝑈𝑆 )
10 simpr ( ( 𝜑 ∧ ( 𝑇𝑈 ) 𝐶 𝑈 ) → ( 𝑇𝑈 ) 𝐶 𝑈 )
11 1 2 3 7 8 9 10 lcvexchlem5 ( ( 𝜑 ∧ ( 𝑇𝑈 ) 𝐶 𝑈 ) → 𝑇 𝐶 ( 𝑇 𝑈 ) )
12 4 adantr ( ( 𝜑𝑇 𝐶 ( 𝑇 𝑈 ) ) → 𝑊 ∈ LMod )
13 5 adantr ( ( 𝜑𝑇 𝐶 ( 𝑇 𝑈 ) ) → 𝑇𝑆 )
14 6 adantr ( ( 𝜑𝑇 𝐶 ( 𝑇 𝑈 ) ) → 𝑈𝑆 )
15 simpr ( ( 𝜑𝑇 𝐶 ( 𝑇 𝑈 ) ) → 𝑇 𝐶 ( 𝑇 𝑈 ) )
16 1 2 3 12 13 14 15 lcvexchlem4 ( ( 𝜑𝑇 𝐶 ( 𝑇 𝑈 ) ) → ( 𝑇𝑈 ) 𝐶 𝑈 )
17 11 16 impbida ( 𝜑 → ( ( 𝑇𝑈 ) 𝐶 𝑈𝑇 𝐶 ( 𝑇 𝑈 ) ) )