This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) ) ) )