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