Metamath Proof Explorer


Theorem cdlemn6

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

Ref Expression
Hypotheses cdlemn8.b B = Base K
cdlemn8.l ˙ = K
cdlemn8.a A = Atoms K
cdlemn8.h H = LHyp K
cdlemn8.p P = oc K W
cdlemn8.o O = h T I B
cdlemn8.t T = LTrn K W
cdlemn8.e E = TEndo K W
cdlemn8.u U = DVecH K W
cdlemn8.s + ˙ = + U
cdlemn8.f F = ι h T | h P = Q
Assertion cdlemn6 K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T s F s + ˙ g O = s F g s

Proof

Step Hyp Ref Expression
1 cdlemn8.b B = Base K
2 cdlemn8.l ˙ = K
3 cdlemn8.a A = Atoms K
4 cdlemn8.h H = LHyp K
5 cdlemn8.p P = oc K W
6 cdlemn8.o O = h T I B
7 cdlemn8.t T = LTrn K W
8 cdlemn8.e E = TEndo K W
9 cdlemn8.u U = DVecH K W
10 cdlemn8.s + ˙ = + U
11 cdlemn8.f F = ι h T | h P = Q
12 simp1 K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T K HL W H
13 simp3l K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T s E
14 2 3 4 5 lhpocnel2 K HL W H P A ¬ P ˙ W
15 12 14 syl K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T P A ¬ P ˙ W
16 simp2l K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T Q A ¬ Q ˙ W
17 2 3 4 7 11 ltrniotacl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T
18 12 15 16 17 syl3anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T F T
19 4 7 8 tendocl K HL W H s E F T s F T
20 12 13 18 19 syl3anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T s F T
21 simp3r K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T g T
22 1 4 7 8 6 tendo0cl K HL W H O E
23 12 22 syl K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T O E
24 eqid Scalar U = Scalar U
25 eqid + Scalar U = + Scalar U
26 4 7 8 9 24 10 25 dvhopvadd K HL W H s F T s E g T O E s F s + ˙ g O = s F g s + Scalar U O
27 12 20 13 21 23 26 syl122anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T s F s + ˙ g O = s F g s + Scalar U O
28 eqid t E , u E h T t h u h = t E , u E h T t h u h
29 4 7 8 9 24 28 25 dvhfplusr K HL W H + Scalar U = t E , u E h T t h u h
30 12 29 syl K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T + Scalar U = t E , u E h T t h u h
31 30 oveqd K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T s + Scalar U O = s t E , u E h T t h u h O
32 1 4 7 8 6 28 tendo0plr K HL W H s E s t E , u E h T t h u h O = s
33 12 13 32 syl2anc K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T s t E , u E h T t h u h O = s
34 31 33 eqtrd K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T s + Scalar U O = s
35 34 opeq2d K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T s F g s + Scalar U O = s F g s
36 27 35 eqtrd K HL W H Q A ¬ Q ˙ W R A ¬ R ˙ W s E g T s F s + ˙ g O = s F g s