Metamath Proof Explorer

Theorem diainN

Description: Inverse partial isomorphism A of an intersection. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses diam.m 
|- ./\ = ( meet ` K )
diam.h 
|- H = ( LHyp ` K )
diam.i 
|- I = ( ( DIsoA ` K ) ` W )
Assertion diainN 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> ( X i^i Y ) = ( I ` ( ( `' I ` X ) ./\ ( `' I ` Y ) ) ) )

Proof

Step Hyp Ref Expression
1 diam.m 
 |-  ./\ = ( meet ` K )
2 diam.h 
 |-  H = ( LHyp ` K )
3 diam.i 
 |-  I = ( ( DIsoA ` K ) ` W )
4 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> ( K e. HL /\ W e. H ) )
5 2 3 diacnvclN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. dom I )
6 5 adantrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> ( `' I ` X ) e. dom I )
7 2 3 diacnvclN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. ran I ) -> ( `' I ` Y ) e. dom I )
8 7 adantrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> ( `' I ` Y ) e. dom I )
9 1 2 3 diameetN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( `' I ` X ) e. dom I /\ ( `' I ` Y ) e. dom I ) ) -> ( I ` ( ( `' I ` X ) ./\ ( `' I ` Y ) ) ) = ( ( I ` ( `' I ` X ) ) i^i ( I ` ( `' I ` Y ) ) ) )
10 4 6 8 9 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> ( I ` ( ( `' I ` X ) ./\ ( `' I ` Y ) ) ) = ( ( I ` ( `' I ` X ) ) i^i ( I ` ( `' I ` Y ) ) ) )
11 2 3 diaf11N 
 |-  ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I )
12 11 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> I : dom I -1-1-onto-> ran I )
13 simprl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> X e. ran I )
14 f1ocnvfv2 
 |-  ( ( I : dom I -1-1-onto-> ran I /\ X e. ran I ) -> ( I ` ( `' I ` X ) ) = X )
15 12 13 14 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> ( I ` ( `' I ` X ) ) = X )
16 simprr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> Y e. ran I )
17 f1ocnvfv2 
 |-  ( ( I : dom I -1-1-onto-> ran I /\ Y e. ran I ) -> ( I ` ( `' I ` Y ) ) = Y )
18 12 16 17 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> ( I ` ( `' I ` Y ) ) = Y )
19 15 18 ineq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> ( ( I ` ( `' I ` X ) ) i^i ( I ` ( `' I ` Y ) ) ) = ( X i^i Y ) )
20 10 19 eqtr2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ran I /\ Y e. ran I ) ) -> ( X i^i Y ) = ( I ` ( ( `' I ` X ) ./\ ( `' I ` Y ) ) ) )