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∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→X∩Y=I⁡I-1⁡X∧˙I-1⁡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∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→K∈HL∧W∈H
5 2 3 diacnvclN ⊢K∈HL∧W∈H∧X∈ran⁡I→I-1⁡X∈dom⁡I
6 5 adantrr ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→I-1⁡X∈dom⁡I
7 2 3 diacnvclN ⊢K∈HL∧W∈H∧Y∈ran⁡I→I-1⁡Y∈dom⁡I
8 7 adantrl ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→I-1⁡Y∈dom⁡I
9 1 2 3 diameetN ⊢K∈HL∧W∈H∧I-1⁡X∈dom⁡I∧I-1⁡Y∈dom⁡I→I⁡I-1⁡X∧˙I-1⁡Y=I⁡I-1⁡X∩I⁡I-1⁡Y
10 4 6 8 9 syl12anc ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→I⁡I-1⁡X∧˙I-1⁡Y=I⁡I-1⁡X∩I⁡I-1⁡Y
11 2 3 diaf11N ⊢K∈HL∧W∈H→I:dom⁡I⟶1-1 ontoran⁡I
12 11 adantr ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→I:dom⁡I⟶1-1 ontoran⁡I
13 simprl ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→X∈ran⁡I
14 f1ocnvfv2 ⊢I:dom⁡I⟶1-1 ontoran⁡I∧X∈ran⁡I→I⁡I-1⁡X=X
15 12 13 14 syl2anc ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→I⁡I-1⁡X=X
16 simprr ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→Y∈ran⁡I
17 f1ocnvfv2 ⊢I:dom⁡I⟶1-1 ontoran⁡I∧Y∈ran⁡I→I⁡I-1⁡Y=Y
18 12 16 17 syl2anc ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→I⁡I-1⁡Y=Y
19 15 18 ineq12d ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→I⁡I-1⁡X∩I⁡I-1⁡Y=X∩Y
20 10 19 eqtr2d ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→X∩Y=I⁡I-1⁡X∧˙I-1⁡Y