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

Metamath Proof Explorer

Theorem linepsubN

Description: A line is a projective subspace. (Contributed by NM, 16-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses linepsub.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
linepsub.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
Assertion linepsubN ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝑁 ) → 𝑋 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 linepsub.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
2 linepsub.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
3 ssrab2 ⊢ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ⊆ ( Atoms ‘ 𝐾 )
4 sseq1 ⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ↔ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ⊆ ( Atoms ‘ 𝐾 ) ) )
5 3 4 mpbiri ⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
6 5 a1i ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
9 7 8 atbase ⊢ ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) → 𝑎 ∈ ( Base ‘ 𝐾 ) )
10 7 8 atbase ⊢ ( 𝑏 ∈ ( Atoms ‘ 𝐾 ) → 𝑏 ∈ ( Base ‘ 𝐾 ) )
11 9 10 anim12i ⊢ ( ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑎 ∈ ( Base ‘ 𝐾 ) ∧ 𝑏 ∈ ( Base ‘ 𝐾 ) ) )
12 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
13 7 12 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑎 ∈ ( Base ‘ 𝐾 ) ∧ 𝑏 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) )
14 13 3expb ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ∈ ( Base ‘ 𝐾 ) ∧ 𝑏 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) )
15 11 14 sylan2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) )
16 eleq2 ⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑝 ∈ 𝑋 ↔ 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) )
17 breq1 ⊢ ( 𝑐 = 𝑝 → ( 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ↔ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
18 17 elrab ⊢ ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ↔ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
19 7 8 atbase ⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
20 19 anim1i ⊢ ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
21 18 20 sylbi ⊢ ( 𝑝 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
22 16 21 biimtrdi ⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑝 ∈ 𝑋 → ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) )
23 eleq2 ⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑞 ∈ 𝑋 ↔ 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) )
24 breq1 ⊢ ( 𝑐 = 𝑞 → ( 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ↔ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
25 24 elrab ⊢ ( 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ↔ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
26 7 8 atbase ⊢ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) → 𝑞 ∈ ( Base ‘ 𝐾 ) )
27 26 anim1i ⊢ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
28 25 27 sylbi ⊢ ( 𝑞 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
29 23 28 biimtrdi ⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑞 ∈ 𝑋 → ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) )
30 22 29 anim12d ⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ∧ ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) )
31 an4 ⊢ ( ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ∧ ( 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ↔ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) )
32 30 31 imbitrdi ⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) )
33 32 imp ⊢ ( ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) )
34 33 anim2i ⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) ) → ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) )
35 34 anassrs ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) )
36 7 8 atbase ⊢ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
37 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
38 7 37 12 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ↔ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
39 38 biimpd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
40 39 3exp2 ⊢ ( 𝐾 ∈ Lat → ( 𝑝 ∈ ( Base ‘ 𝐾 ) → ( 𝑞 ∈ ( Base ‘ 𝐾 ) → ( ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) )
41 40 impd ⊢ ( 𝐾 ∈ Lat → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) )
42 41 com23 ⊢ ( 𝐾 ∈ Lat → ( ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) )
43 42 imp43 ⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) )
44 43 adantr ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) )
45 7 12 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
46 45 3expib ⊢ ( 𝐾 ∈ Lat → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ) )
47 7 37 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑟 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
48 47 3exp2 ⊢ ( 𝐾 ∈ Lat → ( 𝑟 ∈ ( Base ‘ 𝐾 ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) )
49 48 com24 ⊢ ( 𝐾 ∈ Lat → ( ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) → ( 𝑟 ∈ ( Base ‘ 𝐾 ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) )
50 46 49 syl5d ⊢ ( 𝐾 ∈ Lat → ( ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) → ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑟 ∈ ( Base ‘ 𝐾 ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ) )
51 50 imp41 ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
52 51 adantlrr ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
53 44 52 mpan2d ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑝 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑝 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∧ 𝑞 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
54 35 36 53 syl2an ⊢ ( ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
55 simpr ⊢ ( ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
56 54 55 jctild ⊢ ( ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) )
57 eleq2 ⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑟 ∈ 𝑋 ↔ 𝑟 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) )
58 breq1 ⊢ ( 𝑐 = 𝑟 → ( 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ↔ 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
59 58 elrab ⊢ ( 𝑟 ∈ { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ↔ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) )
60 57 59 bitrdi ⊢ ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑟 ∈ 𝑋 ↔ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) )
61 60 ad3antlr ⊢ ( ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑟 ∈ 𝑋 ↔ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ) ) )
62 56 61 sylibrd ⊢ ( ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) )
63 62 ralrimiva ⊢ ( ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ∧ ( 𝑝 ∈ 𝑋 ∧ 𝑞 ∈ 𝑋 ) ) → ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) )
64 63 ralrimivva ⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) → ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) )
65 64 ex ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) )
66 15 65 syldan ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) )
67 6 66 jcad ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) )
68 67 adantld ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) )
69 68 rexlimdvva ⊢ ( 𝐾 ∈ Lat → ( ∃ 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ( 𝑎 ≠ 𝑏 ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) )
70 37 12 8 1 isline ⊢ ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑎 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑏 ∈ ( Atoms ‘ 𝐾 ) ( 𝑎 ≠ 𝑏 ∧ 𝑋 = { 𝑐 ∈ ( Atoms ‘ 𝐾 ) ∣ 𝑐 ( le ‘ 𝐾 ) ( 𝑎 ( join ‘ 𝐾 ) 𝑏 ) } ) ) )
71 37 12 8 2 ispsubsp ⊢ ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) )
72 69 70 71 3imtr4d ⊢ ( 𝐾 ∈ Lat → ( 𝑋 ∈ 𝑁 → 𝑋 ∈ 𝑆 ) )
73 72 imp ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝑁 ) → 𝑋 ∈ 𝑆 )