Theorem cdlemksv

Description: Part of proof of Lemma K of Crawley p. 118. Value of the sigma(p) function. (Contributed by NM, 26-Jun-2013)

	Ref	Expression
Hypotheses	cdlemk.b	|- B = ( Base ` K )
	cdlemk.l	|- .<_ = ( le ` K )
	cdlemk.j	|- .\/ = ( join ` K )
	cdlemk.a	|- A = ( Atoms ` K )
	cdlemk.h	|- H = ( LHyp ` K )
	cdlemk.t	|- T = ( ( LTrn ` K ) ` W )
	cdlemk.r	|- R = ( ( trL ` K ) ` W )
	cdlemk.m	|- ./\ = ( meet ` K )
	cdlemk.s	|- S = ( f e. T |-> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) )
Assertion	cdlemksv	|- ( G e. T -> ( S ` G ) = ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemk.b	|- B = ( Base ` K )
2		cdlemk.l	|- .<_ = ( le ` K )
3		cdlemk.j	|- .\/ = ( join ` K )
4		cdlemk.a	|- A = ( Atoms ` K )
5		cdlemk.h	|- H = ( LHyp ` K )
6		cdlemk.t	|- T = ( ( LTrn ` K ) ` W )
7		cdlemk.r	|- R = ( ( trL ` K ) ` W )
8		cdlemk.m	|- ./\ = ( meet ` K )
9		cdlemk.s	|- S = ( f e. T |-> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) )
10		fveq2	|- ( f = G -> ( R ` f ) = ( R ` G ) )
11	10	oveq2d	|- ( f = G -> ( P .\/ ( R ` f ) ) = ( P .\/ ( R ` G ) ) )
12		coeq1	|- ( f = G -> ( f o. `' F ) = ( G o. `' F ) )
13	12	fveq2d	|- ( f = G -> ( R ` ( f o. `' F ) ) = ( R ` ( G o. `' F ) ) )
14	13	oveq2d	|- ( f = G -> ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) = ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) )
15	11 14	oveq12d	|- ( f = G -> ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) )
16	15	eqeq2d	|- ( f = G -> ( ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) <-> ( i ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) ) )
17	16	riotabidv	|- ( f = G -> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) = ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) ) )
18		riotaex	|- ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) ) e. _V
19	17 9 18	fvmpt	|- ( G e. T -> ( S ` G ) = ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( N ` P ) .\/ ( R ` ( G o. `' F ) ) ) ) ) )