Metamath Proof Explorer

Theorem mapd0

Description: Projectivity map of the zero subspace. Part of property (f) in Baer p. 40. TODO: does proof need to be this long for this simple fact? (Contributed by NM, 15-Mar-2015)

Ref Expression
Hypotheses mapd0.h 
|- H = ( LHyp ` K )
mapd0.m 
|- M = ( ( mapd ` K ) ` W )
mapd0.u 
|- U = ( ( DVecH ` K ) ` W )
mapd0.o 
|- O = ( 0g ` U )
mapd0.c 
|- C = ( ( LCDual ` K ) ` W )
mapd0.z 
|- .0. = ( 0g ` C )
mapd0.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion mapd0 
|- ( ph -> ( M ` { O } ) = { .0. } )

Proof

Step Hyp Ref Expression
1 mapd0.h 
 |-  H = ( LHyp ` K )
2 mapd0.m 
 |-  M = ( ( mapd ` K ) ` W )
3 mapd0.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 mapd0.o 
 |-  O = ( 0g ` U )
5 mapd0.c 
 |-  C = ( ( LCDual ` K ) ` W )
6 mapd0.z 
 |-  .0. = ( 0g ` C )
7 mapd0.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
9 eqid 
 |-  ( LFnl ` U ) = ( LFnl ` U )
10 eqid 
 |-  ( LKer ` U ) = ( LKer ` U )
11 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
12 1 3 7 dvhlmod 
 |-  ( ph -> U e. LMod )
13 4 8 lsssn0 
 |-  ( U e. LMod -> { O } e. ( LSubSp ` U ) )
14 12 13 syl 
 |-  ( ph -> { O } e. ( LSubSp ` U ) )
15 1 3 8 9 10 11 2 7 14 mapdval 
 |-  ( ph -> ( M ` { O } ) = { f e. ( LFnl ` U ) | ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) C_ { O } ) } )
16 simprrr 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } )
17 12 adantr 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> U e. LMod )
18 7 adantr 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> ( K e. HL /\ W e. H ) )
19 eqid 
 |-  ( Base ` U ) = ( Base ` U )
20 simprl 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> g e. ( LFnl ` U ) )
21 19 9 10 17 20 lkrssv 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> ( ( LKer ` U ) ` g ) C_ ( Base ` U ) )
22 1 3 19 8 11 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( LKer ` U ) ` g ) C_ ( Base ` U ) ) -> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) e. ( LSubSp ` U ) )
23 18 21 22 syl2anc 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) e. ( LSubSp ` U ) )
24 4 8 lssle0 
 |-  ( ( U e. LMod /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) e. ( LSubSp ` U ) ) -> ( ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } <-> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) = { O } ) )
25 17 23 24 syl2anc 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> ( ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } <-> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) = { O } ) )
26 16 25 mpbid 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) = { O } )
27 26 fveq2d 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( ( ocH ` K ) ` W ) ` { O } ) )
28 simprrl 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) )
29 1 3 11 19 4 doch0 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( ocH ` K ) ` W ) ` { O } ) = ( Base ` U ) )
30 7 29 syl 
 |-  ( ph -> ( ( ( ocH ` K ) ` W ) ` { O } ) = ( Base ` U ) )
31 30 adantr 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> ( ( ( ocH ` K ) ` W ) ` { O } ) = ( Base ` U ) )
32 27 28 31 3eqtr3d 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> ( ( LKer ` U ) ` g ) = ( Base ` U ) )
33 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
34 eqid 
 |-  ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) )
35 33 34 19 9 10 lkr0f 
 |-  ( ( U e. LMod /\ g e. ( LFnl ` U ) ) -> ( ( ( LKer ` U ) ` g ) = ( Base ` U ) <-> g = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) )
36 17 20 35 syl2anc 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> ( ( ( LKer ` U ) ` g ) = ( Base ` U ) <-> g = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) )
37 32 36 mpbid 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> g = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) )
38 1 3 19 33 34 5 6 7 lcd0v 
 |-  ( ph -> .0. = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) )
39 38 adantr 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> .0. = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) )
40 37 39 eqtr4d 
 |-  ( ( ph /\ ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) -> g = .0. )
41 40 ex 
 |-  ( ph -> ( ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) -> g = .0. ) )
42 eqid 
 |-  ( Base ` C ) = ( Base ` C )
43 1 5 42 6 7 lcd0vcl 
 |-  ( ph -> .0. e. ( Base ` C ) )
44 1 5 42 3 9 7 43 lcdvbaselfl 
 |-  ( ph -> .0. e. ( LFnl ` U ) )
