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

Metamath Proof Explorer

Theorem elpaddat

Description: Membership in a projective subspace sum with a point. (Contributed by NM, 29-Jan-2012)

Ref Expression
Hypotheses paddfval.l ⊢ ≤ = ( le ‘ 𝐾 )
paddfval.j ⊢ ∨ = ( join ‘ 𝐾 )
paddfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddfval.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion elpaddat ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → ( 𝑆 ∈ ( 𝑋 + { 𝑄 } ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑝 ∈ 𝑋 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) ) )

Proof

Step Hyp Ref Expression
1 paddfval.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddfval.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 paddfval.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 simpl1 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → 𝐾 ∈ Lat )
6 simpl2 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → 𝑋 ⊆ 𝐴 )
7 simpl3 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → 𝑄 ∈ 𝐴 )
8 7 snssd ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → { 𝑄 } ⊆ 𝐴 )
9 simpr ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → 𝑋 ≠ ∅ )
10 7 snn0d ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → { 𝑄 } ≠ ∅ )
11 1 2 3 4 elpaddn0 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ { 𝑄 } ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ { 𝑄 } ≠ ∅ ) ) → ( 𝑆 ∈ ( 𝑋 + { 𝑄 } ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑝 ∈ 𝑋 ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ) ) )
12 5 6 8 9 10 11 syl32anc ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → ( 𝑆 ∈ ( 𝑋 + { 𝑄 } ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑝 ∈ 𝑋 ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ) ) )
13 oveq2 ⊢ ( 𝑟 = 𝑄 → ( 𝑝 ∨ 𝑟 ) = ( 𝑝 ∨ 𝑄 ) )
14 13 breq2d ⊢ ( 𝑟 = 𝑄 → ( 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ↔ 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) )
15 14 rexsng ⊢ ( 𝑄 ∈ 𝐴 → ( ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ↔ 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) )
16 7 15 syl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ↔ 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) )
17 16 rexbidv ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑝 ∈ 𝑋 ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ↔ ∃ 𝑝 ∈ 𝑋 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) )
18 17 anbi2d ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → ( ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑝 ∈ 𝑋 ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑝 ∈ 𝑋 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) ) )
19 12 18 bitrd ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → ( 𝑆 ∈ ( 𝑋 + { 𝑄 } ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑝 ∈ 𝑋 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) ) )