Metamath Proof Explorer

Theorem dvh4dimlem

Description: Lemma for dvh4dimN . (Contributed by NM, 22-May-2015)

Ref Expression
Hypotheses dvh3dim.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvh3dim.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvh3dim.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dvh3dim.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dvh3dim.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dvh3dim.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
dvh4dim.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
dvhdim.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
dvh4dim.o ⊢ 0 = ( 0g ‘ 𝑈 )
dvh4dim.x ⊢ ( 𝜑 → 𝑋 ≠ 0 )
dvh4dimlem.y ⊢ ( 𝜑 → 𝑌 ≠ 0 )
dvh4dimlem.z ⊢ ( 𝜑 → 𝑍 ≠ 0 )
Assertion dvh4dimlem ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )

Proof

Step Hyp Ref Expression
1 dvh3dim.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvh3dim.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dvh3dim.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 dvh3dim.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5 dvh3dim.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 dvh3dim.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7 dvh4dim.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8 dvhdim.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
9 dvh4dim.o ⊢ 0 = ( 0g ‘ 𝑈 )
10 dvh4dim.x ⊢ ( 𝜑 → 𝑋 ≠ 0 )
11 dvh4dimlem.y ⊢ ( 𝜑 → 𝑌 ≠ 0 )
12 dvh4dimlem.z ⊢ ( 𝜑 → 𝑍 ≠ 0 )
13 eqid ⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
14 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
15 1 2 5 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
16 eldifsn ⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) )
17 6 10 16 sylanbrc ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
18 3 4 9 14 15 17 lsatlspsn ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSAtoms ‘ 𝑈 ) )
19 eldifsn ⊢ ( 𝑌 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑌 ∈ 𝑉 ∧ 𝑌 ≠ 0 ) )
20 7 11 19 sylanbrc ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
21 3 4 9 14 15 20 lsatlspsn ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSAtoms ‘ 𝑈 ) )
22 eldifsn ⊢ ( 𝑍 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑍 ∈ 𝑉 ∧ 𝑍 ≠ 0 ) )
23 8 12 22 sylanbrc ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
24 3 4 9 14 15 23 lsatlspsn ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSAtoms ‘ 𝑈 ) )
25 1 2 13 14 5 18 21 24 dvh4dimat ⊢ ( 𝜑 → ∃ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) )
26 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ∧ ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) ) → 𝑈 ∈ LMod )
27 simp2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ∧ ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) ) → 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) )
28 3 4 14 islsati ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ) → ∃ 𝑧 ∈ 𝑉 𝑝 = ( 𝑁 ‘ { 𝑧 } ) )
29 26 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ∧ ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) ) → ∃ 𝑧 ∈ 𝑉 𝑝 = ( 𝑁 ‘ { 𝑧 } ) )
30 simp2 ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → 𝑝 = ( 𝑁 ‘ { 𝑧 } ) )
31 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → 𝑈 ∈ LMod )
32 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
33 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → 𝑌 ∈ 𝑉 )
34 3 4 13 31 32 33 lsmpr ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) )
35 34 oveq1d ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) = ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) )
36 prssi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
37 6 7 36 syl2anc ⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ 𝑉 )
38 37 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
39 8 snssd ⊢ ( 𝜑 → { 𝑍 } ⊆ 𝑉 )
40 39 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → { 𝑍 } ⊆ 𝑉 )
41 3 4 13 lsmsp2 ⊢ ( ( 𝑈 ∈ LMod ∧ { 𝑋 , 𝑌 } ⊆ 𝑉 ∧ { 𝑍 } ⊆ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) = ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ) )
42 31 38 40 41 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) = ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ) )
43 35 42 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) = ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ) )
44 30 43 sseq12d ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → ( 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) ↔ ( 𝑁 ‘ { 𝑧 } ) ⊆ ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ) ) )
45 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
46 37 39 unssd ⊢ ( 𝜑 → ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ⊆ 𝑉 )
47 3 45 4 lspcl ⊢ ( ( 𝑈 ∈ LMod ∧ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ⊆ 𝑉 ) → ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
48 15 46 47 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
49 48 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
50 simp3 ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → 𝑧 ∈ 𝑉 )
51 3 45 4 31 49 50 lspsnel5 ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → ( 𝑧 ∈ ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ) ↔ ( 𝑁 ‘ { 𝑧 } ) ⊆ ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ) ) )
52 44 51 bitr4d ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → ( 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) ↔ 𝑧 ∈ ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ) ) )
53 df-tp ⊢ { 𝑋 , 𝑌 , 𝑍 } = ( { 𝑋 , 𝑌 } ∪ { 𝑍 } )
54 53 fveq2i ⊢ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) = ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) )
55 54 eleq2i ⊢ ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ↔ 𝑧 ∈ ( 𝑁 ‘ ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ) )
56 52 55 bitr4di ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → ( 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) ↔ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
57 56 notbid ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → ( ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
58 57 biimpd ⊢ ( ( 𝜑 ∧ 𝑝 = ( 𝑁 ‘ { 𝑧 } ) ∧ 𝑧 ∈ 𝑉 ) → ( ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
59 58 3exp ⊢ ( 𝜑 → ( 𝑝 = ( 𝑁 ‘ { 𝑧 } ) → ( 𝑧 ∈ 𝑉 → ( ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) ) ) )
60 59 com24 ⊢ ( 𝜑 → ( ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) → ( 𝑧 ∈ 𝑉 → ( 𝑝 = ( 𝑁 ‘ { 𝑧 } ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) ) ) )
61 60 a1d ⊢ ( 𝜑 → ( 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) → ( ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) → ( 𝑧 ∈ 𝑉 → ( 𝑝 = ( 𝑁 ‘ { 𝑧 } ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) ) ) ) )
62 61 3imp ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ∧ ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) ) → ( 𝑧 ∈ 𝑉 → ( 𝑝 = ( 𝑁 ‘ { 𝑧 } ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) ) )
63 62 reximdvai ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ∧ ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) ) → ( ∃ 𝑧 ∈ 𝑉 𝑝 = ( 𝑁 ‘ { 𝑧 } ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
64 29 63 mpd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ∧ ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )
65 64 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( LSAtoms ‘ 𝑈 ) ¬ 𝑝 ⊆ ( ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑍 } ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ) )
66 25 65 mpd ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) )