Metamath Proof Explorer


Theorem lsatcmp2

Description: If an atom is included in at-most an atom, they are equal. More general version of lsatcmp . TODO: can lspsncmp shorten this? (Contributed by NM, 3-Feb-2015)

Ref Expression
Hypotheses lsatcmp2.o 0 = ( 0g𝑊 )
lsatcmp2.a 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatcmp2.w ( 𝜑𝑊 ∈ LVec )
lsatcmp2.t ( 𝜑𝑇𝐴 )
lsatcmp2.u ( 𝜑 → ( 𝑈𝐴𝑈 = { 0 } ) )
Assertion lsatcmp2 ( 𝜑 → ( 𝑇𝑈𝑇 = 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lsatcmp2.o 0 = ( 0g𝑊 )
2 lsatcmp2.a 𝐴 = ( LSAtoms ‘ 𝑊 )
3 lsatcmp2.w ( 𝜑𝑊 ∈ LVec )
4 lsatcmp2.t ( 𝜑𝑇𝐴 )
5 lsatcmp2.u ( 𝜑 → ( 𝑈𝐴𝑈 = { 0 } ) )
6 simpr ( ( 𝜑𝑇𝑈 ) → 𝑇𝑈 )
7 3 adantr ( ( 𝜑𝑇𝑈 ) → 𝑊 ∈ LVec )
8 4 adantr ( ( 𝜑𝑇𝑈 ) → 𝑇𝐴 )
9 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10 3 9 syl ( 𝜑𝑊 ∈ LMod )
11 10 adantr ( ( 𝜑𝑇𝑈 ) → 𝑊 ∈ LMod )
12 1 2 11 8 6 lsatssn0 ( ( 𝜑𝑇𝑈 ) → 𝑈 ≠ { 0 } )
13 5 ord ( 𝜑 → ( ¬ 𝑈𝐴𝑈 = { 0 } ) )
14 13 necon1ad ( 𝜑 → ( 𝑈 ≠ { 0 } → 𝑈𝐴 ) )
15 14 adantr ( ( 𝜑𝑇𝑈 ) → ( 𝑈 ≠ { 0 } → 𝑈𝐴 ) )
16 12 15 mpd ( ( 𝜑𝑇𝑈 ) → 𝑈𝐴 )
17 2 7 8 16 lsatcmp ( ( 𝜑𝑇𝑈 ) → ( 𝑇𝑈𝑇 = 𝑈 ) )
18 6 17 mpbid ( ( 𝜑𝑇𝑈 ) → 𝑇 = 𝑈 )
19 18 ex ( 𝜑 → ( 𝑇𝑈𝑇 = 𝑈 ) )
20 eqimss ( 𝑇 = 𝑈𝑇𝑈 )
21 19 20 impbid1 ( 𝜑 → ( 𝑇𝑈𝑇 = 𝑈 ) )