Metamath Proof Explorer


Theorem cdlemn11c

Description: Part of proof of Lemma N of Crawley p. 121 line 37. (Contributed by NM, 27-Feb-2014)

Ref Expression
Hypotheses cdlemn11a.b B = Base K
cdlemn11a.l ˙ = K
cdlemn11a.j ˙ = join K
cdlemn11a.a A = Atoms K
cdlemn11a.h H = LHyp K
cdlemn11a.p P = oc K W
cdlemn11a.o O = h T I B
cdlemn11a.t T = LTrn K W
cdlemn11a.r R = trL K W
cdlemn11a.e E = TEndo K W
cdlemn11a.i I = DIsoB K W
cdlemn11a.J J = DIsoC K W
cdlemn11a.u U = DVecH K W
cdlemn11a.d + ˙ = + U
cdlemn11a.s ˙ = LSSum U
cdlemn11a.f F = ι h T | h P = Q
cdlemn11a.g G = ι h T | h P = N
Assertion cdlemn11c K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X y J Q z I X G I T = y + ˙ z

Proof

Step Hyp Ref Expression
1 cdlemn11a.b B = Base K
2 cdlemn11a.l ˙ = K
3 cdlemn11a.j ˙ = join K
4 cdlemn11a.a A = Atoms K
5 cdlemn11a.h H = LHyp K
6 cdlemn11a.p P = oc K W
7 cdlemn11a.o O = h T I B
8 cdlemn11a.t T = LTrn K W
9 cdlemn11a.r R = trL K W
10 cdlemn11a.e E = TEndo K W
11 cdlemn11a.i I = DIsoB K W
12 cdlemn11a.J J = DIsoC K W
13 cdlemn11a.u U = DVecH K W
14 cdlemn11a.d + ˙ = + U
15 cdlemn11a.s ˙ = LSSum U
16 cdlemn11a.f F = ι h T | h P = Q
17 cdlemn11a.g G = ι h T | h P = N
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 cdlemn11b K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X G I T J Q ˙ I X
19 simp1 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X K HL W H
20 5 13 19 dvhlmod K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X U LMod
21 eqid LSubSp U = LSubSp U
22 21 lsssssubg U LMod LSubSp U SubGrp U
23 20 22 syl K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X LSubSp U SubGrp U
24 simp21 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X Q A ¬ Q ˙ W
25 2 4 5 13 12 21 diclss K HL W H Q A ¬ Q ˙ W J Q LSubSp U
26 19 24 25 syl2anc K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X J Q LSubSp U
27 23 26 sseldd K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X J Q SubGrp U
28 simp23l K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X X B
29 simp23r K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X X ˙ W
30 1 2 5 13 11 21 diblss K HL W H X B X ˙ W I X LSubSp U
31 19 28 29 30 syl12anc K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X I X LSubSp U
32 23 31 sseldd K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X I X SubGrp U
33 14 15 lsmelval J Q SubGrp U I X SubGrp U G I T J Q ˙ I X y J Q z I X G I T = y + ˙ z
34 27 32 33 syl2anc K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X G I T J Q ˙ I X y J Q z I X G I T = y + ˙ z
35 18 34 mpbid K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X y J Q z I X G I T = y + ˙ z