Theorem dia1N

Description: The value of the partial isomorphism A at the fiducial co-atom is the set of all translations i.e. the entire vector space. (Contributed by NM, 26-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dia1.h	|- H = ( LHyp ` K )
	dia1.t	|- T = ( ( LTrn ` K ) ` W )
	dia1.i	|- I = ( ( DIsoA ` K ) ` W )
Assertion	dia1N	|- ( ( K e. HL /\ W e. H ) -> ( I ` W ) = T )

Proof

Step	Hyp	Ref	Expression
1		dia1.h	|- H = ( LHyp ` K )
2		dia1.t	|- T = ( ( LTrn ` K ) ` W )
3		dia1.i	|- I = ( ( DIsoA ` K ) ` W )
4		id	|- ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
5		eqid	|- ( Base ` K ) = ( Base ` K )
6	5 1	lhpbase	|- ( W e. H -> W e. ( Base ` K ) )
7	6	adantl	|- ( ( K e. HL /\ W e. H ) -> W e. ( Base ` K ) )
8		hllat	|- ( K e. HL -> K e. Lat )
9		eqid	|- ( le ` K ) = ( le ` K )
10	5 9	latref	|- ( ( K e. Lat /\ W e. ( Base ` K ) ) -> W ( le ` K ) W )
11	8 6 10	syl2an	|- ( ( K e. HL /\ W e. H ) -> W ( le ` K ) W )
12		eqid	|- ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
13	5 9 1 2 12 3	diaval	|- ( ( ( K e. HL /\ W e. H ) /\ ( W e. ( Base ` K ) /\ W ( le ` K ) W ) ) -> ( I ` W ) = { f e. T | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W } )
14	4 7 11 13	syl12anc	|- ( ( K e. HL /\ W e. H ) -> ( I ` W ) = { f e. T | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W } )
15	9 1 2 12	trlle	|- ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W )
16	15	ralrimiva	|- ( ( K e. HL /\ W e. H ) -> A. f e. T ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W )
17		rabid2	|- ( T = { f e. T | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W } <-> A. f e. T ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W )
18	16 17	sylibr	|- ( ( K e. HL /\ W e. H ) -> T = { f e. T | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) W } )
19	14 18	eqtr4d	|- ( ( K e. HL /\ W e. H ) -> ( I ` W ) = T )