Metamath Proof Explorer

Theorem islshpcv

Description: Hyperplane properties expressed with covers relation. (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses islshpcv.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
islshpcv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
islshpcv.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
islshpcv.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
islshpcv.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
Assertion islshpcv ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 islshpcv.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 islshpcv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 islshpcv.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
4 islshpcv.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
5 islshpcv.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 eqid ⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
7 eqid ⊢ ( LSAtoms ‘ 𝑊 ) = ( LSAtoms ‘ 𝑊 )
8 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9 5 8 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
10 1 2 6 3 7 9 islshpat ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) ) )
11 simp12 ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → 𝑈 ∈ 𝑆 )
12 1 2 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 )
13 11 12 syl ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → 𝑈 ⊆ 𝑉 )
14 simp13 ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → 𝑈 ≠ 𝑉 )
15 df-pss ⊢ ( 𝑈 ⊊ 𝑉 ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ 𝑉 ) )
16 13 14 15 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → 𝑈 ⊊ 𝑉 )
17 psseq2 ⊢ ( ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 → ( 𝑈 ⊊ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) ↔ 𝑈 ⊊ 𝑉 ) )
18 17 3ad2ant3 ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → ( 𝑈 ⊊ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) ↔ 𝑈 ⊊ 𝑉 ) )
19 16 18 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → 𝑈 ⊊ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) )
20 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) → 𝑊 ∈ LVec )
21 20 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → 𝑊 ∈ LVec )
22 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) )
23 2 6 7 4 21 11 22 lcv2 ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → ( 𝑈 ⊊ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) ↔ 𝑈 𝐶 ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) ) )
24 19 23 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → 𝑈 𝐶 ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) )
25 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 )
26 24 25 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → 𝑈 𝐶 𝑉 )
27 11 26 jca ⊢ ( ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) ∧ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) )
28 27 rexlimdv3a ⊢ ( ( 𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ) → ( ∃ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 → ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) )
29 28 3exp ⊢ ( 𝜑 → ( 𝑈 ∈ 𝑆 → ( 𝑈 ≠ 𝑉 → ( ∃ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 → ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) ) ) )
30 29 3impd ⊢ ( 𝜑 → ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) → ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) )
31 simprl ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) → 𝑈 ∈ 𝑆 )
32 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) → 𝑊 ∈ LVec )
33 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) → 𝑊 ∈ LMod )
34 1 2 lss1 ⊢ ( 𝑊 ∈ LMod → 𝑉 ∈ 𝑆 )
35 33 34 syl ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) → 𝑉 ∈ 𝑆 )
36 simprr ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) → 𝑈 𝐶 𝑉 )
37 2 4 32 31 35 36 lcvpss ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) → 𝑈 ⊊ 𝑉 )
38 37 pssned ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) → 𝑈 ≠ 𝑉 )
39 2 6 7 4 33 31 35 36 lcvat ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) → ∃ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 )
40 31 38 39 3jca ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) → ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) )
41 40 ex ⊢ ( 𝜑 → ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) → ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) ) )
42 30 41 impbid ⊢ ( 𝜑 → ( ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑞 ∈ ( LSAtoms ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) 𝑞 ) = 𝑉 ) ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) )
43 10 42 bitrd ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 𝐶 𝑉 ) ) )