Metamath Proof Explorer

Theorem mapdin

Description: Subspace intersection is preserved by the map defined by df-mapd . Part of property (e) in Baer p. 40. (Contributed by NM, 12-Apr-2015)

Ref Expression
Hypotheses mapdin.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdin.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdin.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdin.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
mapdin.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdin.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
mapdin.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion mapdin ( 𝜑 → ( 𝑀 ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 mapdin.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdin.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3 mapdin.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 mapdin.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5 mapdin.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 mapdin.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
7 mapdin.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
8 inss1 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋
9 1 3 5 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
10 4 lssincl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 ∩ 𝑌 ) ∈ 𝑆 )
11 9 6 7 10 syl3anc ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ∈ 𝑆 )
12 1 3 4 2 5 11 6 mapdord ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( 𝑀 ‘ 𝑋 ) ↔ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋 ) )
13 8 12 mpbiri ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( 𝑀 ‘ 𝑋 ) )
14 inss2 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌
15 1 3 4 2 5 11 7 mapdord ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( 𝑀 ‘ 𝑌 ) ↔ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 ) )
16 14 15 mpbiri ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( 𝑀 ‘ 𝑌 ) )
17 13 16 ssind ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) )
18 eqid ⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
19 eqid ⊢ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
20 1 2 3 4 18 19 5 6 mapdcl2 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
21 1 2 18 19 5 mapdrn2 ⊢ ( 𝜑 → ran 𝑀 = ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
22 20 21 eleqtrrd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ ran 𝑀 )
23 1 2 3 4 18 19 5 7 mapdcl2 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
24 23 21 eleqtrrd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ ran 𝑀 )
25 1 2 3 18 5 22 24 mapdincl ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ∈ ran 𝑀 )
26 1 2 5 25 mapdcnvid2 ⊢ ( 𝜑 → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ) = ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) )
27 inss1 ⊢ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ⊆ ( 𝑀 ‘ 𝑋 )
28 26 27 eqsstrdi ⊢ ( 𝜑 → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ) ⊆ ( 𝑀 ‘ 𝑋 ) )
29 1 18 5 lcdlmod ⊢ ( 𝜑 → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod )
30 19 lssincl ⊢ ( ( ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod ∧ ( 𝑀 ‘ 𝑋 ) ∈ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ∈ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
31 29 20 23 30 syl3anc ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ∈ ( LSubSp ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
32 31 21 eleqtrrd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ∈ ran 𝑀 )
33 1 2 3 4 5 32 mapdcnvcl ⊢ ( 𝜑 → ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ∈ 𝑆 )
34 1 3 4 2 5 33 6 mapdord ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ) ⊆ ( 𝑀 ‘ 𝑋 ) ↔ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ⊆ 𝑋 ) )
35 28 34 mpbid ⊢ ( 𝜑 → ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ⊆ 𝑋 )
36 1 2 5 32 mapdcnvid2 ⊢ ( 𝜑 → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ) = ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) )
37 inss2 ⊢ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ⊆ ( 𝑀 ‘ 𝑌 )
38 36 37 eqsstrdi ⊢ ( 𝜑 → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ) ⊆ ( 𝑀 ‘ 𝑌 ) )
39 1 3 4 2 5 33 7 mapdord ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ) ⊆ ( 𝑀 ‘ 𝑌 ) ↔ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ⊆ 𝑌 ) )
40 38 39 mpbid ⊢ ( 𝜑 → ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ⊆ 𝑌 )
41 35 40 ssind ⊢ ( 𝜑 → ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ⊆ ( 𝑋 ∩ 𝑌 ) )
42 1 3 4 2 5 33 11 mapdord ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ) ⊆ ( 𝑀 ‘ ( 𝑋 ∩ 𝑌 ) ) ↔ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ⊆ ( 𝑋 ∩ 𝑌 ) ) )
43 41 42 mpbird ⊢ ( 𝜑 → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ) ) ⊆ ( 𝑀 ‘ ( 𝑋 ∩ 𝑌 ) ) )
44 26 43 eqsstrrd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) ⊆ ( 𝑀 ‘ ( 𝑋 ∩ 𝑌 ) ) )
45 17 44 eqssd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( 𝑀 ‘ 𝑋 ) ∩ ( 𝑀 ‘ 𝑌 ) ) )