Metamath Proof Explorer


Theorem l1cvat

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

Ref Expression
Hypotheses l1cvat.v V = Base W
l1cvat.s S = LSubSp W
l1cvat.p ˙ = LSSum W
l1cvat.a A = LSAtoms W
l1cvat.c C = L W
l1cvat.w φ W LVec
l1cvat.u φ U S
l1cvat.q φ Q A
l1cvat.r φ R A
l1cvat.n φ Q R
l1cvat.l φ U C V
l1cvat.m φ ¬ Q U
Assertion l1cvat φ Q ˙ R U A

Proof

Step Hyp Ref Expression
1 l1cvat.v V = Base W
2 l1cvat.s S = LSubSp W
3 l1cvat.p ˙ = LSSum W
4 l1cvat.a A = LSAtoms W
5 l1cvat.c C = L W
6 l1cvat.w φ W LVec
7 l1cvat.u φ U S
8 l1cvat.q φ Q A
9 l1cvat.r φ R A
10 l1cvat.n φ Q R
11 l1cvat.l φ U C V
12 l1cvat.m φ ¬ Q U
13 lveclmod W LVec W LMod
14 6 13 syl φ W LMod
15 lmodabl W LMod W Abel
16 14 15 syl φ W Abel
17 2 lsssssubg W LMod S SubGrp W
18 14 17 syl φ S SubGrp W
19 2 4 14 8 lsatlssel φ Q S
20 18 19 sseldd φ Q SubGrp W
21 2 4 14 9 lsatlssel φ R S
22 18 21 sseldd φ R SubGrp W
23 3 lsmcom W Abel Q SubGrp W R SubGrp W Q ˙ R = R ˙ Q
24 16 20 22 23 syl3anc φ Q ˙ R = R ˙ Q
25 24 ineq1d φ Q ˙ R U = R ˙ Q U
26 incom R ˙ Q U = U R ˙ Q
27 25 26 eqtrdi φ Q ˙ R U = U R ˙ Q
28 10 necomd φ R Q
29 1 4 14 9 lsatssv φ R V
30 1 2 3 4 5 6 7 8 11 12 l1cvpat φ U ˙ Q = V
31 29 30 sseqtrrd φ R U ˙ Q
32 2 3 4 6 7 9 8 28 12 31 lsatcvat3 φ U R ˙ Q A
33 27 32 eqeltrd φ Q ˙ R U A