45 33 34 19 9 10 lkr0f 
 |-  ( ( U e. LMod /\ .0. e. ( LFnl ` U ) ) -> ( ( ( LKer ` U ) ` .0. ) = ( Base ` U ) <-> .0. = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) )
46 12 44 45 syl2anc 
 |-  ( ph -> ( ( ( LKer ` U ) ` .0. ) = ( Base ` U ) <-> .0. = ( ( Base ` U ) X. { ( 0g ` ( Scalar ` U ) ) } ) ) )
47 38 46 mpbird 
 |-  ( ph -> ( ( LKer ` U ) ` .0. ) = ( Base ` U ) )
48 47 fveq2d 
 |-  ( ph -> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) = ( ( ( ocH ` K ) ` W ) ` ( Base ` U ) ) )
49 48 fveq2d 
 |-  ( ph -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( Base ` U ) ) ) )
50 1 3 11 19 7 dochoc1 
 |-  ( ph -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( Base ` U ) ) ) = ( Base ` U ) )
51 49 50 eqtrd 
 |-  ( ph -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) ) = ( Base ` U ) )
52 51 47 eqtr4d 
 |-  ( ph -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) ) = ( ( LKer ` U ) ` .0. ) )
53 1 3 11 19 4 doch1 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( ocH ` K ) ` W ) ` ( Base ` U ) ) = { O } )
54 7 53 syl 
 |-  ( ph -> ( ( ( ocH ` K ) ` W ) ` ( Base ` U ) ) = { O } )
55 48 54 eqtrd 
 |-  ( ph -> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) = { O } )
56 eqimss 
 |-  ( ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) = { O } -> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) C_ { O } )
57 55 56 syl 
 |-  ( ph -> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) C_ { O } )
58 44 52 57 jca32 
 |-  ( ph -> ( .0. e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) ) = ( ( LKer ` U ) ` .0. ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) C_ { O } ) ) )
59 eleq1 
 |-  ( g = .0. -> ( g e. ( LFnl ` U ) <-> .0. e. ( LFnl ` U ) ) )
60 2fveq3 
 |-  ( g = .0. -> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) )
61 60 fveq2d 
 |-  ( g = .0. -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) ) )
62 fveq2 
 |-  ( g = .0. -> ( ( LKer ` U ) ` g ) = ( ( LKer ` U ) ` .0. ) )
63 61 62 eqeq12d 
 |-  ( g = .0. -> ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) <-> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) ) = ( ( LKer ` U ) ` .0. ) ) )
64 60 sseq1d 
 |-  ( g = .0. -> ( ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } <-> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) C_ { O } ) )
65 63 64 anbi12d 
 |-  ( g = .0. -> ( ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) <-> ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) ) = ( ( LKer ` U ) ` .0. ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) C_ { O } ) ) )
66 59 65 anbi12d 
 |-  ( g = .0. -> ( ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) <-> ( .0. e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) ) = ( ( LKer ` U ) ` .0. ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` .0. ) ) C_ { O } ) ) ) )
67 58 66 syl5ibrcom 
 |-  ( ph -> ( g = .0. -> ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) ) )
68 41 67 impbid 
 |-  ( ph -> ( ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) <-> g = .0. ) )
69 2fveq3 
 |-  ( f = g -> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) )
70 69 fveq2d 
 |-  ( f = g -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) )
71 fveq2 
 |-  ( f = g -> ( ( LKer ` U ) ` f ) = ( ( LKer ` U ) ` g ) )
72 70 71 eqeq12d 
 |-  ( f = g -> ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) <-> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) ) )
73 69 sseq1d 
 |-  ( f = g -> ( ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) C_ { O } <-> ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) )
74 72 73 anbi12d 
 |-  ( f = g -> ( ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) C_ { O } ) <-> ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) )
75 74 elrab 
 |-  ( g e. { f e. ( LFnl ` U ) | ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) C_ { O } ) } <-> ( g e. ( LFnl ` U ) /\ ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) ) = ( ( LKer ` U ) ` g ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` g ) ) C_ { O } ) ) )
76 velsn 
 |-  ( g e. { .0. } <-> g = .0. )
77 68 75 76 3bitr4g 
 |-  ( ph -> ( g e. { f e. ( LFnl ` U ) | ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) C_ { O } ) } <-> g e. { .0. } ) )
78 77 eqrdv 
 |-  ( ph -> { f e. ( LFnl ` U ) | ( ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) ) = ( ( LKer ` U ) ` f ) /\ ( ( ( ocH ` K ) ` W ) ` ( ( LKer ` U ) ` f ) ) C_ { O } ) } = { .0. } )
79 15 78 eqtrd 
 |-  ( ph -> ( M ` { O } ) = { .0. } )