Theorem dih1dimc

Description: Isomorphism H at an atom not under W . (Contributed by NM, 27-Apr-2014)

	Ref	Expression
Hypotheses	dih1dimc.l	|- .<_ = ( le ` K )
	dih1dimc.a	|- A = ( Atoms ` K )
	dih1dimc.h	|- H = ( LHyp ` K )
	dih1dimc.p	|- P = ( ( oc ` K ) ` W )
	dih1dimc.t	|- T = ( ( LTrn ` K ) ` W )
	dih1dimc.i	|- I = ( ( DIsoH ` K ) ` W )
	dih1dimc.u	|- U = ( ( DVecH ` K ) ` W )
	dih1dimc.n	|- N = ( LSpan ` U )
	dih1dimc.f	|- F = ( iota_ f e. T ( f ` P ) = Q )
Assertion	dih1dimc	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( N ` { <. F , ( _I |` T ) >. } ) )

Proof

Step	Hyp	Ref	Expression
1		dih1dimc.l	|- .<_ = ( le ` K )
2		dih1dimc.a	|- A = ( Atoms ` K )
3		dih1dimc.h	|- H = ( LHyp ` K )
4		dih1dimc.p	|- P = ( ( oc ` K ) ` W )
5		dih1dimc.t	|- T = ( ( LTrn ` K ) ` W )
6		dih1dimc.i	|- I = ( ( DIsoH ` K ) ` W )
7		dih1dimc.u	|- U = ( ( DVecH ` K ) ` W )
8		dih1dimc.n	|- N = ( LSpan ` U )
9		dih1dimc.f	|- F = ( iota_ f e. T ( f ` P ) = Q )
10		eqid	|- ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W )
11	1 2 3 10 6	dihvalcqat	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( ( ( DIsoC ` K ) ` W ) ` Q ) )
12	1 2 3 4 5 10 7 8 9	diclspsn	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( ( DIsoC ` K ) ` W ) ` Q ) = ( N ` { <. F , ( _I |` T ) >. } ) )
13	11 12	eqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( N ` { <. F , ( _I |` T ) >. } ) )