This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑈 ⊕ 𝑄 ) )