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	$⊢ S = LSubSp (W)$
	lsatexch.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lsatexch.o	$⊢ \underset{˙}{0} = 0_{W}$
	lsatexch.a	$⊢ A = LSAtoms (W)$
	lsatexch.w	$⊢ φ \to W \in LVec$
	lsatexch.u	$⊢ φ \to U \in S$
	lsatexch.q	$⊢ φ \to Q \in A$
	lsatexch.r	$⊢ φ \to R \in A$
	lsatexch.l	$⊢ φ \to Q \subseteq U \underset{˙}{\oplus} R$
	lsatexch.z	$⊢ φ \to U \cap Q = \{\underset{˙}{0}\}$
Assertion	lsatexch	$⊢ φ \to R \subseteq U \underset{˙}{\oplus} Q$

Proof

Step	Hyp	Ref	Expression
1		lsatexch.s	$⊢ S = LSubSp (W)$
2		lsatexch.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		lsatexch.o	$⊢ \underset{˙}{0} = 0_{W}$
4		lsatexch.a	$⊢ A = LSAtoms (W)$
5		lsatexch.w	$⊢ φ \to W \in LVec$
6		lsatexch.u	$⊢ φ \to U \in S$
7		lsatexch.q	$⊢ φ \to Q \in A$
8		lsatexch.r	$⊢ φ \to R \in A$
9		lsatexch.l	$⊢ φ \to Q \subseteq U \underset{˙}{\oplus} R$
10		lsatexch.z	$⊢ φ \to U \cap Q = \{\underset{˙}{0}\}$
11		lveclmod	$⊢ W \in LVec \to W \in LMod$
12	5 11	syl	$⊢ φ \to W \in LMod$
13	1	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$
14	12 13	syl	$⊢ φ \to S \subseteq SubGrp (W)$
15	14 6	sseldd	$⊢ φ \to U \in SubGrp (W)$
16	1 4 12 8	lsatlssel	$⊢ φ \to R \in S$
17	14 16	sseldd	$⊢ φ \to R \in SubGrp (W)$
18	2	lsmub2	$⊢ (U \in SubGrp (W) \land R \in SubGrp (W)) \to R \subseteq U \underset{˙}{\oplus} R$
19	15 17 18	syl2anc	$⊢ φ \to R \subseteq U \underset{˙}{\oplus} R$
20		eqid	$⊢ ⋖_{L} (W) = ⋖_{L} (W)$
21	1 2	lsmcl	$⊢ (W \in LMod \land U \in S \land R \in S) \to U \underset{˙}{\oplus} R \in S$
22	12 6 16 21	syl3anc	$⊢ φ \to U \underset{˙}{\oplus} R \in S$
23	1 4 12 7	lsatlssel	$⊢ φ \to Q \in S$
24	1 2	lsmcl	$⊢ (W \in LMod \land U \in S \land Q \in S) \to U \underset{˙}{\oplus} Q \in S$
25	12 6 23 24	syl3anc	$⊢ φ \to U \underset{˙}{\oplus} Q \in S$
26	1 2 3 4 20 5 6 7	lcvp	$⊢ φ \to (U \cap Q = \{\underset{˙}{0}\} \leftrightarrow U ⋖_{L} (W) (U \underset{˙}{\oplus} Q))$
27	10 26	mpbid	$⊢ φ \to U ⋖_{L} (W) (U \underset{˙}{\oplus} Q)$
28	1 20 5 6 25 27	lcvpss	$⊢ φ \to U \subset U \underset{˙}{\oplus} Q$
29	2	lsmub1	$⊢ (U \in SubGrp (W) \land R \in SubGrp (W)) \to U \subseteq U \underset{˙}{\oplus} R$
30	15 17 29	syl2anc	$⊢ φ \to U \subseteq U \underset{˙}{\oplus} R$
31	14 23	sseldd	$⊢ φ \to Q \in SubGrp (W)$
32	14 22	sseldd	$⊢ φ \to U \underset{˙}{\oplus} R \in SubGrp (W)$
33	2	lsmlub	$⊢ (U \in SubGrp (W) \land Q \in SubGrp (W) \land U \underset{˙}{\oplus} R \in SubGrp (W)) \to ((U \subseteq U \underset{˙}{\oplus} R \land Q \subseteq U \underset{˙}{\oplus} R) \leftrightarrow U \underset{˙}{\oplus} Q \subseteq U \underset{˙}{\oplus} R)$
34	15 31 32 33	syl3anc	$⊢ φ \to ((U \subseteq U \underset{˙}{\oplus} R \land Q \subseteq U \underset{˙}{\oplus} R) \leftrightarrow U \underset{˙}{\oplus} Q \subseteq U \underset{˙}{\oplus} R)$
35	30 9 34	mpbi2and	$⊢ φ \to U \underset{˙}{\oplus} Q \subseteq U \underset{˙}{\oplus} R$
36	28 35	psssstrd	$⊢ φ \to U \subset U \underset{˙}{\oplus} R$
37	1 2 4 20 5 6 8	lcv2	$⊢ φ \to (U \subset U \underset{˙}{\oplus} R \leftrightarrow U ⋖_{L} (W) (U \underset{˙}{\oplus} R))$
38	36 37	mpbid	$⊢ φ \to U ⋖_{L} (W) (U \underset{˙}{\oplus} R)$
39	1 20 5 6 22 25 38 28 35	lcvnbtwn2	$⊢ φ \to U \underset{˙}{\oplus} Q = U \underset{˙}{\oplus} R$
40	19 39	sseqtrrd	$⊢ φ \to R \subseteq U \underset{˙}{\oplus} Q$

Metamath Proof Explorer

Theorem lsatexch

Proof