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 ‘ 𝐾 )
diam.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
diam.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion diainN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝑋 ∩ 𝑌 ) = ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 diam.m ⊢ ∧ = ( meet ‘ 𝐾 )
2 diam.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 diam.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
5 2 3 diacnvclN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ dom 𝐼 )
6 5 adantrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ dom 𝐼 )
7 2 3 diacnvclN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑌 ) ∈ dom 𝐼 )
8 7 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( ◡ 𝐼 ‘ 𝑌 ) ∈ dom 𝐼 )
9 1 2 3 diameetN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ◡ 𝐼 ‘ 𝑋 ) ∈ dom 𝐼 ∧ ( ◡ 𝐼 ‘ 𝑌 ) ∈ dom 𝐼 ) ) → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ) = ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ) )
10 4 6 8 9 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ) = ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ) )
11 2 3 diaf11N ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 )
12 11 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 )
13 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → 𝑋 ∈ ran 𝐼 )
14 f1ocnvfv2 ⊢ ( ( 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
15 12 13 14 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
16 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → 𝑌 ∈ ran 𝐼 )
17 f1ocnvfv2 ⊢ ( ( 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) = 𝑌 )
18 12 16 17 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) = 𝑌 )
19 15 18 ineq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ) = ( 𝑋 ∩ 𝑌 ) )
20 10 19 eqtr2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝑋 ∩ 𝑌 ) = ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ) )