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 onto ran ⁡ I
12 11 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I
13 simprl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → X ∈ ran ⁡ I
14 f1ocnvfv2 ⊢ I : dom ⁡ I ⟶ 1-1 onto ran ⁡ 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 onto ran ⁡ 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