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 = ( 0_g ‘ 𝑊 )
	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 = ( 0_g ‘ 𝑊 )
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	⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑈 ⊕ 𝑄 ) )

Metamath Proof Explorer

Theorem lsatexch

Proof