Metamath Proof Explorer


Theorem dib1dim

Description: Two expressions for the 1-dimensional subspaces of vector space H. (Contributed by NM, 24-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses dib1dim.b B = Base K
dib1dim.h H = LHyp K
dib1dim.t T = LTrn K W
dib1dim.r R = trL K W
dib1dim.e E = TEndo K W
dib1dim.o O = h T I B
dib1dim.i I = DIsoB K W
Assertion dib1dim K HL W H F T I R F = g T × E | s E g = s F O

Proof

Step Hyp Ref Expression
1 dib1dim.b B = Base K
2 dib1dim.h H = LHyp K
3 dib1dim.t T = LTrn K W
4 dib1dim.r R = trL K W
5 dib1dim.e E = TEndo K W
6 dib1dim.o O = h T I B
7 dib1dim.i I = DIsoB K W
8 simpl K HL W H F T K HL W H
9 1 2 3 4 trlcl K HL W H F T R F B
10 eqid K = K
11 10 2 3 4 trlle K HL W H F T R F K W
12 eqid DIsoA K W = DIsoA K W
13 1 10 2 3 6 12 7 dibval2 K HL W H R F B R F K W I R F = DIsoA K W R F × O
14 8 9 11 13 syl12anc K HL W H F T I R F = DIsoA K W R F × O
15 relxp Rel DIsoA K W R F × O
16 opelxp f t DIsoA K W R F × O f DIsoA K W R F t O
17 2 3 4 5 12 dia1dim K HL W H F T DIsoA K W R F = f | s E f = s F
18 17 abeq2d K HL W H F T f DIsoA K W R F s E f = s F
19 18 anbi1d K HL W H F T f DIsoA K W R F t O s E f = s F t O
20 2 3 5 tendocl K HL W H s E F T s F T
21 20 3expa K HL W H s E F T s F T
22 21 an32s K HL W H F T s E s F T
23 1 2 3 5 6 tendo0cl K HL W H O E
24 23 ad2antrr K HL W H F T s E O E
25 22 24 jca K HL W H F T s E s F T O E
26 eleq1 f = s F f T s F T
27 eleq1 t = O t E O E
28 26 27 bi2anan9 f = s F t = O f T t E s F T O E
29 25 28 syl5ibrcom K HL W H F T s E f = s F t = O f T t E
30 29 rexlimdva K HL W H F T s E f = s F t = O f T t E
31 30 pm4.71rd K HL W H F T s E f = s F t = O f T t E s E f = s F t = O
32 velsn t O t = O
33 32 anbi2i s E f = s F t O s E f = s F t = O
34 r19.41v s E f = s F t = O s E f = s F t = O
35 33 34 bitr4i s E f = s F t O s E f = s F t = O
36 df-3an f T t E s E f = s F t = O f T t E s E f = s F t = O
37 31 35 36 3bitr4g K HL W H F T s E f = s F t O f T t E s E f = s F t = O
38 19 37 bitrd K HL W H F T f DIsoA K W R F t O f T t E s E f = s F t = O
39 16 38 syl5bb K HL W H F T f t DIsoA K W R F × O f T t E s E f = s F t = O
40 15 39 opabbi2dv K HL W H F T DIsoA K W R F × O = f t | f T t E s E f = s F t = O
41 14 40 eqtrd K HL W H F T I R F = f t | f T t E s E f = s F t = O
42 eqeq1 g = f t g = s F O f t = s F O
43 vex f V
44 vex t V
45 43 44 opth f t = s F O f = s F t = O
46 42 45 bitrdi g = f t g = s F O f = s F t = O
47 46 rexbidv g = f t s E g = s F O s E f = s F t = O
48 47 rabxp g T × E | s E g = s F O = f t | f T t E s E f = s F t = O
49 41 48 eqtr4di K HL W H F T I R F = g T × E | s E g = s F O