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

Metamath Proof Explorer

Theorem pclclN

Description: Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pclfval.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
pclfval.c ⊢ 𝑈 = ( PCl ‘ 𝐾 )
Assertion pclclN ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 pclfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 pclfval.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
3 pclfval.c ⊢ 𝑈 = ( PCl ‘ 𝐾 )
4 1 2 3 pclvalN ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) = ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } )
5 1 2 atpsubN ⊢ ( 𝐾 ∈ 𝑉 → 𝐴 ∈ 𝑆 )
6 sseq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑋 ⊆ 𝑦 ↔ 𝑋 ⊆ 𝐴 ) )
7 6 intminss ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑋 ⊆ 𝐴 ) → ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ⊆ 𝐴 )
8 5 7 sylan ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ⊆ 𝐴 )
9 r19.26 ⊢ ( ∀ 𝑦 ∈ 𝑆 ( ( 𝑋 ⊆ 𝑦 → 𝑝 ∈ 𝑦 ) ∧ ( 𝑋 ⊆ 𝑦 → 𝑞 ∈ 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → 𝑝 ∈ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → 𝑞 ∈ 𝑦 ) ) )
10 jcab ⊢ ( ( 𝑋 ⊆ 𝑦 → ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) ↔ ( ( 𝑋 ⊆ 𝑦 → 𝑝 ∈ 𝑦 ) ∧ ( 𝑋 ⊆ 𝑦 → 𝑞 ∈ 𝑦 ) ) )
11 10 ralbii ⊢ ( ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑆 ( ( 𝑋 ⊆ 𝑦 → 𝑝 ∈ 𝑦 ) ∧ ( 𝑋 ⊆ 𝑦 → 𝑞 ∈ 𝑦 ) ) )
12 vex ⊢ 𝑝 ∈ V
13 12 elintrab ⊢ ( 𝑝 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → 𝑝 ∈ 𝑦 ) )
14 vex ⊢ 𝑞 ∈ V
15 14 elintrab ⊢ ( 𝑞 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → 𝑞 ∈ 𝑦 ) )
16 13 15 anbi12i ⊢ ( ( 𝑝 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∧ 𝑞 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) ↔ ( ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → 𝑝 ∈ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → 𝑞 ∈ 𝑦 ) ) )
17 9 11 16 3bitr4ri ⊢ ( ( 𝑝 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∧ 𝑞 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) )
18 simpll1 ⊢ ( ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) → 𝐾 ∈ 𝑉 )
19 simplr ⊢ ( ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) → 𝑦 ∈ 𝑆 )
20 simpll3 ⊢ ( ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) → 𝑟 ∈ 𝐴 )
21 simprl ⊢ ( ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) → 𝑝 ∈ 𝑦 )
22 simprr ⊢ ( ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) → 𝑞 ∈ 𝑦 )
23 simpll2 ⊢ ( ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
24 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
25 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
26 24 25 1 2 psubspi2N ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑦 ∈ 𝑆 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) → 𝑟 ∈ 𝑦 )
27 18 19 20 21 22 23 26 syl33anc ⊢ ( ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) → 𝑟 ∈ 𝑦 )
28 27 ex ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) → 𝑟 ∈ 𝑦 ) )
29 28 imim2d ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑋 ⊆ 𝑦 → ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) → ( 𝑋 ⊆ 𝑦 → 𝑟 ∈ 𝑦 ) ) )
30 29 ralimdva ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑟 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) → ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → 𝑟 ∈ 𝑦 ) ) )
31 vex ⊢ 𝑟 ∈ V
32 31 elintrab ⊢ ( 𝑟 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → 𝑟 ∈ 𝑦 ) )
33 30 32 imbitrrdi ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑟 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) → 𝑟 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) )
34 33 3exp ⊢ ( 𝐾 ∈ 𝑉 → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → ( 𝑟 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) → 𝑟 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) ) ) )
35 34 com24 ⊢ ( 𝐾 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → ( 𝑝 ∈ 𝑦 ∧ 𝑞 ∈ 𝑦 ) ) → ( 𝑟 ∈ 𝐴 → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) ) ) )
36 17 35 biimtrid ⊢ ( 𝐾 ∈ 𝑉 → ( ( 𝑝 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∧ 𝑞 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) → ( 𝑟 ∈ 𝐴 → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) ) ) )
37 36 ralrimdv ⊢ ( 𝐾 ∈ 𝑉 → ( ( 𝑝 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∧ 𝑞 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) → ∀ 𝑟 ∈ 𝐴 ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) ) )
38 37 ralrimivv ⊢ ( 𝐾 ∈ 𝑉 → ∀ 𝑝 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∀ 𝑞 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∀ 𝑟 ∈ 𝐴 ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) )
39 38 adantr ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ∀ 𝑝 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∀ 𝑞 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∀ 𝑟 ∈ 𝐴 ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) )
40 24 25 1 2 ispsubsp ⊢ ( 𝐾 ∈ 𝑉 → ( ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∈ 𝑆 ↔ ( ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ⊆ 𝐴 ∧ ∀ 𝑝 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∀ 𝑞 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∀ 𝑟 ∈ 𝐴 ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) ) ) )
41 40 adantr ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∈ 𝑆 ↔ ( ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ⊆ 𝐴 ∧ ∀ 𝑝 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∀ 𝑞 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∀ 𝑟 ∈ 𝐴 ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) ) ) )
42 8 39 41 mpbir2and ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∈ 𝑆 )
43 4 42 eqeltrd ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) ∈ 𝑆 )