Metamath Proof Explorer


Theorem dihpN

Description: The value of isomorphism H at the fiducial atom P is determined by the vector <. 0 , S >. (the zero translation ltrnid and a nonzero member of the endomorphism ring). In particular, S can be replaced with the ring unit ` ( _I |`T ) . (Contributed by NM, 26-Aug-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihp.b
|- B = ( Base ` K )
dihp.h
|- H = ( LHyp ` K )
dihp.p
|- P = ( ( oc ` K ) ` W )
dihp.t
|- T = ( ( LTrn ` K ) ` W )
dihp.e
|- E = ( ( TEndo ` K ) ` W )
dihp.o
|- O = ( f e. T |-> ( _I |` B ) )
dihp.i
|- I = ( ( DIsoH ` K ) ` W )
dihp.u
|- U = ( ( DVecH ` K ) ` W )
dihp.n
|- N = ( LSpan ` U )
dihp.k
|- ( ph -> ( K e. HL /\ W e. H ) )
dihp.s
|- ( ph -> ( S e. E /\ S =/= O ) )
Assertion dihpN
|- ( ph -> ( I ` P ) = ( N ` { <. ( _I |` B ) , S >. } ) )

Proof

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 >. } ) )