This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem djhcvat42

Description: A covering property. ( cvrat42 analog.) (Contributed by NM, 17-Aug-2014)

Ref Expression
Hypotheses djhcvat42.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
djhcvat42.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
djhcvat42.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
djhcvat42.o ⊢ 0 = ( 0g ‘ 𝑈 )
djhcvat42.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
djhcvat42.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
djhcvat42.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
djhcvat42.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
djhcvat42.s ⊢ ( 𝜑 → 𝑆 ∈ ran 𝐼 )
djhcvat42.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
djhcvat42.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion djhcvat42 ( 𝜑 → ( ( 𝑆 ≠ { 0 } ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑆 ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) → ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝑁 ‘ { 𝑧 } ) ⊆ 𝑆 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑧 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 djhcvat42.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 djhcvat42.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 djhcvat42.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 djhcvat42.o ⊢ 0 = ( 0g ‘ 𝑈 )
5 djhcvat42.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6 djhcvat42.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
7 djhcvat42.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
8 djhcvat42.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 djhcvat42.s ⊢ ( 𝜑 → 𝑆 ∈ ran 𝐼 )
10 djhcvat42.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
11 djhcvat42.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
12 8 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
13 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 1 6 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
15 8 9 14 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
16 10 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
17 eldifsni ⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → 𝑋 ≠ 0 )
18 10 17 syl ⊢ ( 𝜑 → 𝑋 ≠ 0 )
19 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
20 19 1 2 3 4 5 6 dihlspsnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Atoms ‘ 𝐾 ) )
21 8 16 18 20 syl3anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Atoms ‘ 𝐾 ) )
22 11 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
23 eldifsni ⊢ ( 𝑌 ∈ ( 𝑉 ∖ { 0 } ) → 𝑌 ≠ 0 )
24 11 23 syl ⊢ ( 𝜑 → 𝑌 ≠ 0 )
25 19 1 2 3 4 5 6 dihlspsnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝑉 ∧ 𝑌 ≠ 0 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( Atoms ‘ 𝐾 ) )
26 8 22 24 25 syl3anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( Atoms ‘ 𝐾 ) )
27 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
28 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
29 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
30 13 27 28 29 19 cvrat42 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ◡ 𝐼 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( ( ◡ 𝐼 ‘ 𝑆 ) ≠ ( 0. ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ) )
31 12 15 21 26 30 syl13anc ⊢ ( 𝜑 → ( ( ( ◡ 𝐼 ‘ 𝑆 ) ≠ ( 0. ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ) )
32 1 29 6 2 3 4 5 8 9 dih0sb ⊢ ( 𝜑 → ( 𝑆 = { 0 } ↔ ( ◡ 𝐼 ‘ 𝑆 ) = ( 0. ‘ 𝐾 ) ) )
33 32 necon3bid ⊢ ( 𝜑 → ( 𝑆 ≠ { 0 } ↔ ( ◡ 𝐼 ‘ 𝑆 ) ≠ ( 0. ‘ 𝐾 ) ) )
34 1 2 3 5 6 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
35 8 16 34 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
36 1 2 6 3 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ ran 𝐼 ) → 𝑆 ⊆ 𝑉 )
37 8 9 36 syl2anc ⊢ ( 𝜑 → 𝑆 ⊆ 𝑉 )
38 1 2 3 5 6 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ran 𝐼 )
39 8 22 38 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ran 𝐼 )
40 1 2 6 3 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ran 𝐼 ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ 𝑉 )
41 8 39 40 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ⊆ 𝑉 )
42 1 6 2 3 7 djhcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ⊆ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 } ) ⊆ 𝑉 ) ) → ( 𝑆 ∨ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ran 𝐼 )
43 8 37 41 42 syl12anc ⊢ ( 𝜑 → ( 𝑆 ∨ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ran 𝐼 )
44 27 1 6 8 35 43 dihcnvord ⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑆 ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑆 ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) )
45 28 1 6 7 8 9 39 djhj ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑆 ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) = ( ( ◡ 𝐼 ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) )
46 45 breq2d ⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑆 ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) )
47 44 46 bitr3d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑆 ∨ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) )
48 33 47 anbi12d ⊢ ( 𝜑 → ( ( 𝑆 ≠ { 0 } ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑆 ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ( ( ◡ 𝐼 ‘ 𝑆 ) ≠ ( 0. ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ 𝑆 ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ) )
49 8 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
50 eldifi ⊢ ( 𝑧 ∈ ( 𝑉 ∖ { 0 } ) → 𝑧 ∈ 𝑉 )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑧 ∈ 𝑉 )
52 eldifsni ⊢ ( 𝑧 ∈ ( 𝑉 ∖ { 0 } ) → 𝑧 ≠ 0 )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑧 ≠ 0 )
54 19 1 2 3 4 5 6 dihlspsnat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝑉 ∧ 𝑧 ≠ 0 ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ∈ ( Atoms ‘ 𝐾 ) )
55 49 51 53 54 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ∈ ( Atoms ‘ 𝐾 ) )
56 19 1 2 3 4 5 6 8 dihatexv2 ⊢ ( 𝜑 → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ↔ ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) 𝑟 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ) )
57 breq1 ⊢ ( 𝑟 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ↔ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ) )
58 oveq1 ⊢ ( 𝑟 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) → ( 𝑟 ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) = ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) )
59 58 breq2d ⊢ ( 𝑟 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) → ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) )
60 57 59 anbi12d ⊢ ( 𝑟 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ↔ ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ) )
61 60 adantl ⊢ ( ( 𝜑 ∧ 𝑟 = ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ↔ ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ) )
62 55 56 61 rexxfr2d ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ↔ ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ) )
63 1 2 3 5 6 dihlsprn ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑧 } ) ∈ ran 𝐼 )
64 49 51 63 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑁 ‘ { 𝑧 } ) ∈ ran 𝐼 )
65 9 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑆 ∈ ran 𝐼 )
66 27 1 6 49 64 65 dihcnvord ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ↔ ( 𝑁 ‘ { 𝑧 } ) ⊆ 𝑆 ) )
67 39 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ran 𝐼 )
68 28 1 6 7 49 64 67 djhj ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ◡ 𝐼 ‘ ( ( 𝑁 ‘ { 𝑧 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) = ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) )
69 68 breq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( ( 𝑁 ‘ { 𝑧 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) )
70 16 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑋 ∈ 𝑉 )
71 49 70 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 )
72 1 2 6 3 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑧 } ) ∈ ran 𝐼 ) → ( 𝑁 ‘ { 𝑧 } ) ⊆ 𝑉 )
73 49 64 72 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑁 ‘ { 𝑧 } ) ⊆ 𝑉 )
74 41 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ 𝑉 )
75 1 6 2 3 7 djhcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑁 ‘ { 𝑧 } ) ⊆ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 } ) ⊆ 𝑉 ) ) → ( ( 𝑁 ‘ { 𝑧 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ran 𝐼 )
76 49 73 74 75 syl12anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝑁 ‘ { 𝑧 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ran 𝐼 )
77 27 1 6 49 71 76 dihcnvord ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( ( 𝑁 ‘ { 𝑧 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑧 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) )
78 69 77 bitr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑧 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) )
79 66 78 anbi12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ↔ ( ( 𝑁 ‘ { 𝑧 } ) ⊆ 𝑆 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑧 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) ) )
80 79 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑧 } ) ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ↔ ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝑁 ‘ { 𝑧 } ) ⊆ 𝑆 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑧 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) ) )
81 62 80 bitr2d ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝑁 ‘ { 𝑧 } ) ⊆ 𝑆 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑧 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( ◡ 𝐼 ‘ 𝑆 ) ∧ ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑋 } ) ) ( le ‘ 𝐾 ) ( 𝑟 ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ ( 𝑁 ‘ { 𝑌 } ) ) ) ) ) )
82 31 48 81 3imtr4d ⊢ ( 𝜑 → ( ( 𝑆 ≠ { 0 } ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑆 ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) → ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝑁 ‘ { 𝑧 } ) ⊆ 𝑆 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑧 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) ) )