Metamath Proof Explorer

Theorem mapdlsm

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

Ref Expression
Hypotheses mapdlsm.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdlsm.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdlsm.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdlsm.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
mapdlsm.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
mapdlsm.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
mapdlsm.q ⊢ ✚ = ( LSSum ‘ 𝐶 )
mapdlsm.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdlsm.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
mapdlsm.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion mapdlsm ( 𝜑 → ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) = ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 mapdlsm.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdlsm.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3 mapdlsm.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 mapdlsm.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5 mapdlsm.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
6 mapdlsm.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7 mapdlsm.q ⊢ ✚ = ( LSSum ‘ 𝐶 )
8 mapdlsm.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 mapdlsm.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
10 mapdlsm.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
11 1 6 8 lcdlmod ⊢ ( 𝜑 → 𝐶 ∈ LMod )
12 eqid ⊢ ( LSubSp ‘ 𝐶 ) = ( LSubSp ‘ 𝐶 )
13 12 lsssssubg ⊢ ( 𝐶 ∈ LMod → ( LSubSp ‘ 𝐶 ) ⊆ ( SubGrp ‘ 𝐶 ) )
14 11 13 syl ⊢ ( 𝜑 → ( LSubSp ‘ 𝐶 ) ⊆ ( SubGrp ‘ 𝐶 ) )
15 1 2 3 4 6 12 8 9 mapdcl2 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝐶 ) )
16 14 15 sseldd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐶 ) )
17 1 2 3 4 6 12 8 10 mapdcl2 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝐶 ) )
18 14 17 sseldd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ ( SubGrp ‘ 𝐶 ) )
19 7 lsmub1 ⊢ ( ( ( 𝑀 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐶 ) ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( SubGrp ‘ 𝐶 ) ) → ( 𝑀 ‘ 𝑋 ) ⊆ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) )
20 16 18 19 syl2anc ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ⊆ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) )
21 1 2 3 4 8 9 mapdcl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ ran 𝑀 )
22 1 2 3 4 8 10 mapdcl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ ran 𝑀 )
23 1 2 3 6 7 8 21 22 mapdlsmcl ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ∈ ran 𝑀 )
24 1 2 8 23 mapdcnvid2 ⊢ ( 𝜑 → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) = ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) )
25 20 24 sseqtrrd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) )
26 1 2 3 4 8 23 mapdcnvcl ⊢ ( 𝜑 → ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ∈ 𝑆 )
27 1 3 4 2 8 9 26 mapdord ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) ↔ 𝑋 ⊆ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) )
28 25 27 mpbid ⊢ ( 𝜑 → 𝑋 ⊆ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) )
29 7 lsmub2 ⊢ ( ( ( 𝑀 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐶 ) ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( SubGrp ‘ 𝐶 ) ) → ( 𝑀 ‘ 𝑌 ) ⊆ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) )
30 16 18 29 syl2anc ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ⊆ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) )
31 30 24 sseqtrrd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ⊆ ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) )
32 1 3 4 2 8 10 26 mapdord ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑌 ) ⊆ ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) ↔ 𝑌 ⊆ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) )
33 31 32 mpbid ⊢ ( 𝜑 → 𝑌 ⊆ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) )
34 1 3 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
35 4 lsssssubg ⊢ ( 𝑈 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
36 34 35 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
37 36 9 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( SubGrp ‘ 𝑈 ) )
38 36 10 sseldd ⊢ ( 𝜑 → 𝑌 ∈ ( SubGrp ‘ 𝑈 ) )
39 36 26 sseldd ⊢ ( 𝜑 → ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ∈ ( SubGrp ‘ 𝑈 ) )
40 5 lsmlub ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑈 ) ∧ 𝑌 ∈ ( SubGrp ‘ 𝑈 ) ∧ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ∈ ( SubGrp ‘ 𝑈 ) ) → ( ( 𝑋 ⊆ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ∧ 𝑌 ⊆ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) ↔ ( 𝑋 ⊕ 𝑌 ) ⊆ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) )
41 37 38 39 40 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 ⊆ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ∧ 𝑌 ⊆ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) ↔ ( 𝑋 ⊕ 𝑌 ) ⊆ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) )
42 28 33 41 mpbi2and ⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑌 ) ⊆ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) )
43 4 5 lsmcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 ⊕ 𝑌 ) ∈ 𝑆 )
44 34 9 10 43 syl3anc ⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑌 ) ∈ 𝑆 )
45 1 3 4 2 8 44 26 mapdord ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ⊆ ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) ↔ ( 𝑋 ⊕ 𝑌 ) ⊆ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) )
46 42 45 mpbird ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ⊆ ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ) ) )
47 46 24 sseqtrd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ⊆ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) )
48 5 lsmub1 ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑈 ) ∧ 𝑌 ∈ ( SubGrp ‘ 𝑈 ) ) → 𝑋 ⊆ ( 𝑋 ⊕ 𝑌 ) )
49 37 38 48 syl2anc ⊢ ( 𝜑 → 𝑋 ⊆ ( 𝑋 ⊕ 𝑌 ) )
50 1 3 4 2 8 9 44 mapdord ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ↔ 𝑋 ⊆ ( 𝑋 ⊕ 𝑌 ) ) )
51 49 50 mpbird ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) )
52 5 lsmub2 ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑈 ) ∧ 𝑌 ∈ ( SubGrp ‘ 𝑈 ) ) → 𝑌 ⊆ ( 𝑋 ⊕ 𝑌 ) )
53 37 38 52 syl2anc ⊢ ( 𝜑 → 𝑌 ⊆ ( 𝑋 ⊕ 𝑌 ) )
54 1 3 4 2 8 10 44 mapdord ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑌 ) ⊆ ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ↔ 𝑌 ⊆ ( 𝑋 ⊕ 𝑌 ) ) )
55 53 54 mpbird ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ⊆ ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) )
56 1 2 3 4 6 12 8 44 mapdcl2 ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ∈ ( LSubSp ‘ 𝐶 ) )
57 14 56 sseldd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ∈ ( SubGrp ‘ 𝐶 ) )
58 7 lsmlub ⊢ ( ( ( 𝑀 ‘ 𝑋 ) ∈ ( SubGrp ‘ 𝐶 ) ∧ ( 𝑀 ‘ 𝑌 ) ∈ ( SubGrp ‘ 𝐶 ) ∧ ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ∈ ( SubGrp ‘ 𝐶 ) ) → ( ( ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ∧ ( 𝑀 ‘ 𝑌 ) ⊆ ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ) ↔ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ⊆ ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ) )
59 16 18 57 58 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑀 ‘ 𝑋 ) ⊆ ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ∧ ( 𝑀 ‘ 𝑌 ) ⊆ ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ) ↔ ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ⊆ ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) ) )
60 51 55 59 mpbi2and ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) ⊆ ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) )
61 47 60 eqssd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑋 ⊕ 𝑌 ) ) = ( ( 𝑀 ‘ 𝑋 ) ✚ ( 𝑀 ‘ 𝑌 ) ) )