Metamath Proof Explorer

Theorem cdlemj3

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

Ref Expression
Hypotheses cdlemj.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemj.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemj.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemj.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemj.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemj3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( 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 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
8 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
9 7 8 2 lhpexle2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) )
10 6 9 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) → ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) )
11 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) → 𝐾 ∈ HL )
12 11 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ) → 𝐾 ∈ HL )
13 simpl1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) → 𝑊 ∈ 𝐻 )
14 13 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ) → 𝑊 ∈ 𝐻 )
15 simprl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ) → 𝑢 ∈ ( Atoms ‘ 𝐾 ) )
16 simprr1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ) → 𝑢 ( le ‘ 𝐾 ) 𝑊 )
17 1 7 8 2 3 4 cdlemfnid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ( le ‘ 𝐾 ) 𝑊 ) ) → ∃ 𝑔 ∈ 𝑇 ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) )
18 12 14 15 16 17 syl22anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ) → ∃ 𝑔 ∈ 𝑇 ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) )
19 simp1l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) )
20 simp1r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) ) → ℎ ≠ ( I ↾ 𝐵 ) )
21 simp3l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) ) → 𝑔 ∈ 𝑇 )
22 simp3rr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) ) → 𝑔 ≠ ( I ↾ 𝐵 ) )
23 simp2r2 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) ) → 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) )
24 23 necomd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ 𝑢 )
25 simp3rl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) ) → ( 𝑅 ‘ 𝑔 ) = 𝑢 )
26 24 25 neeqtrrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) )
27 simp2r3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) ) → 𝑢 ≠ ( 𝑅 ‘ ℎ ) )
28 25 27 eqnetrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) ) → ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) )
29 1 2 3 4 5 cdlemj2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ( ℎ ≠ ( I ↾ 𝐵 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝑔 ) ∧ ( 𝑅 ‘ 𝑔 ) ≠ ( 𝑅 ‘ ℎ ) ) ) → ( 𝑈 ‘ ℎ ) = ( 𝑉 ‘ ℎ ) )
30 19 20 21 22 26 28 29 syl132anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) ) → ( 𝑈 ‘ ℎ ) = ( 𝑉 ‘ ℎ ) )
31 30 3expia ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ) → ( ( 𝑔 ∈ 𝑇 ∧ ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑈 ‘ ℎ ) = ( 𝑉 ‘ ℎ ) ) )
32 31 expd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ) → ( 𝑔 ∈ 𝑇 → ( ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) → ( 𝑈 ‘ ℎ ) = ( 𝑉 ‘ ℎ ) ) ) )
33 32 rexlimdv ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ) → ( ∃ 𝑔 ∈ 𝑇 ( ( 𝑅 ‘ 𝑔 ) = 𝑢 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) → ( 𝑈 ‘ ℎ ) = ( 𝑉 ‘ ℎ ) ) )
34 18 33 mpd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑢 ( le ‘ 𝐾 ) 𝑊 ∧ 𝑢 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑢 ≠ ( 𝑅 ‘ ℎ ) ) ) ) → ( 𝑈 ‘ ℎ ) = ( 𝑉 ‘ ℎ ) )
35 10 34 rexlimddv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑈 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐹 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ℎ ∈ 𝑇 ) ) ∧ ℎ ≠ ( I ↾ 𝐵 ) ) → ( 𝑈 ‘ ℎ ) = ( 𝑉 ‘ ℎ ) )