Metamath Proof Explorer

Theorem cdlemg44b

Description: Eliminate ( FP ) =/= P , ( GP ) =/= P from cdlemg44a . (Contributed by NM, 3-Jun-2013)

Ref Expression
Hypotheses cdlemg44.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemg44.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemg44.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemg44.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemg44.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cdlemg44b ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 cdlemg44.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 cdlemg44.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 cdlemg44.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
4 cdlemg44.l ⊢ ≤ = ( le ‘ 𝐾 )
5 cdlemg44.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 simpl21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝐹 ∈ 𝑇 )
8 simpl23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
9 simpl22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝐺 ∈ 𝑇 )
10 4 5 1 2 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐺 ‘ 𝑃 ) ≤ 𝑊 ) )
11 6 9 8 10 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐺 ‘ 𝑃 ) ≤ 𝑊 ) )
12 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐹 ‘ 𝑃 ) = 𝑃 )
13 4 5 1 2 ltrnateq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐺 ‘ 𝑃 ) ≤ 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) = ( 𝐺 ‘ 𝑃 ) )
14 6 7 8 11 12 13 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) = ( 𝐺 ‘ 𝑃 ) )
15 12 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) = ( 𝐺 ‘ 𝑃 ) )
16 14 15 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) )
17 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑃 ) = 𝑃 ) → ( 𝐺 ‘ 𝑃 ) = 𝑃 )
18 17 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑃 ) = 𝑃 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) = ( 𝐹 ‘ 𝑃 ) )
19 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑃 ) = 𝑃 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
20 simpl22 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑃 ) = 𝑃 ) → 𝐺 ∈ 𝑇 )
21 simpl23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑃 ) = 𝑃 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
22 simpl21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑃 ) = 𝑃 ) → 𝐹 ∈ 𝑇 )
23 4 5 1 2 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
24 19 22 21 23 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑃 ) = 𝑃 ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
25 4 5 1 2 ltrnateq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) ) ∧ ( 𝐺 ‘ 𝑃 ) = 𝑃 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) = ( 𝐹 ‘ 𝑃 ) )
26 19 20 21 24 17 25 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑃 ) = 𝑃 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) = ( 𝐹 ‘ 𝑃 ) )
27 18 26 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑃 ) = 𝑃 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) )
28 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
29 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ) ) → ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) )
30 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ) ) → ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 )
31 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ) ) → ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 )
32 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) )
33 1 2 3 4 5 cdlemg44a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) )
34 28 29 30 31 32 33 syl113anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) )
35 16 27 34 pm2.61da2ne ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑃 ) ) )