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

Metamath Proof Explorer

Theorem atexchcvrN

Description: Atom exchange property. Version of hlatexch2 with covers relation. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses atexchcvr.j ⊢ ∨ = ( join ‘ 𝐾 )
atexchcvr.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
atexchcvr.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion atexchcvrN ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) → 𝑄 𝐶 ( 𝑃 ∨ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 atexchcvr.j ⊢ ∨ = ( join ‘ 𝐾 )
2 atexchcvr.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 atexchcvr.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝐾 ∈ HL )
5 simpl21 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ∈ 𝐴 )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 6 2 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
8 5 7 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
9 4 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝐾 ∈ Lat )
10 simpl22 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ∈ 𝐴 )
11 6 2 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
12 10 11 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
13 simpl23 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑅 ∈ 𝐴 )
14 6 2 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
16 6 1 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
17 9 12 15 16 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
18 4 8 17 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) )
19 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
20 6 19 3 cvrle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) )
21 18 20 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) )
22 21 ex ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
23 19 1 2 hlatexch2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) → 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) )
24 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝐾 ∈ HL )
25 simpl22 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝑄 ∈ 𝐴 )
26 simpl21 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝑃 ∈ 𝐴 )
27 simpl23 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝑅 ∈ 𝐴 )
28 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝑃 ≠ 𝑅 )
29 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) )
30 19 1 3 2 atcvrj2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) ) → 𝑄 𝐶 ( 𝑃 ∨ 𝑅 ) )
31 24 25 26 27 28 29 30 syl132anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝑄 𝐶 ( 𝑃 ∨ 𝑅 ) )
32 31 ex ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) → 𝑄 𝐶 ( 𝑃 ∨ 𝑅 ) ) )
33 22 23 32 3syld ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) → 𝑄 𝐶 ( 𝑃 ∨ 𝑅 ) ) )