Metamath Proof Explorer


Theorem cdlemn11pre

Description: Part of proof of Lemma N of Crawley p. 121 line 37. TODO: combine cdlemn11a , cdlemn11b , cdlemn11c , cdlemn11pre into one? (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 cdlemn11pre K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X N ˙ Q ˙ X

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 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
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 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
21 2 4 5 6 8 10 12 16 dicelval3 K HL W H Q A ¬ Q ˙ W y J Q s E y = s F s
22 19 20 21 syl2anc 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 s E y = s F s
23 simp23 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X X B X ˙ W
24 1 2 5 8 9 7 11 dibelval3 K HL W H X B X ˙ W z I X g T z = g O R g ˙ X
25 19 23 24 syl2anc K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X z I X g T z = g O R g ˙ X
26 22 25 anbi12d 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 s E y = s F s g T z = g O R g ˙ X
27 reeanv s E g T y = s F s z = g O R g ˙ X s E y = s F s g T z = g O R g ˙ X
28 simpl1 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T R g ˙ X G I T = s F s + ˙ g O K HL W H
29 simpl21 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T R g ˙ X G I T = s F s + ˙ g O Q A ¬ Q ˙ W
30 simpl22 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T R g ˙ X G I T = s F s + ˙ g O N A ¬ N ˙ W
31 simpl23 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T R g ˙ X G I T = s F s + ˙ g O X B X ˙ W
32 simpr1r K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T R g ˙ X G I T = s F s + ˙ g O g T
33 simpr1l K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T R g ˙ X G I T = s F s + ˙ g O s E
34 simpr3 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T R g ˙ X G I T = s F s + ˙ g O G I T = s F s + ˙ g O
35 1 2 4 5 6 7 8 10 13 14 16 17 cdlemn9 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W s E g T G I T = s F s + ˙ g O g Q = N
36 28 29 30 33 32 34 35 syl123anc K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T R g ˙ X G I T = s F s + ˙ g O g Q = N
37 simpr2 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T R g ˙ X G I T = s F s + ˙ g O R g ˙ X
38 1 2 3 4 5 8 9 cdlemn10 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W g T g Q = N R g ˙ X N ˙ Q ˙ X
39 28 29 30 31 32 36 37 38 syl133anc K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T R g ˙ X G I T = s F s + ˙ g O N ˙ Q ˙ X
40 39 3exp2 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T R g ˙ X G I T = s F s + ˙ g O N ˙ Q ˙ X
41 oveq12 y = s F s z = g O y + ˙ z = s F s + ˙ g O
42 41 eqeq2d y = s F s z = g O G I T = y + ˙ z G I T = s F s + ˙ g O
43 42 imbi1d y = s F s z = g O G I T = y + ˙ z N ˙ Q ˙ X G I T = s F s + ˙ g O N ˙ Q ˙ X
44 43 imbi2d y = s F s z = g O R g ˙ X G I T = y + ˙ z N ˙ Q ˙ X R g ˙ X G I T = s F s + ˙ g O N ˙ Q ˙ X
45 44 biimprd y = s F s z = g O R g ˙ X G I T = s F s + ˙ g O N ˙ Q ˙ X R g ˙ X G I T = y + ˙ z N ˙ Q ˙ X
46 45 com23 y = s F s z = g O R g ˙ X R g ˙ X G I T = s F s + ˙ g O N ˙ Q ˙ X G I T = y + ˙ z N ˙ Q ˙ X
47 46 impr y = s F s z = g O R g ˙ X R g ˙ X G I T = s F s + ˙ g O N ˙ Q ˙ X G I T = y + ˙ z N ˙ Q ˙ X
48 47 com12 R g ˙ X G I T = s F s + ˙ g O N ˙ Q ˙ X y = s F s z = g O R g ˙ X G I T = y + ˙ z N ˙ Q ˙ X
49 40 48 syl6 K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T y = s F s z = g O R g ˙ X G I T = y + ˙ z N ˙ Q ˙ X
50 49 rexlimdvv K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E g T y = s F s z = g O R g ˙ X G I T = y + ˙ z N ˙ Q ˙ X
51 27 50 syl5bir K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X s E y = s F s g T z = g O R g ˙ X G I T = y + ˙ z N ˙ Q ˙ X
52 26 51 sylbid 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 N ˙ Q ˙ X
53 52 rexlimdvv 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 N ˙ Q ˙ X
54 18 53 mpd K HL W H Q A ¬ Q ˙ W N A ¬ N ˙ W X B X ˙ W J N J Q ˙ I X N ˙ Q ˙ X