Theorem cdleml4N

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

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	1 2 3	cdlemftr0	|- ( ( K e. HL /\ W e. H ) -> E. f e. T f =/= ( _I |` B ) )
8	7	3ad2ant1	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( U =/= .0. /\ V =/= .0. ) ) -> E. f e. T f =/= ( _I |` B ) )
9		simp11	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( U =/= .0. /\ V =/= .0. ) ) /\ f e. T /\ f =/= ( _I |` B ) ) -> ( K e. HL /\ W e. H ) )
10		simp12l	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( U =/= .0. /\ V =/= .0. ) ) /\ f e. T /\ f =/= ( _I |` B ) ) -> U e. E )
11		simp12r	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( U =/= .0. /\ V =/= .0. ) ) /\ f e. T /\ f =/= ( _I |` B ) ) -> V e. E )
12		simp2	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( U =/= .0. /\ V =/= .0. ) ) /\ f e. T /\ f =/= ( _I |` B ) ) -> f e. T )
13		simp3	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( U =/= .0. /\ V =/= .0. ) ) /\ f e. T /\ f =/= ( _I |` B ) ) -> f =/= ( _I |` B ) )
14		simp13l	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( U =/= .0. /\ V =/= .0. ) ) /\ f e. T /\ f =/= ( _I |` B ) ) -> U =/= .0. )
15		simp13r	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( U =/= .0. /\ V =/= .0. ) ) /\ f e. T /\ f =/= ( _I |` B ) ) -> V =/= .0. )
16	1 2 3 4 5 6	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 )
17	9 10 11 12 13 14 15 16	syl133anc	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( U =/= .0. /\ V =/= .0. ) ) /\ f e. T /\ f =/= ( _I |` B ) ) -> E. s e. E ( s o. U ) = V )
18	17	rexlimdv3a	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( U =/= .0. /\ V =/= .0. ) ) -> ( E. f e. T f =/= ( _I |` B ) -> E. s e. E ( s o. U ) = V ) )
19	8 18	mpd	|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( U =/= .0. /\ V =/= .0. ) ) -> E. s e. E ( s o. U ) = V )