Theorem diatrl

Description: Trace of a member of the partial isomorphism A. (Contributed by NM, 17-Jan-2014)

	Ref	Expression
Hypotheses	diatrl.b	|- B = ( Base ` K )
	diatrl.l	|- .<_ = ( le ` K )
	diatrl.h	|- H = ( LHyp ` K )
	diatrl.t	|- T = ( ( LTrn ` K ) ` W )
	diatrl.r	|- R = ( ( trL ` K ) ` W )
	diatrl.i	|- I = ( ( DIsoA ` K ) ` W )
Assertion	diatrl	|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ F e. ( I ` X ) ) -> ( R ` F ) .<_ X )

Proof

Step	Hyp	Ref	Expression
1		diatrl.b	|- B = ( Base ` K )
2		diatrl.l	|- .<_ = ( le ` K )
3		diatrl.h	|- H = ( LHyp ` K )
4		diatrl.t	|- T = ( ( LTrn ` K ) ` W )
5		diatrl.r	|- R = ( ( trL ` K ) ` W )
6		diatrl.i	|- I = ( ( DIsoA ` K ) ` W )
7	1 2 3 4 5 6	diaelval	|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( F e. ( I ` X ) <-> ( F e. T /\ ( R ` F ) .<_ X ) ) )
8		simpr	|- ( ( F e. T /\ ( R ` F ) .<_ X ) -> ( R ` F ) .<_ X )
9	7 8	syl6bi	|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( F e. ( I ` X ) -> ( R ` F ) .<_ X ) )
10	9	3impia	|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ F e. ( I ` X ) ) -> ( R ` F ) .<_ X )