Metamath Proof Explorer

Theorem cdlemj1

Description: Part of proof of Lemma J of Crawley p. 118. (Contributed by NM, 19-Jun-2013)

Ref Expression
Hypotheses cdlemj.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemj.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemj.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemj.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemj.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
cdlemj.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemj.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cdlemj1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( ( 𝑈 ‘ ℎ ) ‘ 𝑝 ) = ( ( 𝑉 ‘ ℎ ) ‘ 𝑝 ) )

Proof

Step Hyp Ref Expression
1 cdlemj.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemj.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 cdlemj.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 cdlemj.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5 cdlemj.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6 cdlemj.l ⊢ ≤ = ( le ‘ 𝐾 )
7 cdlemj.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
8 simp123 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) )
9 8 fveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑝 ) = ( ( 𝑉 ‘ 𝐹 ) ‘ 𝑝 ) )
10 9 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝐹 ) ) ) = ( ( ( 𝑉 ‘ 𝐹 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝐹 ) ) ) )
11 10 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑔 ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝐹 ) ) ) ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑔 ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑉 ‘ 𝐹 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝐹 ) ) ) ) )
12 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 simp131 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → 𝐹 ∈ 𝑇 )
14 simp22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → 𝑔 ∈ 𝑇 )
15 simp121 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → 𝑈 ∈ 𝐸 )
16 simp33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) )
17 simp132 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
18 simp23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → 𝑔 ≠ ( I ↾ 𝐵 ) )
19 simp31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) )
20 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
21 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
22 eqid ⊢ ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑔 ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝐹 ) ) ) ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑔 ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝐹 ) ) ) )
23 1 6 20 21 7 2 3 4 5 22 cdlemi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ) ) → ( ( 𝑈 ‘ 𝑔 ) ‘ 𝑝 ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑔 ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝐹 ) ) ) ) )
24 12 13 14 15 16 17 18 19 23 syl323anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( ( 𝑈 ‘ 𝑔 ) ‘ 𝑝 ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑔 ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝐹 ) ) ) ) )
25 simp122 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → 𝑉 ∈ 𝐸 )
26 eqid ⊢ ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑔 ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑉 ‘ 𝐹 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝐹 ) ) ) ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑔 ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑉 ‘ 𝐹 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝐹 ) ) ) )
27 1 6 20 21 7 2 3 4 5 26 cdlemi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) ∧ ( 𝑉 ∈ 𝐸 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ) ) → ( ( 𝑉 ‘ 𝑔 ) ‘ 𝑝 ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑔 ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑉 ‘ 𝐹 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝐹 ) ) ) ) )
28 12 13 14 25 16 17 18 19 27 syl323anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( ( 𝑉 ‘ 𝑔 ) ‘ 𝑝 ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝑔 ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑉 ‘ 𝐹 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑔 ∘ ◡ 𝐹 ) ) ) ) )
29 11 24 28 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( ( 𝑈 ‘ 𝑔 ) ‘ 𝑝 ) = ( ( 𝑉 ‘ 𝑔 ) ‘ 𝑝 ) )
30 29 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( ( ( 𝑈 ‘ 𝑔 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( ℎ ∘ ◡ 𝑔 ) ) ) = ( ( ( 𝑉 ‘ 𝑔 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( ℎ ∘ ◡ 𝑔 ) ) ) )
31 30 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ ℎ ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑈 ‘ 𝑔 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( ℎ ∘ ◡ 𝑔 ) ) ) ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ ℎ ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑉 ‘ 𝑔 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( ℎ ∘ ◡ 𝑔 ) ) ) ) )
32 simp133 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ℎ ∈ 𝑇 )
33 simp21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ℎ ≠ ( I ↾ 𝐵 ) )
34 simp32 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) )
35 eqid ⊢ ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ ℎ ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑈 ‘ 𝑔 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( ℎ ∘ ◡ 𝑔 ) ) ) ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ ℎ ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑈 ‘ 𝑔 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( ℎ ∘ ◡ 𝑔 ) ) ) )
36 1 6 20 21 7 2 3 4 5 35 cdlemi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( 𝑔 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → ( ( 𝑈 ‘ ℎ ) ‘ 𝑝 ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ ℎ ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑈 ‘ 𝑔 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( ℎ ∘ ◡ 𝑔 ) ) ) ) )
37 12 14 32 15 16 18 33 34 36 syl323anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( ( 𝑈 ‘ ℎ ) ‘ 𝑝 ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ ℎ ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑈 ‘ 𝑔 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( ℎ ∘ ◡ 𝑔 ) ) ) ) )
38 eqid ⊢ ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ ℎ ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑉 ‘ 𝑔 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( ℎ ∘ ◡ 𝑔 ) ) ) ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ ℎ ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑉 ‘ 𝑔 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( ℎ ∘ ◡ 𝑔 ) ) ) )
39 1 6 20 21 7 2 3 4 5 38 cdlemi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) ∧ ( 𝑉 ∈ 𝐸 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ∧ ( 𝑔 ≠ ( I ↾ 𝐵 ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → ( ( 𝑉 ‘ ℎ ) ‘ 𝑝 ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ ℎ ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑉 ‘ 𝑔 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( ℎ ∘ ◡ 𝑔 ) ) ) ) )
40 12 14 32 25 16 18 33 34 39 syl323anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( ( 𝑉 ‘ ℎ ) ‘ 𝑝 ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑅 ‘ ℎ ) ) ( meet ‘ 𝐾 ) ( ( ( 𝑉 ‘ 𝑔 ) ‘ 𝑝 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( ℎ ∘ ◡ 𝑔 ) ) ) ) )
41 31 37 40 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) ) → ( ( 𝑈 ‘ ℎ ) ‘ 𝑝 ) = ( ( 𝑉 ‘ ℎ ) ‘ 𝑝 ) )