This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 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