Metamath Proof Explorer

Theorem lsatcmp

Description: If two atoms are comparable, they are equal. ( atsseq analog.) TODO: can lspsncmp shorten this? (Contributed by NM, 25-Aug-2014)

Ref Expression
Hypotheses lsatcmp.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatcmp.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lsatcmp.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐴 )
lsatcmp.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
Assertion lsatcmp ( 𝜑 → ( 𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lsatcmp.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
2 lsatcmp.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
3 lsatcmp.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐴 )
4 lsatcmp.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
5 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
6 2 5 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
7 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
8 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
9 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
10 7 8 9 1 islsat ⊢ ( 𝑊 ∈ LMod → ( 𝑈 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
11 6 10 syl ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
12 4 11 mpbid ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) )
13 eldifsn ⊢ ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) )
14 9 1 6 3 lsatn0 ⊢ ( 𝜑 → 𝑇 ≠ { ( 0g ‘ 𝑊 ) } )
15 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ) ∧ 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → 𝑇 ≠ { ( 0g ‘ 𝑊 ) } )
16 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ) ∧ 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → 𝑊 ∈ LVec )
17 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
18 17 1 6 3 lsatlssel ⊢ ( 𝜑 → 𝑇 ∈ ( LSubSp ‘ 𝑊 ) )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ) ∧ 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → 𝑇 ∈ ( LSubSp ‘ 𝑊 ) )
20 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ) ∧ 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → 𝑣 ∈ ( Base ‘ 𝑊 ) )
21 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ) ∧ 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) )
22 7 9 17 8 lspsnat ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑇 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∨ 𝑇 = { ( 0g ‘ 𝑊 ) } ) )
23 16 19 20 21 22 syl31anc ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ) ∧ 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ∨ 𝑇 = { ( 0g ‘ 𝑊 ) } ) )
24 23 ord ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ) ∧ 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( ¬ 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → 𝑇 = { ( 0g ‘ 𝑊 ) } ) )
25 24 necon1ad ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ) ∧ 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( 𝑇 ≠ { ( 0g ‘ 𝑊 ) } → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
26 15 25 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ) ∧ 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) )
27 26 ex ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ) → ( 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
28 eqimss ⊢ ( 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) )
29 27 28 impbid1 ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) ) → ( 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ↔ 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
30 29 ex ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ ( 0g ‘ 𝑊 ) ) → ( 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ↔ 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) )
31 13 30 syl5bi ⊢ ( 𝜑 → ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) → ( 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ↔ 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) )
32 sseq2 ⊢ ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑇 ⊆ 𝑈 ↔ 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
33 eqeq2 ⊢ ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑇 = 𝑈 ↔ 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
34 32 33 bibi12d ⊢ ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( ( 𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈 ) ↔ ( 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ↔ 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) )
35 34 biimprcd ⊢ ( ( 𝑇 ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ↔ 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈 ) ) )
36 31 35 syl6 ⊢ ( 𝜑 → ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) → ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈 ) ) ) )
37 36 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈 ) ) )
38 12 37 mpd ⊢ ( 𝜑 → ( 𝑇 ⊆ 𝑈 ↔ 𝑇 = 𝑈 ) )