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