Metamath Proof Explorer


Theorem cdlemg48

Description: Eliminate h from cdlemg47 . (Contributed by NM, 5-Jun-2013)

Ref Expression
Hypotheses cdlemg46.b 𝐵 = ( Base ‘ 𝐾 )
cdlemg46.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemg46.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemg46.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemg48 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) → ( 𝐹𝐺 ) = ( 𝐺𝐹 ) )

Proof

Step Hyp Ref Expression
1 cdlemg46.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemg46.h 𝐻 = ( LHyp ‘ 𝐾 )
3 cdlemg46.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 cdlemg46.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5 1 2 3 4 cdlemftr1 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑇 ( ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) )
6 5 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) → ∃ 𝑇 ( ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) )
7 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) ∧ 𝑇 ∧ ( ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
8 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) ∧ 𝑇 ∧ ( ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) ) → 𝐹𝑇 )
9 simp12r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) ∧ 𝑇 ∧ ( ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) ) → 𝐺𝑇 )
10 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) ∧ 𝑇 ∧ ( ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) ) → 𝑇 )
11 simp13r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) ∧ 𝑇 ∧ ( ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) ) → ( 𝑅𝐹 ) = ( 𝑅𝐺 ) )
12 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) ∧ 𝑇 ∧ ( ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
13 simp3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) ∧ 𝑇 ∧ ( ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) ) → ≠ ( I ↾ 𝐵 ) )
14 simp3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) ∧ 𝑇 ∧ ( ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) ) → ( 𝑅 ) ≠ ( 𝑅𝐹 ) )
15 1 2 3 4 cdlemg47 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐺𝑇 ) ∧ ( 𝑇 ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) ) → ( 𝐹𝐺 ) = ( 𝐺𝐹 ) )
16 7 8 9 10 11 12 13 14 15 syl323anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) ∧ 𝑇 ∧ ( ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) ) → ( 𝐹𝐺 ) = ( 𝐺𝐹 ) )
17 16 rexlimdv3a ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) → ( ∃ 𝑇 ( ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ) ≠ ( 𝑅𝐹 ) ) → ( 𝐹𝐺 ) = ( 𝐺𝐹 ) ) )
18 6 17 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝐺 ) ) ) → ( 𝐹𝐺 ) = ( 𝐺𝐹 ) )