Metamath Proof Explorer


Theorem lsatexch

Description: The atom exchange property. Proposition 1(i) of Kalmbach p. 140. A version of this theorem was originally proved by Hermann Grassmann in 1862. ( atexch analog.) (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lsatexch.s 𝑆 = ( LSubSp ‘ 𝑊 )
lsatexch.p = ( LSSum ‘ 𝑊 )
lsatexch.o 0 = ( 0g𝑊 )
lsatexch.a 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatexch.w ( 𝜑𝑊 ∈ LVec )
lsatexch.u ( 𝜑𝑈𝑆 )
lsatexch.q ( 𝜑𝑄𝐴 )
lsatexch.r ( 𝜑𝑅𝐴 )
lsatexch.l ( 𝜑𝑄 ⊆ ( 𝑈 𝑅 ) )
lsatexch.z ( 𝜑 → ( 𝑈𝑄 ) = { 0 } )
Assertion lsatexch ( 𝜑𝑅 ⊆ ( 𝑈 𝑄 ) )

Proof

Step Hyp Ref Expression
1 lsatexch.s 𝑆 = ( LSubSp ‘ 𝑊 )
2 lsatexch.p = ( LSSum ‘ 𝑊 )
3 lsatexch.o 0 = ( 0g𝑊 )
4 lsatexch.a 𝐴 = ( LSAtoms ‘ 𝑊 )
5 lsatexch.w ( 𝜑𝑊 ∈ LVec )
6 lsatexch.u ( 𝜑𝑈𝑆 )
7 lsatexch.q ( 𝜑𝑄𝐴 )
8 lsatexch.r ( 𝜑𝑅𝐴 )
9 lsatexch.l ( 𝜑𝑄 ⊆ ( 𝑈 𝑅 ) )
10 lsatexch.z ( 𝜑 → ( 𝑈𝑄 ) = { 0 } )
11 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
12 5 11 syl ( 𝜑𝑊 ∈ LMod )
13 1 lsssssubg ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
14 12 13 syl ( 𝜑𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
15 14 6 sseldd ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
16 1 4 12 8 lsatlssel ( 𝜑𝑅𝑆 )
17 14 16 sseldd ( 𝜑𝑅 ∈ ( SubGrp ‘ 𝑊 ) )
18 2 lsmub2 ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ) → 𝑅 ⊆ ( 𝑈 𝑅 ) )
19 15 17 18 syl2anc ( 𝜑𝑅 ⊆ ( 𝑈 𝑅 ) )
20 eqid ( ⋖L𝑊 ) = ( ⋖L𝑊 )
21 1 2 lsmcl ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆𝑅𝑆 ) → ( 𝑈 𝑅 ) ∈ 𝑆 )
22 12 6 16 21 syl3anc ( 𝜑 → ( 𝑈 𝑅 ) ∈ 𝑆 )
23 1 4 12 7 lsatlssel ( 𝜑𝑄𝑆 )
24 1 2 lsmcl ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆𝑄𝑆 ) → ( 𝑈 𝑄 ) ∈ 𝑆 )
25 12 6 23 24 syl3anc ( 𝜑 → ( 𝑈 𝑄 ) ∈ 𝑆 )
26 1 2 3 4 20 5 6 7 lcvp ( 𝜑 → ( ( 𝑈𝑄 ) = { 0 } ↔ 𝑈 ( ⋖L𝑊 ) ( 𝑈 𝑄 ) ) )
27 10 26 mpbid ( 𝜑𝑈 ( ⋖L𝑊 ) ( 𝑈 𝑄 ) )
28 1 20 5 6 25 27 lcvpss ( 𝜑𝑈 ⊊ ( 𝑈 𝑄 ) )
29 2 lsmub1 ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ) → 𝑈 ⊆ ( 𝑈 𝑅 ) )
30 15 17 29 syl2anc ( 𝜑𝑈 ⊆ ( 𝑈 𝑅 ) )
31 14 23 sseldd ( 𝜑𝑄 ∈ ( SubGrp ‘ 𝑊 ) )
32 14 22 sseldd ( 𝜑 → ( 𝑈 𝑅 ) ∈ ( SubGrp ‘ 𝑊 ) )
33 2 lsmlub ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑄 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑈 𝑅 ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( 𝑈 ⊆ ( 𝑈 𝑅 ) ∧ 𝑄 ⊆ ( 𝑈 𝑅 ) ) ↔ ( 𝑈 𝑄 ) ⊆ ( 𝑈 𝑅 ) ) )
34 15 31 32 33 syl3anc ( 𝜑 → ( ( 𝑈 ⊆ ( 𝑈 𝑅 ) ∧ 𝑄 ⊆ ( 𝑈 𝑅 ) ) ↔ ( 𝑈 𝑄 ) ⊆ ( 𝑈 𝑅 ) ) )
35 30 9 34 mpbi2and ( 𝜑 → ( 𝑈 𝑄 ) ⊆ ( 𝑈 𝑅 ) )
36 28 35 psssstrd ( 𝜑𝑈 ⊊ ( 𝑈 𝑅 ) )
37 1 2 4 20 5 6 8 lcv2 ( 𝜑 → ( 𝑈 ⊊ ( 𝑈 𝑅 ) ↔ 𝑈 ( ⋖L𝑊 ) ( 𝑈 𝑅 ) ) )
38 36 37 mpbid ( 𝜑𝑈 ( ⋖L𝑊 ) ( 𝑈 𝑅 ) )
39 1 20 5 6 22 25 38 28 35 lcvnbtwn2 ( 𝜑 → ( 𝑈 𝑄 ) = ( 𝑈 𝑅 ) )
40 19 39 sseqtrrd ( 𝜑𝑅 ⊆ ( 𝑈 𝑄 ) )