Metamath Proof Explorer

Theorem cdleml3N

Description: Part of proof of Lemma L of Crawley p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdleml1.b 
|- B = ( Base ` K )
cdleml1.h 
|- H = ( LHyp ` K )
cdleml1.t 
|- T = ( ( LTrn ` K ) ` W )
cdleml1.r 
|- R = ( ( trL ` K ) ` W )
cdleml1.e 
|- E = ( ( TEndo ` K ) ` W )
cdleml3.o 
|- .0. = ( g e. T |-> ( _I |` B ) )
Assertion cdleml3N 
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> E. s e. E ( s o. U ) = V )

Proof

Step Hyp Ref Expression
1 cdleml1.b 
 |-  B = ( Base ` K )
2 cdleml1.h 
 |-  H = ( LHyp ` K )
3 cdleml1.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 cdleml1.r 
 |-  R = ( ( trL ` K ) ` W )
5 cdleml1.e 
 |-  E = ( ( TEndo ` K ) ` W )
6 cdleml3.o 
 |-  .0. = ( g e. T |-> ( _I |` B ) )
7 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> ( K e. HL /\ W e. H ) )
8 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> ( U e. E /\ V e. E /\ f e. T ) )
9 simp31 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> f =/= ( _I |` B ) )
10 simp32 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> U =/= .0. )
11 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> U e. E )
12 simp23 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> f e. T )
13 1 2 3 5 6 tendoid0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( f e. T /\ f =/= ( _I |` B ) ) ) -> ( ( U ` f ) = ( _I |` B ) <-> U = .0. ) )
14 7 11 12 9 13 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> ( ( U ` f ) = ( _I |` B ) <-> U = .0. ) )
15 14 necon3bid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> ( ( U ` f ) =/= ( _I |` B ) <-> U =/= .0. ) )
16 10 15 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> ( U ` f ) =/= ( _I |` B ) )
17 simp33 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> V =/= .0. )
18 simp22 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> V e. E )
19 1 2 3 5 6 tendoid0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E /\ ( f e. T /\ f =/= ( _I |` B ) ) ) -> ( ( V ` f ) = ( _I |` B ) <-> V = .0. ) )
20 7 18 12 9 19 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> ( ( V ` f ) = ( _I |` B ) <-> V = .0. ) )
21 20 necon3bid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> ( ( V ` f ) =/= ( _I |` B ) <-> V =/= .0. ) )
22 17 21 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> ( V ` f ) =/= ( _I |` B ) )
23 1 2 3 4 5 cdleml2N 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ ( U ` f ) =/= ( _I |` B ) /\ ( V ` f ) =/= ( _I |` B ) ) ) -> E. s e. E ( s ` ( U ` f ) ) = ( V ` f ) )
24 7 8 9 16 22 23 syl113anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> E. s e. E ( s ` ( U ` f ) ) = ( V ` f ) )
25 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E ) -> ( K e. HL /\ W e. H ) )
26 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E ) -> s e. E )
27 simpl21 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E ) -> U e. E )
28 simpl23 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E ) -> f e. T )
29 2 3 5 tendocoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s e. E /\ U e. E ) /\ f e. T ) -> ( ( s o. U ) ` f ) = ( s ` ( U ` f ) ) )
30 25 26 27 28 29 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E ) -> ( ( s o. U ) ` f ) = ( s ` ( U ` f ) ) )
31 30 eqeq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E ) -> ( ( ( s o. U ) ` f ) = ( V ` f ) <-> ( s ` ( U ` f ) ) = ( V ` f ) ) )
32 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E /\ ( ( s o. U ) ` f ) = ( V ` f ) ) -> ( K e. HL /\ W e. H ) )
33 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E /\ ( ( s o. U ) ` f ) = ( V ` f ) ) -> s e. E )
34 simp121 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E /\ ( ( s o. U ) ` f ) = ( V ` f ) ) -> U e. E )
35 2 5 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ U e. E ) -> ( s o. U ) e. E )
36 32 33 34 35 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E /\ ( ( s o. U ) ` f ) = ( V ` f ) ) -> ( s o. U ) e. E )
37 simp122 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E /\ ( ( s o. U ) ` f ) = ( V ` f ) ) -> V e. E )
38 simp3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E /\ ( ( s o. U ) ` f ) = ( V ` f ) ) -> ( ( s o. U ) ` f ) = ( V ` f ) )
39 simp123 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E /\ ( ( s o. U ) ` f ) = ( V ` f ) ) -> f e. T )
40 simp131 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E /\ ( ( s o. U ) ` f ) = ( V ` f ) ) -> f =/= ( _I |` B ) )
41 1 2 3 5 tendocan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( s o. U ) e. E /\ V e. E /\ ( ( s o. U ) ` f ) = ( V ` f ) ) /\ ( f e. T /\ f =/= ( _I |` B ) ) ) -> ( s o. U ) = V )
42 32 36 37 38 39 40 41 syl132anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E /\ ( ( s o. U ) ` f ) = ( V ` f ) ) -> ( s o. U ) = V )
43 42 3expia 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E ) -> ( ( ( s o. U ) ` f ) = ( V ` f ) -> ( s o. U ) = V ) )
44 31 43 sylbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) /\ s e. E ) -> ( ( s ` ( U ` f ) ) = ( V ` f ) -> ( s o. U ) = V ) )
45 44 reximdva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> ( E. s e. E ( s ` ( U ` f ) ) = ( V ` f ) -> E. s e. E ( s o. U ) = V ) )
46 24 45 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ f e. T ) /\ ( f =/= ( _I |` B ) /\ U =/= .0. /\ V =/= .0. ) ) -> E. s e. E ( s o. U ) = V )