Metamath Proof Explorer

Theorem dihmeetcl

Description: Closure of closed subspace meet for DVecH vector space. (Contributed by NM, 5-Aug-2014)

Ref Expression
Hypotheses dihmeetcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihmeetcl.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihmeetcl ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝑋 ∩ 𝑌 ) ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dihmeetcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dihmeetcl.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 1 2 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
4 3 adantrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
5 1 2 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) = 𝑌 )
6 5 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) = 𝑌 )
7 4 6 ineq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ) = ( 𝑋 ∩ 𝑌 ) )
8 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 9 1 2 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
11 10 adantrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
12 9 1 2 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
13 12 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
14 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
15 9 14 1 2 dihmeet ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) = ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ) )
16 8 11 13 15 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) = ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ) )
17 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
18 17 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → 𝐾 ∈ Lat )
19 9 14 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ◡ 𝐼 ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) )
20 18 11 13 19 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( ( ◡ 𝐼 ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) )
21 9 1 2 dihcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ◡ 𝐼 ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) ∈ ran 𝐼 )
22 20 21 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑌 ) ) ) ∈ ran 𝐼 )
23 16 22 eqeltrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑌 ) ) ) ∈ ran 𝐼 )
24 7 23 eqeltrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼 ) ) → ( 𝑋 ∩ 𝑌 ) ∈ ran 𝐼 )