Metamath Proof Explorer


Theorem cdlemkuu

Description: Convert between function and operation forms of Y . TODO: Use operation form everywhere. (Contributed by NM, 6-Jul-2013)

Ref Expression
Hypotheses cdlemk3.b
|- B = ( Base ` K )
cdlemk3.l
|- .<_ = ( le ` K )
cdlemk3.j
|- .\/ = ( join ` K )
cdlemk3.m
|- ./\ = ( meet ` K )
cdlemk3.a
|- A = ( Atoms ` K )
cdlemk3.h
|- H = ( LHyp ` K )
cdlemk3.t
|- T = ( ( LTrn ` K ) ` W )
cdlemk3.r
|- R = ( ( trL ` K ) ` W )
cdlemk3.s
|- S = ( f e. T |-> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) )
cdlemk3.u1
|- Y = ( d e. T , e e. T |-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` d ) ` P ) .\/ ( R ` ( e o. `' d ) ) ) ) ) )
cdlemk3.o2
|- Q = ( S ` D )
cdlemk3.u2
|- Z = ( e e. T |-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) )
Assertion cdlemkuu
|- ( ( D e. T /\ G e. T ) -> ( D Y G ) = ( Z ` G ) )

Proof

Step Hyp Ref Expression
1 cdlemk3.b
 |-  B = ( Base ` K )
2 cdlemk3.l
 |-  .<_ = ( le ` K )
3 cdlemk3.j
 |-  .\/ = ( join ` K )
4 cdlemk3.m
 |-  ./\ = ( meet ` K )
5 cdlemk3.a
 |-  A = ( Atoms ` K )
6 cdlemk3.h
 |-  H = ( LHyp ` K )
7 cdlemk3.t
 |-  T = ( ( LTrn ` K ) ` W )
8 cdlemk3.r
 |-  R = ( ( trL ` K ) ` W )
9 cdlemk3.s
 |-  S = ( f e. T |-> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) )
10 cdlemk3.u1
 |-  Y = ( d e. T , e e. T |-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` d ) ` P ) .\/ ( R ` ( e o. `' d ) ) ) ) ) )
11 cdlemk3.o2
 |-  Q = ( S ` D )
12 cdlemk3.u2
 |-  Z = ( e e. T |-> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) )
13 fveq2
 |-  ( d = D -> ( S ` d ) = ( S ` D ) )
14 13 11 eqtr4di
 |-  ( d = D -> ( S ` d ) = Q )
15 14 fveq1d
 |-  ( d = D -> ( ( S ` d ) ` P ) = ( Q ` P ) )
16 cnveq
 |-  ( d = D -> `' d = `' D )
17 16 coeq2d
 |-  ( d = D -> ( e o. `' d ) = ( e o. `' D ) )
18 17 fveq2d
 |-  ( d = D -> ( R ` ( e o. `' d ) ) = ( R ` ( e o. `' D ) ) )
19 15 18 oveq12d
 |-  ( d = D -> ( ( ( S ` d ) ` P ) .\/ ( R ` ( e o. `' d ) ) ) = ( ( Q ` P ) .\/ ( R ` ( e o. `' D ) ) ) )
20 19 oveq2d
 |-  ( d = D -> ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` d ) ` P ) .\/ ( R ` ( e o. `' d ) ) ) ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) )
21 20 eqeq2d
 |-  ( d = D -> ( ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` d ) ` P ) .\/ ( R ` ( e o. `' d ) ) ) ) <-> ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) )
22 21 riotabidv
 |-  ( d = D -> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( ( S ` d ) ` P ) .\/ ( R ` ( e o. `' d ) ) ) ) ) = ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) )
23 fveq2
 |-  ( e = G -> ( R ` e ) = ( R ` G ) )
24 23 oveq2d
 |-  ( e = G -> ( P .\/ ( R ` e ) ) = ( P .\/ ( R ` G ) ) )
25 coeq1
 |-  ( e = G -> ( e o. `' D ) = ( G o. `' D ) )
26 25 fveq2d
 |-  ( e = G -> ( R ` ( e o. `' D ) ) = ( R ` ( G o. `' D ) ) )
27 26 oveq2d
 |-  ( e = G -> ( ( Q ` P ) .\/ ( R ` ( e o. `' D ) ) ) = ( ( Q ` P ) .\/ ( R ` ( G o. `' D ) ) ) )
28 24 27 oveq12d
 |-  ( e = G -> ( ( P .\/ ( R ` e ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) )
29 28 eqeq2d
 |-  ( e = G -> ( ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) <-> ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) )
30 29 riotabidv
 |-  ( e = G -> ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` e ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( e o. `' D ) ) ) ) ) = ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) )
31 riotaex
 |-  ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) e. _V
32 22 30 10 31 ovmpo
 |-  ( ( D e. T /\ G e. T ) -> ( D Y G ) = ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) )
33 1 2 3 5 6 7 8 4 12 cdlemksv
 |-  ( G e. T -> ( Z ` G ) = ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) )
34 33 adantl
 |-  ( ( D e. T /\ G e. T ) -> ( Z ` G ) = ( iota_ j e. T ( j ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( G o. `' D ) ) ) ) ) )
35 32 34 eqtr4d
 |-  ( ( D e. T /\ G e. T ) -> ( D Y G ) = ( Z ` G ) )