This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdleml5N

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 cdleml5N 
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .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 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) /\ V = .0. ) -> ( K e. HL /\ W e. H ) )
8 1 2 3 5 6 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> .0. e. E )
9 7 8 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) /\ V = .0. ) -> .0. e. E )
10 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) /\ V = .0. ) -> U e. E )
11 1 2 3 5 6 tendo0mul 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E ) -> ( .0. o. U ) = .0. )
12 7 10 11 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) /\ V = .0. ) -> ( .0. o. U ) = .0. )
13 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) /\ V = .0. ) -> V = .0. )
14 12 13 eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) /\ V = .0. ) -> ( .0. o. U ) = V )
15 coeq1 
 |-  ( s = .0. -> ( s o. U ) = ( .0. o. U ) )
16 15 eqeq1d 
 |-  ( s = .0. -> ( ( s o. U ) = V <-> ( .0. o. U ) = V ) )
17 16 rspcev 
 |-  ( ( .0. e. E /\ ( .0. o. U ) = V ) -> E. s e. E ( s o. U ) = V )
18 9 14 17 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) /\ V = .0. ) -> E. s e. E ( s o. U ) = V )
19 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) /\ V =/= .0. ) -> ( K e. HL /\ W e. H ) )
20 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) /\ V =/= .0. ) -> ( U e. E /\ V e. E ) )
21 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) /\ V =/= .0. ) -> U =/= .0. )
22 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) /\ V =/= .0. ) -> V =/= .0. )
23 1 2 3 4 5 6 cdleml4N 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( U =/= .0. /\ V =/= .0. ) ) -> E. s e. E ( s o. U ) = V )
24 19 20 21 22 23 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) /\ V =/= .0. ) -> E. s e. E ( s o. U ) = V )
25 18 24 pm2.61dane 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ U =/= .0. ) -> E. s e. E ( s o. U ) = V )