Theorem mapdordlem1a

Description: Lemma for mapdord . (Contributed by NM, 27-Jan-2015)

	Ref	Expression
Hypotheses	mapdordlem1a.h	|- H = ( LHyp ` K )
	mapdordlem1a.o	|- O = ( ( ocH ` K ) ` W )
	mapdordlem1a.u	|- U = ( ( DVecH ` K ) ` W )
	mapdordlem1a.v	|- V = ( Base ` U )
	mapdordlem1a.y	|- Y = ( LSHyp ` U )
	mapdordlem1a.f	|- F = ( LFnl ` U )
	mapdordlem1a.l	|- L = ( LKer ` U )
	mapdordlem1a.t	|- T = { g e. F | ( O ` ( O ` ( L ` g ) ) ) e. Y }
	mapdordlem1a.c	|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
	mapdordlem1a.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	mapdordlem1a	|- ( ph -> ( J e. T <-> ( J e. C /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		mapdordlem1a.h	|- H = ( LHyp ` K )
2		mapdordlem1a.o	|- O = ( ( ocH ` K ) ` W )
3		mapdordlem1a.u	|- U = ( ( DVecH ` K ) ` W )
4		mapdordlem1a.v	|- V = ( Base ` U )
5		mapdordlem1a.y	|- Y = ( LSHyp ` U )
6		mapdordlem1a.f	|- F = ( LFnl ` U )
7		mapdordlem1a.l	|- L = ( LKer ` U )
8		mapdordlem1a.t	|- T = { g e. F | ( O ` ( O ` ( L ` g ) ) ) e. Y }
9		mapdordlem1a.c	|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
10		mapdordlem1a.k	|- ( ph -> ( K e. HL /\ W e. H ) )
11		simprr	|- ( ( ph /\ ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) -> ( O ` ( O ` ( L ` J ) ) ) e. Y )
12	10	adantr	|- ( ( ph /\ ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) -> ( K e. HL /\ W e. H ) )
13		simprl	|- ( ( ph /\ ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) -> J e. F )
14	1 2 3 6 5 7 12 13	dochlkr	|- ( ( ph /\ ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) -> ( ( O ` ( O ` ( L ` J ) ) ) e. Y <-> ( ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) /\ ( L ` J ) e. Y ) ) )
15	11 14	mpbid	|- ( ( ph /\ ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) -> ( ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) /\ ( L ` J ) e. Y ) )
16	15	simpld	|- ( ( ph /\ ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) -> ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) )
17	16	ex	|- ( ph -> ( ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) -> ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) ) )
18	17	pm4.71rd	|- ( ph -> ( ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) <-> ( ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) /\ ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) ) )
19		2fveq3	|- ( g = J -> ( O ` ( L ` g ) ) = ( O ` ( L ` J ) ) )
20	19	fveq2d	|- ( g = J -> ( O ` ( O ` ( L ` g ) ) ) = ( O ` ( O ` ( L ` J ) ) ) )
21	20	eleq1d	|- ( g = J -> ( ( O ` ( O ` ( L ` g ) ) ) e. Y <-> ( O ` ( O ` ( L ` J ) ) ) e. Y ) )
22	21 8	elrab2	|- ( J e. T <-> ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) )
23	9	lcfl1lem	|- ( J e. C <-> ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) ) )
24	23	anbi1i	|- ( ( J e. C /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) <-> ( ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) ) /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) )
25		anass	|- ( ( ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) ) /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) <-> ( J e. F /\ ( ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) )
26		an12	|- ( ( J e. F /\ ( ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) <-> ( ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) /\ ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) )
27	24 25 26	3bitri	|- ( ( J e. C /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) <-> ( ( O ` ( O ` ( L ` J ) ) ) = ( L ` J ) /\ ( J e. F /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) )
28	18 22 27	3bitr4g	|- ( ph -> ( J e. T <-> ( J e. C /\ ( O ` ( O ` ( L ` J ) ) ) e. Y ) ) )