Metamath Proof Explorer


Theorem dih1dimatlem0

Description: Lemma for dih1dimat . (Contributed by NM, 11-Apr-2014)

Ref Expression
Hypotheses dih1dimat.h H = LHyp K
dih1dimat.u U = DVecH K W
dih1dimat.i I = DIsoH K W
dih1dimat.a A = LSAtoms U
dih1dimat.b B = Base K
dih1dimat.l ˙ = K
dih1dimat.c C = Atoms K
dih1dimat.p P = oc K W
dih1dimat.t T = LTrn K W
dih1dimat.r R = trL K W
dih1dimat.e E = TEndo K W
dih1dimat.o O = h T I B
dih1dimat.d F = Scalar U
dih1dimat.j J = inv r F
dih1dimat.v V = Base U
dih1dimat.m · ˙ = U
dih1dimat.s S = LSubSp U
dih1dimat.n N = LSpan U
dih1dimat.z 0 ˙ = 0 U
dih1dimat.g G = ι h T | h P = J s f P
Assertion dih1dimatlem0 K HL W H f T s E s O i = p G p E i T p E t E i = t f p = t s

Proof

Step Hyp Ref Expression
1 dih1dimat.h H = LHyp K
2 dih1dimat.u U = DVecH K W
3 dih1dimat.i I = DIsoH K W
4 dih1dimat.a A = LSAtoms U
5 dih1dimat.b B = Base K
6 dih1dimat.l ˙ = K
7 dih1dimat.c C = Atoms K
8 dih1dimat.p P = oc K W
9 dih1dimat.t T = LTrn K W
10 dih1dimat.r R = trL K W
11 dih1dimat.e E = TEndo K W
12 dih1dimat.o O = h T I B
13 dih1dimat.d F = Scalar U
14 dih1dimat.j J = inv r F
15 dih1dimat.v V = Base U
16 dih1dimat.m · ˙ = U
17 dih1dimat.s S = LSubSp U
18 dih1dimat.n N = LSpan U
19 dih1dimat.z 0 ˙ = 0 U
20 dih1dimat.g G = ι h T | h P = J s f P
21 simprl K HL W H f T s E s O i = p G p E i = p G
22 simpl1 K HL W H f T s E s O i = p G p E K HL W H
23 simprr K HL W H f T s E s O i = p G p E p E
24 6 7 1 8 lhpocnel2 K HL W H P C ¬ P ˙ W
25 22 24 syl K HL W H f T s E s O i = p G p E P C ¬ P ˙ W
26 simpl2r K HL W H f T s E s O i = p G p E s E
27 simpl3 K HL W H f T s E s O i = p G p E s O
28 5 1 9 11 12 2 13 14 tendoinvcl K HL W H s E s O J s E J s O
29 28 simpld K HL W H s E s O J s E
30 22 26 27 29 syl3anc K HL W H f T s E s O i = p G p E J s E
31 simpl2l K HL W H f T s E s O i = p G p E f T
32 1 9 11 tendocl K HL W H J s E f T J s f T
33 22 30 31 32 syl3anc K HL W H f T s E s O i = p G p E J s f T
34 6 7 1 9 ltrnel K HL W H J s f T P C ¬ P ˙ W J s f P C ¬ J s f P ˙ W
35 22 33 25 34 syl3anc K HL W H f T s E s O i = p G p E J s f P C ¬ J s f P ˙ W
36 6 7 1 9 20 ltrniotacl K HL W H P C ¬ P ˙ W J s f P C ¬ J s f P ˙ W G T
37 22 25 35 36 syl3anc K HL W H f T s E s O i = p G p E G T
38 1 9 11 tendocl K HL W H p E G T p G T
39 22 23 37 38 syl3anc K HL W H f T s E s O i = p G p E p G T
40 21 39 eqeltrd K HL W H f T s E s O i = p G p E i T
41 1 11 tendococl K HL W H p E J s E p J s E
42 22 23 30 41 syl3anc K HL W H f T s E s O i = p G p E p J s E
43 simp1 K HL W H f T s E s O K HL W H
44 24 3ad2ant1 K HL W H f T s E s O P C ¬ P ˙ W
45 29 3adant2l K HL W H f T s E s O J s E
46 simp2l K HL W H f T s E s O f T
47 43 45 46 32 syl3anc K HL W H f T s E s O J s f T
48 43 47 44 34 syl3anc K HL W H f T s E s O J s f P C ¬ J s f P ˙ W
49 43 44 48 36 syl3anc K HL W H f T s E s O G T
50 6 7 1 9 20 ltrniotaval K HL W H P C ¬ P ˙ W J s f P C ¬ J s f P ˙ W G P = J s f P
51 43 44 48 50 syl3anc K HL W H f T s E s O G P = J s f P
52 6 7 1 9 cdlemd K HL W H G T J s f T P C ¬ P ˙ W G P = J s f P G = J s f
53 43 49 47 44 51 52 syl311anc K HL W H f T s E s O G = J s f
54 53 adantr K HL W H f T s E s O i = p G p E G = J s f
55 54 fveq2d K HL W H f T s E s O i = p G p E p G = p J s f
56 1 9 11 tendocoval K HL W H p E J s E f T p J s f = p J s f
57 22 23 30 31 56 syl121anc K HL W H f T s E s O i = p G p E p J s f = p J s f
58 55 21 57 3eqtr4d K HL W H f T s E s O i = p G p E i = p J s f
59 coass p J s s = p J s s
60 5 1 9 11 12 2 13 14 tendolinv K HL W H s E s O J s s = I T
61 22 26 27 60 syl3anc K HL W H f T s E s O i = p G p E J s s = I T
62 61 coeq2d K HL W H f T s E s O i = p G p E p J s s = p I T
63 1 9 11 tendo1mulr K HL W H p E p I T = p
64 22 23 63 syl2anc K HL W H f T s E s O i = p G p E p I T = p
65 62 64 eqtrd K HL W H f T s E s O i = p G p E p J s s = p
66 59 65 eqtr2id K HL W H f T s E s O i = p G p E p = p J s s
67 fveq1 t = p J s t f = p J s f
68 67 eqeq2d t = p J s i = t f i = p J s f
69 coeq1 t = p J s t s = p J s s
70 69 eqeq2d t = p J s p = t s p = p J s s
71 68 70 anbi12d t = p J s i = t f p = t s i = p J s f p = p J s s
72 71 rspcev p J s E i = p J s f p = p J s s t E i = t f p = t s
73 42 58 66 72 syl12anc K HL W H f T s E s O i = p G p E t E i = t f p = t s
74 40 23 73 jca31 K HL W H f T s E s O i = p G p E i T p E t E i = t f p = t s
75 simp3r K HL W H f T s E s O i T p E t E i = t f p = t s p = t s
76 75 fveq1d K HL W H f T s E s O i T p E t E i = t f p = t s p J s f = t s J s f
77 simp1l1 K HL W H f T s E s O i T p E t E i = t f p = t s K HL W H
78 simp2 K HL W H f T s E s O i T p E t E i = t f p = t s t E
79 simpl2r K HL W H f T s E s O i T p E s E
80 79 3ad2ant1 K HL W H f T s E s O i T p E t E i = t f p = t s s E
81 1 11 tendococl K HL W H t E s E t s E
82 77 78 80 81 syl3anc K HL W H f T s E s O i T p E t E i = t f p = t s t s E
83 simp1l3 K HL W H f T s E s O i T p E t E i = t f p = t s s O
84 77 80 83 29 syl3anc K HL W H f T s E s O i T p E t E i = t f p = t s J s E
85 simpl2l K HL W H f T s E s O i T p E f T
86 85 3ad2ant1 K HL W H f T s E s O i T p E t E i = t f p = t s f T
87 1 9 11 tendocoval K HL W H t s E J s E f T t s J s f = t s J s f
88 77 82 84 86 87 syl121anc K HL W H f T s E s O i T p E t E i = t f p = t s t s J s f = t s J s f
89 coass t s J s = t s J s
90 5 1 9 11 12 2 13 14 tendorinv K HL W H s E s O s J s = I T
91 77 80 83 90 syl3anc K HL W H f T s E s O i T p E t E i = t f p = t s s J s = I T
92 91 coeq2d K HL W H f T s E s O i T p E t E i = t f p = t s t s J s = t I T
93 1 9 11 tendo1mulr K HL W H t E t I T = t
94 77 78 93 syl2anc K HL W H f T s E s O i T p E t E i = t f p = t s t I T = t
95 92 94 eqtrd K HL W H f T s E s O i T p E t E i = t f p = t s t s J s = t
96 89 95 syl5eq K HL W H f T s E s O i T p E t E i = t f p = t s t s J s = t
97 96 fveq1d K HL W H f T s E s O i T p E t E i = t f p = t s t s J s f = t f
98 76 88 97 3eqtr2rd K HL W H f T s E s O i T p E t E i = t f p = t s t f = p J s f
99 simp3l K HL W H f T s E s O i T p E t E i = t f p = t s i = t f
100 53 adantr K HL W H f T s E s O i T p E G = J s f
101 100 3ad2ant1 K HL W H f T s E s O i T p E t E i = t f p = t s G = J s f
102 101 fveq2d K HL W H f T s E s O i T p E t E i = t f p = t s p G = p J s f
103 98 99 102 3eqtr4d K HL W H f T s E s O i T p E t E i = t f p = t s i = p G
104 103 rexlimdv3a K HL W H f T s E s O i T p E t E i = t f p = t s i = p G
105 104 impr K HL W H f T s E s O i T p E t E i = t f p = t s i = p G
106 simprlr K HL W H f T s E s O i T p E t E i = t f p = t s p E
107 105 106 jca K HL W H f T s E s O i T p E t E i = t f p = t s i = p G p E
108 74 107 impbida K HL W H f T s E s O i = p G p E i T p E t E i = t f p = t s