l1cvat

Description: Create an atom under an element covered by the lattice unity. Part of proof of Lemma B in Crawley p. 112. ( 1cvrat analog.) (Contributed by NM, 11-Jan-2015)

	Ref	Expression
Hypotheses	l1cvat.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	l1cvat.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	l1cvat.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	l1cvat.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	l1cvat.c	⊢ 𝐶 = ( ⋖_L ‘ 𝑊 )
	l1cvat.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	l1cvat.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	l1cvat.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
	l1cvat.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
	l1cvat.n	⊢ ( 𝜑 → 𝑄 ≠ 𝑅 )
	l1cvat.l	⊢ ( 𝜑 → 𝑈 𝐶 𝑉 )
	l1cvat.m	⊢ ( 𝜑 → ¬ 𝑄 ⊆ 𝑈 )
Assertion	l1cvat	⊢ ( 𝜑 → ( ( 𝑄 ⊕ 𝑅 ) ∩ 𝑈 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		l1cvat.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		l1cvat.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		l1cvat.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
4		l1cvat.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5		l1cvat.c	⊢ 𝐶 = ( ⋖_L ‘ 𝑊 )
6		l1cvat.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
7		l1cvat.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
8		l1cvat.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
9		l1cvat.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
10		l1cvat.n	⊢ ( 𝜑 → 𝑄 ≠ 𝑅 )
11		l1cvat.l	⊢ ( 𝜑 → 𝑈 𝐶 𝑉 )
12		l1cvat.m	⊢ ( 𝜑 → ¬ 𝑄 ⊆ 𝑈 )
13		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
14	6 13	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
15		lmodabl	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
16	14 15	syl	⊢ ( 𝜑 → 𝑊 ∈ Abel )
17	2	lsssssubg	⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
18	14 17	syl	⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
19	2 4 14 8	lsatlssel	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
20	18 19	sseldd	⊢ ( 𝜑 → 𝑄 ∈ ( SubGrp ‘ 𝑊 ) )
21	2 4 14 9	lsatlssel	⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
22	18 21	sseldd	⊢ ( 𝜑 → 𝑅 ∈ ( SubGrp ‘ 𝑊 ) )
23	3	lsmcom	⊢ ( ( 𝑊 ∈ Abel ∧ 𝑄 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑄 ⊕ 𝑅 ) = ( 𝑅 ⊕ 𝑄 ) )
24	16 20 22 23	syl3anc	⊢ ( 𝜑 → ( 𝑄 ⊕ 𝑅 ) = ( 𝑅 ⊕ 𝑄 ) )
25	24	ineq1d	⊢ ( 𝜑 → ( ( 𝑄 ⊕ 𝑅 ) ∩ 𝑈 ) = ( ( 𝑅 ⊕ 𝑄 ) ∩ 𝑈 ) )
26		incom	⊢ ( ( 𝑅 ⊕ 𝑄 ) ∩ 𝑈 ) = ( 𝑈 ∩ ( 𝑅 ⊕ 𝑄 ) )
27	25 26	eqtrdi	⊢ ( 𝜑 → ( ( 𝑄 ⊕ 𝑅 ) ∩ 𝑈 ) = ( 𝑈 ∩ ( 𝑅 ⊕ 𝑄 ) ) )
28	10	necomd	⊢ ( 𝜑 → 𝑅 ≠ 𝑄 )
29	1 4 14 9	lsatssv	⊢ ( 𝜑 → 𝑅 ⊆ 𝑉 )
30	1 2 3 4 5 6 7 8 11 12	l1cvpat	⊢ ( 𝜑 → ( 𝑈 ⊕ 𝑄 ) = 𝑉 )
31	29 30	sseqtrrd	⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑈 ⊕ 𝑄 ) )
32	2 3 4 6 7 9 8 28 12 31	lsatcvat3	⊢ ( 𝜑 → ( 𝑈 ∩ ( 𝑅 ⊕ 𝑄 ) ) ∈ 𝐴 )
33	27 32	eqeltrd	⊢ ( 𝜑 → ( ( 𝑄 ⊕ 𝑅 ) ∩ 𝑈 ) ∈ 𝐴 )

Metamath Proof Explorer

Theorem l1cvat

Proof