Step |
Hyp |
Ref |
Expression |
1 |
|
dihp.b |
|- B = ( Base ` K ) |
2 |
|
dihp.h |
|- H = ( LHyp ` K ) |
3 |
|
dihp.p |
|- P = ( ( oc ` K ) ` W ) |
4 |
|
dihp.t |
|- T = ( ( LTrn ` K ) ` W ) |
5 |
|
dihp.e |
|- E = ( ( TEndo ` K ) ` W ) |
6 |
|
dihp.o |
|- O = ( f e. T |-> ( _I |` B ) ) |
7 |
|
dihp.i |
|- I = ( ( DIsoH ` K ) ` W ) |
8 |
|
dihp.u |
|- U = ( ( DVecH ` K ) ` W ) |
9 |
|
dihp.n |
|- N = ( LSpan ` U ) |
10 |
|
dihp.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
11 |
|
dihp.s |
|- ( ph -> ( S e. E /\ S =/= O ) ) |
12 |
|
eqid |
|- ( 0g ` U ) = ( 0g ` U ) |
13 |
|
eqid |
|- ( LSAtoms ` U ) = ( LSAtoms ` U ) |
14 |
2 8 10
|
dvhlvec |
|- ( ph -> U e. LVec ) |
15 |
2 3 7 8 13 10
|
dihat |
|- ( ph -> ( I ` P ) e. ( LSAtoms ` U ) ) |
16 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
17 |
|
eqid |
|- ( Atoms ` K ) = ( Atoms ` K ) |
18 |
16 17 2 3
|
lhpocnel2 |
|- ( ( K e. HL /\ W e. H ) -> ( P e. ( Atoms ` K ) /\ -. P ( le ` K ) W ) ) |
19 |
|
eqid |
|- ( iota_ f e. T ( f ` P ) = P ) = ( iota_ f e. T ( f ` P ) = P ) |
20 |
1 16 17 2 4 19
|
ltrniotaidvalN |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. ( Atoms ` K ) /\ -. P ( le ` K ) W ) ) -> ( iota_ f e. T ( f ` P ) = P ) = ( _I |` B ) ) |
21 |
10 18 20
|
syl2anc2 |
|- ( ph -> ( iota_ f e. T ( f ` P ) = P ) = ( _I |` B ) ) |
22 |
21
|
fveq2d |
|- ( ph -> ( S ` ( iota_ f e. T ( f ` P ) = P ) ) = ( S ` ( _I |` B ) ) ) |
23 |
11
|
simpld |
|- ( ph -> S e. E ) |
24 |
1 2 5
|
tendoid |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( S ` ( _I |` B ) ) = ( _I |` B ) ) |
25 |
10 23 24
|
syl2anc |
|- ( ph -> ( S ` ( _I |` B ) ) = ( _I |` B ) ) |
26 |
22 25
|
eqtr2d |
|- ( ph -> ( _I |` B ) = ( S ` ( iota_ f e. T ( f ` P ) = P ) ) ) |
27 |
1
|
fvexi |
|- B e. _V |
28 |
|
resiexg |
|- ( B e. _V -> ( _I |` B ) e. _V ) |
29 |
27 28
|
mp1i |
|- ( ph -> ( _I |` B ) e. _V ) |
30 |
|
eqeq1 |
|- ( g = ( _I |` B ) -> ( g = ( s ` ( iota_ f e. T ( f ` P ) = P ) ) <-> ( _I |` B ) = ( s ` ( iota_ f e. T ( f ` P ) = P ) ) ) ) |
31 |
30
|
anbi1d |
|- ( g = ( _I |` B ) -> ( ( g = ( s ` ( iota_ f e. T ( f ` P ) = P ) ) /\ s e. E ) <-> ( ( _I |` B ) = ( s ` ( iota_ f e. T ( f ` P ) = P ) ) /\ s e. E ) ) ) |
32 |
|
fveq1 |
|- ( s = S -> ( s ` ( iota_ f e. T ( f ` P ) = P ) ) = ( S ` ( iota_ f e. T ( f ` P ) = P ) ) ) |
33 |
32
|
eqeq2d |
|- ( s = S -> ( ( _I |` B ) = ( s ` ( iota_ f e. T ( f ` P ) = P ) ) <-> ( _I |` B ) = ( S ` ( iota_ f e. T ( f ` P ) = P ) ) ) ) |
34 |
|
eleq1 |
|- ( s = S -> ( s e. E <-> S e. E ) ) |
35 |
33 34
|
anbi12d |
|- ( s = S -> ( ( ( _I |` B ) = ( s ` ( iota_ f e. T ( f ` P ) = P ) ) /\ s e. E ) <-> ( ( _I |` B ) = ( S ` ( iota_ f e. T ( f ` P ) = P ) ) /\ S e. E ) ) ) |
36 |
31 35
|
opelopabg |
|- ( ( ( _I |` B ) e. _V /\ S e. E ) -> ( <. ( _I |` B ) , S >. e. { <. g , s >. | ( g = ( s ` ( iota_ f e. T ( f ` P ) = P ) ) /\ s e. E ) } <-> ( ( _I |` B ) = ( S ` ( iota_ f e. T ( f ` P ) = P ) ) /\ S e. E ) ) ) |
37 |
29 23 36
|
syl2anc |
|- ( ph -> ( <. ( _I |` B ) , S >. e. { <. g , s >. | ( g = ( s ` ( iota_ f e. T ( f ` P ) = P ) ) /\ s e. E ) } <-> ( ( _I |` B ) = ( S ` ( iota_ f e. T ( f ` P ) = P ) ) /\ S e. E ) ) ) |
38 |
26 23 37
|
mpbir2and |
|- ( ph -> <. ( _I |` B ) , S >. e. { <. g , s >. | ( g = ( s ` ( iota_ f e. T ( f ` P ) = P ) ) /\ s e. E ) } ) |
39 |
|
eqid |
|- ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W ) |
40 |
16 17 2 39 7
|
dihvalcqat |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. ( Atoms ` K ) /\ -. P ( le ` K ) W ) ) -> ( I ` P ) = ( ( ( DIsoC ` K ) ` W ) ` P ) ) |
41 |
10 18 40
|
syl2anc2 |
|- ( ph -> ( I ` P ) = ( ( ( DIsoC ` K ) ` W ) ` P ) ) |
42 |
16 17 2 3 4 5 39
|
dicval |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. ( Atoms ` K ) /\ -. P ( le ` K ) W ) ) -> ( ( ( DIsoC ` K ) ` W ) ` P ) = { <. g , s >. | ( g = ( s ` ( iota_ f e. T ( f ` P ) = P ) ) /\ s e. E ) } ) |
43 |
10 18 42
|
syl2anc2 |
|- ( ph -> ( ( ( DIsoC ` K ) ` W ) ` P ) = { <. g , s >. | ( g = ( s ` ( iota_ f e. T ( f ` P ) = P ) ) /\ s e. E ) } ) |
44 |
41 43
|
eqtr2d |
|- ( ph -> { <. g , s >. | ( g = ( s ` ( iota_ f e. T ( f ` P ) = P ) ) /\ s e. E ) } = ( I ` P ) ) |
45 |
38 44
|
eleqtrd |
|- ( ph -> <. ( _I |` B ) , S >. e. ( I ` P ) ) |
46 |
11
|
simprd |
|- ( ph -> S =/= O ) |
47 |
1 2 4 8 12 6
|
dvh0g |
|- ( ( K e. HL /\ W e. H ) -> ( 0g ` U ) = <. ( _I |` B ) , O >. ) |
48 |
10 47
|
syl |
|- ( ph -> ( 0g ` U ) = <. ( _I |` B ) , O >. ) |
49 |
48
|
eqeq2d |
|- ( ph -> ( <. ( _I |` B ) , S >. = ( 0g ` U ) <-> <. ( _I |` B ) , S >. = <. ( _I |` B ) , O >. ) ) |
50 |
27 28
|
ax-mp |
|- ( _I |` B ) e. _V |
51 |
4
|
fvexi |
|- T e. _V |
52 |
51
|
mptex |
|- ( f e. T |-> ( _I |` B ) ) e. _V |
53 |
6 52
|
eqeltri |
|- O e. _V |
54 |
50 53
|
opth2 |
|- ( <. ( _I |` B ) , S >. = <. ( _I |` B ) , O >. <-> ( ( _I |` B ) = ( _I |` B ) /\ S = O ) ) |
55 |
54
|
simprbi |
|- ( <. ( _I |` B ) , S >. = <. ( _I |` B ) , O >. -> S = O ) |
56 |
49 55
|
syl6bi |
|- ( ph -> ( <. ( _I |` B ) , S >. = ( 0g ` U ) -> S = O ) ) |
57 |
56
|
necon3d |
|- ( ph -> ( S =/= O -> <. ( _I |` B ) , S >. =/= ( 0g ` U ) ) ) |
58 |
46 57
|
mpd |
|- ( ph -> <. ( _I |` B ) , S >. =/= ( 0g ` U ) ) |
59 |
12 9 13 14 15 45 58
|
lsatel |
|- ( ph -> ( I ` P ) = ( N ` { <. ( _I |` B ) , S >. } ) ) |