This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihmeet2

Description: Reverse isomorphism H of a closed subspace intersection. (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dihmeet2.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihmeet2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihmeet2.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihmeet2.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dihmeet2.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
dihmeet2.y ⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
Assertion dihmeet2 ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 dihmeet2.m ⊢ ∧ = ( meet ‘ 𝐾 )
2 dihmeet2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dihmeet2.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dihmeet2.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
5 dihmeet2.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
6 dihmeet2.y ⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
7 2 3 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
8 4 5 7 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
9 2 3 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) = 𝑌 )
10 4 6 9 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) = 𝑌 )
11 8 10 ineq12d ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ) = ( 𝑋 ∩ 𝑌 ) )
12 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 12 2 3 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
14 4 5 13 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
15 12 2 3 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
16 4 6 15 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
17 12 1 2 3 dihmeet ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ) = ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ) )
18 4 14 16 17 syl3anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ) = ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ) )
19 2 3 dihmeetcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝑋 ∩ 𝑌 ) ∈ ran 𝐼 )
20 4 5 6 19 syl12anc ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ∈ ran 𝐼 )
21 2 3 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∩ 𝑌 ) ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑋 ∩ 𝑌 ) ) ) = ( 𝑋 ∩ 𝑌 ) )
22 4 20 21 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑋 ∩ 𝑌 ) ) ) = ( 𝑋 ∩ 𝑌 ) )
23 11 18 22 3eqtr4rd ⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑋 ∩ 𝑌 ) ) ) = ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ) )
24 12 2 3 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∩ 𝑌 ) ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ ( 𝑋 ∩ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) )
25 4 20 24 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑋 ∩ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) )
26 4 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
27 26 hllatd ⊢ ( 𝜑 → 𝐾 ∈ Lat )
28 12 1 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) )
29 27 14 16 28 syl3anc ⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) )
30 12 2 3 dih11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ◡ 𝐼 ‘ ( 𝑋 ∩ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑋 ∩ 𝑌 ) ) ) = ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ) ↔ ( ◡ 𝐼 ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ) )
31 4 25 29 30 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( 𝑋 ∩ 𝑌 ) ) ) = ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ) ↔ ( ◡ 𝐼 ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) ) )
32 23 31 mpbid ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ◡ 𝐼 ‘ 𝑋 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ) )