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

Metamath Proof Explorer

Theorem cdlemd2

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 29-May-2012)

Ref Expression
Hypotheses cdlemd2.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemd2.j ⊢ ∨ = ( join ‘ 𝐾 )
cdlemd2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemd2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemd2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemd2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ 𝑅 ) = ( 𝐺 ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 cdlemd2.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdlemd2.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdlemd2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 cdlemd2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 cdlemd2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) )
7 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝐹 ∈ 𝑇 )
9 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝐾 ∈ HL )
10 9 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝐾 ∈ Lat )
11 simp21l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝑃 ∈ 𝐴 )
12 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝑅 ∈ 𝐴 )
13 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
15 9 11 12 14 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
16 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝑊 ∈ 𝐻 )
17 13 4 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
18 16 17 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
19 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
20 13 19 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
21 10 15 18 20 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
22 13 1 19 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 )
23 10 15 18 22 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 )
24 13 1 4 5 ltrnval1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 ) ) → ( 𝐹 ‘ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
25 7 8 21 23 24 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
26 simp12r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝐺 ∈ 𝑇 )
27 13 1 4 5 ltrnval1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 ) ) → ( 𝐺 ‘ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
28 7 26 21 23 27 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐺 ‘ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
29 25 28 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( 𝐺 ‘ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) )
30 6 29 oveq12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐺 ‘ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
31 13 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
32 11 31 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
33 13 2 4 5 ltrnj ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐹 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
34 7 8 32 21 33 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝐹 ‘ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
35 13 2 4 5 ltrnj ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐺 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐺 ‘ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
36 7 26 32 21 35 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐺 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝐺 ‘ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
37 30 34 36 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( 𝐺 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
38 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) )
39 simp22l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝑄 ∈ 𝐴 )
40 13 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
41 9 39 12 40 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
42 13 19 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
43 10 41 18 42 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
44 13 1 19 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 )
45 10 41 18 44 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 )
46 13 1 4 5 ltrnval1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 ) ) → ( 𝐹 ‘ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
47 7 8 43 45 46 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
48 13 1 4 5 ltrnval1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ≤ 𝑊 ) ) → ( 𝐺 ‘ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
49 7 26 43 45 48 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐺 ‘ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) )
50 47 49 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) = ( 𝐺 ‘ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) )
51 38 50 oveq12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐺 ‘ 𝑄 ) ∨ ( 𝐺 ‘ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
52 13 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
53 39 52 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
54 13 2 4 5 ltrnj ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐹 ‘ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
55 7 8 53 43 54 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐹 ‘ 𝑄 ) ∨ ( 𝐹 ‘ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
56 13 2 4 5 ltrnj ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐺 ‘ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐺 ‘ 𝑄 ) ∨ ( 𝐺 ‘ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
57 7 26 53 43 56 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐺 ‘ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( ( 𝐺 ‘ 𝑄 ) ∨ ( 𝐺 ‘ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
58 51 55 57 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) = ( 𝐺 ‘ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
59 37 58 oveq12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( ( 𝐹 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ( meet ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) = ( ( 𝐺 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ( meet ‘ 𝐾 ) ( 𝐺 ‘ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
60 13 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
61 10 32 21 60 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
62 13 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
63 10 53 43 62 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) )
64 13 19 4 5 ltrnm ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ( meet ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
65 7 8 61 63 64 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ( meet ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
66 13 19 4 5 ltrnm ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐺 ‘ ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) = ( ( 𝐺 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ( meet ‘ 𝐾 ) ( 𝐺 ‘ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
67 7 26 61 63 66 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐺 ‘ ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) = ( ( 𝐺 ‘ ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ( meet ‘ 𝐾 ) ( 𝐺 ‘ ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
68 59 65 67 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) = ( 𝐺 ‘ ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
69 simp21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
70 simp22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
71 simp23l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝑃 ≠ 𝑄 )
72 simp23r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
73 12 71 72 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
74 1 2 19 3 4 cdlemd1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) → 𝑅 = ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
75 7 69 70 73 74 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → 𝑅 = ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) )
76 75 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ 𝑅 ) = ( 𝐹 ‘ ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
77 75 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐺 ‘ 𝑅 ) = ( 𝐺 ‘ ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ( meet ‘ 𝐾 ) ( 𝑄 ∨ ( ( 𝑄 ∨ 𝑅 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) )
78 68 76 77 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑃 ) ∧ ( 𝐹 ‘ 𝑄 ) = ( 𝐺 ‘ 𝑄 ) ) ) → ( 𝐹 ‘ 𝑅 ) = ( 𝐺 ‘ 𝑅 ) )