Metamath Proof Explorer

Theorem lssatle

Description: The ordering of two subspaces is determined by the atoms under them. ( chrelat3 analog.) (Contributed by NM, 29-Oct-2014)

Ref Expression
Hypotheses lssatle.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lssatle.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lssatle.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lssatle.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
lssatle.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
Assertion lssatle ( 𝜑 → ( 𝑇 ⊆ 𝑈 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 lssatle.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lssatle.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3 lssatle.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
4 lssatle.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
5 lssatle.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6 sstr ⊢ ( ( 𝑝 ⊆ 𝑇 ∧ 𝑇 ⊆ 𝑈 ) → 𝑝 ⊆ 𝑈 )
7 6 expcom ⊢ ( 𝑇 ⊆ 𝑈 → ( 𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈 ) )
8 7 ralrimivw ⊢ ( 𝑇 ⊆ 𝑈 → ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈 ) )
9 ss2rab ⊢ ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈 ) )
10 1 2 lsatlss ⊢ ( 𝑊 ∈ LMod → 𝐴 ⊆ 𝑆 )
11 rabss2 ⊢ ( 𝐴 ⊆ 𝑆 → { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } )
12 uniss ⊢ ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } )
13 3 10 11 12 4syl ⊢ ( 𝜑 → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } )
14 unimax ⊢ ( 𝑈 ∈ 𝑆 → ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } = 𝑈 )
15 5 14 syl ⊢ ( 𝜑 → ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } = 𝑈 )
16 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
17 16 1 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
18 5 17 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
19 15 18 eqsstrd ⊢ ( 𝜑 → ∪ { 𝑝 ∈ 𝑆 ∣ 𝑝 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) )
20 13 19 sstrd ⊢ ( 𝜑 → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) )
21 uniss ⊢ ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } → ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } )
22 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
23 16 22 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) ∧ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) )
24 3 20 21 23 syl2an3an ⊢ ( ( 𝜑 ∧ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) → ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) )
25 24 ex ⊢ ( 𝜑 → ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } → ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) ) )
26 1 22 2 lssats ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ) → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ) )
27 3 4 26 syl2anc ⊢ ( 𝜑 → 𝑇 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ) )
28 1 22 2 lssats ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) )
29 3 5 28 syl2anc ⊢ ( 𝜑 → 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) )
30 27 29 sseq12d ⊢ ( 𝜑 → ( 𝑇 ⊆ 𝑈 ↔ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ∪ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } ) ) )
31 25 30 sylibrd ⊢ ( 𝜑 → ( { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑇 } ⊆ { 𝑝 ∈ 𝐴 ∣ 𝑝 ⊆ 𝑈 } → 𝑇 ⊆ 𝑈 ) )
32 9 31 biimtrrid ⊢ ( 𝜑 → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈 ) → 𝑇 ⊆ 𝑈 ) )
33 8 32 impbid2 ⊢ ( 𝜑 → ( 𝑇 ⊆ 𝑈 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 → 𝑝 ⊆ 𝑈 ) ) )