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

Proof

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