Metamath Proof Explorer

Theorem mapdincl

Description: Closure of dual subspace intersection for the map defined by df-mapd . (Contributed by NM, 12-Apr-2015)

Ref Expression
Hypotheses mapdincl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdincl.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdincl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdincl.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
mapdincl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdincl.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝑀 )
mapdincl.y ⊢ ( 𝜑 → 𝑌 ∈ ran 𝑀 )
Assertion mapdincl ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ∈ ran 𝑀 )

Proof

Step Hyp Ref Expression
1 mapdincl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdincl.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3 mapdincl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 mapdincl.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
5 mapdincl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 mapdincl.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝑀 )
7 mapdincl.y ⊢ ( 𝜑 → 𝑌 ∈ ran 𝑀 )
8 eqid ⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
9 1 8 5 lcdlmod ⊢ ( 𝜑 → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod )
10 eqid ⊢ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
11 1 2 8 10 5 mapdrn2 ⊢ ( 𝜑 → ran 𝑀 = ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
12 6 11 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
13 7 11 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
14 10 lssincl ⊢ ( ( ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod ∧ 𝑋 ∈ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ 𝑌 ∈ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑋 ∩ 𝑌 ) ∈ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
15 9 12 13 14 syl3anc ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ∈ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
16 15 11 eleqtrrd ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ∈ ran 𝑀 )