Theorem cdlemn7

Description: Part of proof of Lemma N of Crawley p. 121 line 36. (Contributed by NM, 26-Feb-2014)

	Ref	Expression
Hypotheses	cdlemn8.b	|- B = ( Base ` K )
	cdlemn8.l	|- .<_ = ( le ` K )
	cdlemn8.a	|- A = ( Atoms ` K )
	cdlemn8.h	|- H = ( LHyp ` K )
	cdlemn8.p	|- P = ( ( oc ` K ) ` W )
	cdlemn8.o	|- O = ( h e. T |-> ( _I |` B ) )
	cdlemn8.t	|- T = ( ( LTrn ` K ) ` W )
	cdlemn8.e	|- E = ( ( TEndo ` K ) ` W )
	cdlemn8.u	|- U = ( ( DVecH ` K ) ` W )
	cdlemn8.s	|- .+ = ( +g ` U )
	cdlemn8.f	|- F = ( iota_ h e. T ( h ` P ) = Q )
	cdlemn8.g	|- G = ( iota_ h e. T ( h ` P ) = R )
Assertion	cdlemn7	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> ( G = ( ( s ` F ) o. g ) /\ ( _I |` T ) = s ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemn8.b	|- B = ( Base ` K )
2		cdlemn8.l	|- .<_ = ( le ` K )
3		cdlemn8.a	|- A = ( Atoms ` K )
4		cdlemn8.h	|- H = ( LHyp ` K )
5		cdlemn8.p	|- P = ( ( oc ` K ) ` W )
6		cdlemn8.o	|- O = ( h e. T |-> ( _I |` B ) )
7		cdlemn8.t	|- T = ( ( LTrn ` K ) ` W )
8		cdlemn8.e	|- E = ( ( TEndo ` K ) ` W )
9		cdlemn8.u	|- U = ( ( DVecH ` K ) ` W )
10		cdlemn8.s	|- .+ = ( +g ` U )
11		cdlemn8.f	|- F = ( iota_ h e. T ( h ` P ) = Q )
12		cdlemn8.g	|- G = ( iota_ h e. T ( h ` P ) = R )
13		simp33	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) )
14		simp1	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> ( K e. HL /\ W e. H ) )
15		simp2l	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
16		simp2r	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> ( R e. A /\ -. R .<_ W ) )
17		simp31	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> s e. E )
18		simp32	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> g e. T )
19	1 2 3 4 5 6 7 8 9 10 11	cdlemn6	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T ) ) -> ( <. ( s ` F ) , s >. .+ <. g , O >. ) = <. ( ( s ` F ) o. g ) , s >. )
20	14 15 16 17 18 19	syl122anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> ( <. ( s ` F ) , s >. .+ <. g , O >. ) = <. ( ( s ` F ) o. g ) , s >. )
21	13 20	eqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> <. G , ( _I |` T ) >. = <. ( ( s ` F ) o. g ) , s >. )
22		fvex	|- ( s ` F ) e. _V
23		vex	|- g e. _V
24	22 23	coex	|- ( ( s ` F ) o. g ) e. _V
25		vex	|- s e. _V
26	24 25	opth2	|- ( <. G , ( _I |` T ) >. = <. ( ( s ` F ) o. g ) , s >. <-> ( G = ( ( s ` F ) o. g ) /\ ( _I |` T ) = s ) )
27	21 26	sylib	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( s e. E /\ g e. T /\ <. G , ( _I |` T ) >. = ( <. ( s ` F ) , s >. .+ <. g , O >. ) ) ) -> ( G = ( ( s ` F ) o. g ) /\ ( _I |` T ) = s ) )