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 )`