Metamath Proof Explorer

Theorem mapdcv

Description: Covering property of the converse of the map defined by df-mapd . (Contributed by NM, 14-Mar-2015)

Ref Expression
Hypotheses mapdcv.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdcv.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdcv.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdcv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
mapdcv.c ⊢ 𝐶 = ( ⋖L ‘ 𝑈 )
mapdcv.d ⊢ 𝐷 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
mapdcv.e ⊢ 𝐸 = ( ⋖L ‘ 𝐷 )
mapdcv.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdcv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
mapdcv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion mapdcv ( 𝜑 → ( 𝑋 𝐶 𝑌 ↔ ( 𝑀 ‘ 𝑋 ) 𝐸 ( 𝑀 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 mapdcv.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdcv.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3 mapdcv.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 mapdcv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5 mapdcv.c ⊢ 𝐶 = ( ⋖L ‘ 𝑈 )
6 mapdcv.d ⊢ 𝐷 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7 mapdcv.e ⊢ 𝐸 = ( ⋖L ‘ 𝐷 )
8 mapdcv.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 mapdcv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
10 mapdcv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
11 1 2 3 4 8 9 10 mapdsord ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ⊊ ( 𝑀 ‘ 𝑌 ) ↔ 𝑋 ⊊ 𝑌 ) )
12 eqid ⊢ ( LSubSp ‘ 𝐷 ) = ( LSubSp ‘ 𝐷 )
13 8 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ) → 𝑣 ∈ 𝑆 )
15 1 2 3 4 6 12 13 14 mapdcl2 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑀 ‘ 𝑣 ) ∈ ( LSubSp ‘ 𝐷 ) )
16 8 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( LSubSp ‘ 𝐷 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 1 2 6 12 8 mapdrn2 ⊢ ( 𝜑 → ran 𝑀 = ( LSubSp ‘ 𝐷 ) )
18 17 eleq2d ⊢ ( 𝜑 → ( 𝑓 ∈ ran 𝑀 ↔ 𝑓 ∈ ( LSubSp ‘ 𝐷 ) ) )
19 18 biimpar ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( LSubSp ‘ 𝐷 ) ) → 𝑓 ∈ ran 𝑀 )
20 1 2 3 4 16 19 mapdcnvcl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( LSubSp ‘ 𝐷 ) ) → ( ◡ 𝑀 ‘ 𝑓 ) ∈ 𝑆 )
21 1 2 16 19 mapdcnvid2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( LSubSp ‘ 𝐷 ) ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑓 ) ) = 𝑓 )
22 21 eqcomd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( LSubSp ‘ 𝐷 ) ) → 𝑓 = ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑓 ) ) )
23 fveq2 ⊢ ( 𝑣 = ( ◡ 𝑀 ‘ 𝑓 ) → ( 𝑀 ‘ 𝑣 ) = ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑓 ) ) )
24 23 rspceeqv ⊢ ( ( ( ◡ 𝑀 ‘ 𝑓 ) ∈ 𝑆 ∧ 𝑓 = ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑓 ) ) ) → ∃ 𝑣 ∈ 𝑆 𝑓 = ( 𝑀 ‘ 𝑣 ) )
25 20 22 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( LSubSp ‘ 𝐷 ) ) → ∃ 𝑣 ∈ 𝑆 𝑓 = ( 𝑀 ‘ 𝑣 ) )
26 psseq2 ⊢ ( 𝑓 = ( 𝑀 ‘ 𝑣 ) → ( ( 𝑀 ‘ 𝑋 ) ⊊ 𝑓 ↔ ( 𝑀 ‘ 𝑋 ) ⊊ ( 𝑀 ‘ 𝑣 ) ) )
27 psseq1 ⊢ ( 𝑓 = ( 𝑀 ‘ 𝑣 ) → ( 𝑓 ⊊ ( 𝑀 ‘ 𝑌 ) ↔ ( 𝑀 ‘ 𝑣 ) ⊊ ( 𝑀 ‘ 𝑌 ) ) )
28 26 27 anbi12d ⊢ ( 𝑓 = ( 𝑀 ‘ 𝑣 ) → ( ( ( 𝑀 ‘ 𝑋 ) ⊊ 𝑓 ∧ 𝑓 ⊊ ( 𝑀 ‘ 𝑌 ) ) ↔ ( ( 𝑀 ‘ 𝑋 ) ⊊ ( 𝑀 ‘ 𝑣 ) ∧ ( 𝑀 ‘ 𝑣 ) ⊊ ( 𝑀 ‘ 𝑌 ) ) ) )
29 28 adantl ⊢ ( ( 𝜑 ∧ 𝑓 = ( 𝑀 ‘ 𝑣 ) ) → ( ( ( 𝑀 ‘ 𝑋 ) ⊊ 𝑓 ∧ 𝑓 ⊊ ( 𝑀 ‘ 𝑌 ) ) ↔ ( ( 𝑀 ‘ 𝑋 ) ⊊ ( 𝑀 ‘ 𝑣 ) ∧ ( 𝑀 ‘ 𝑣 ) ⊊ ( 𝑀 ‘ 𝑌 ) ) ) )
30 15 25 29 rexxfrd ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( LSubSp ‘ 𝐷 ) ( ( 𝑀 ‘ 𝑋 ) ⊊ 𝑓 ∧ 𝑓 ⊊ ( 𝑀 ‘ 𝑌 ) ) ↔ ∃ 𝑣 ∈ 𝑆 ( ( 𝑀 ‘ 𝑋 ) ⊊ ( 𝑀 ‘ 𝑣 ) ∧ ( 𝑀 ‘ 𝑣 ) ⊊ ( 𝑀 ‘ 𝑌 ) ) ) )
31 9 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
32 1 2 3 4 13 31 14 mapdsord ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ) → ( ( 𝑀 ‘ 𝑋 ) ⊊ ( 𝑀 ‘ 𝑣 ) ↔ 𝑋 ⊊ 𝑣 ) )
33 10 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ) → 𝑌 ∈ 𝑆 )
34 1 2 3 4 13 14 33 mapdsord ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ) → ( ( 𝑀 ‘ 𝑣 ) ⊊ ( 𝑀 ‘ 𝑌 ) ↔ 𝑣 ⊊ 𝑌 ) )
35 32 34 anbi12d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ) → ( ( ( 𝑀 ‘ 𝑋 ) ⊊ ( 𝑀 ‘ 𝑣 ) ∧ ( 𝑀 ‘ 𝑣 ) ⊊ ( 𝑀 ‘ 𝑌 ) ) ↔ ( 𝑋 ⊊ 𝑣 ∧ 𝑣 ⊊ 𝑌 ) ) )
36 35 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝑆 ( ( 𝑀 ‘ 𝑋 ) ⊊ ( 𝑀 ‘ 𝑣 ) ∧ ( 𝑀 ‘ 𝑣 ) ⊊ ( 𝑀 ‘ 𝑌 ) ) ↔ ∃ 𝑣 ∈ 𝑆 ( 𝑋 ⊊ 𝑣 ∧ 𝑣 ⊊ 𝑌 ) ) )
37 30 36 bitrd ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( LSubSp ‘ 𝐷 ) ( ( 𝑀 ‘ 𝑋 ) ⊊ 𝑓 ∧ 𝑓 ⊊ ( 𝑀 ‘ 𝑌 ) ) ↔ ∃ 𝑣 ∈ 𝑆 ( 𝑋 ⊊ 𝑣 ∧ 𝑣 ⊊ 𝑌 ) ) )
38 37 notbid ⊢ ( 𝜑 → ( ¬ ∃ 𝑓 ∈ ( LSubSp ‘ 𝐷 ) ( ( 𝑀 ‘ 𝑋 ) ⊊ 𝑓 ∧ 𝑓 ⊊ ( 𝑀 ‘ 𝑌 ) ) ↔ ¬ ∃ 𝑣 ∈ 𝑆 ( 𝑋 ⊊ 𝑣 ∧ 𝑣 ⊊ 𝑌 ) ) )
39 11 38 anbi12d ⊢ ( 𝜑 → ( ( ( 𝑀 ‘ 𝑋 ) ⊊ ( 𝑀 ‘ 𝑌 ) ∧ ¬ ∃ 𝑓 ∈ ( LSubSp ‘ 𝐷 ) ( ( 𝑀 ‘ 𝑋 ) ⊊ 𝑓 ∧ 𝑓 ⊊ ( 𝑀 ‘ 𝑌 ) ) ) ↔ ( 𝑋 ⊊ 𝑌 ∧ ¬ ∃ 𝑣 ∈ 𝑆 ( 𝑋 ⊊ 𝑣 ∧ 𝑣 ⊊ 𝑌 ) ) ) )
40 1 6 8 lcdlmod ⊢ ( 𝜑 → 𝐷 ∈ LMod )
41 1 2 3 4 6 12 8 9 mapdcl2 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝐷 ) )
42 1 2 3 4 6 12 8 10 mapdcl2 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ ( LSubSp ‘ 𝐷 ) )
43 12 7 40 41 42 lcvbr ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) 𝐸 ( 𝑀 ‘ 𝑌 ) ↔ ( ( 𝑀 ‘ 𝑋 ) ⊊ ( 𝑀 ‘ 𝑌 ) ∧ ¬ ∃ 𝑓 ∈ ( LSubSp ‘ 𝐷 ) ( ( 𝑀 ‘ 𝑋 ) ⊊ 𝑓 ∧ 𝑓 ⊊ ( 𝑀 ‘ 𝑌 ) ) ) ) )
44 1 3 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
45 4 5 44 9 10 lcvbr ⊢ ( 𝜑 → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ⊊ 𝑌 ∧ ¬ ∃ 𝑣 ∈ 𝑆 ( 𝑋 ⊊ 𝑣 ∧ 𝑣 ⊊ 𝑌 ) ) ) )
46 39 43 45 3bitr4rd ⊢ ( 𝜑 → ( 𝑋 𝐶 𝑌 ↔ ( 𝑀 ‘ 𝑋 ) 𝐸 ( 𝑀 ‘ 𝑌 ) ) )