Metamath Proof Explorer

Theorem ltrniotavalbN

Description: Value of the unique translation specified by a value. (Contributed by NM, 10-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses ltrniotavalb.l ⊢ ≤ = ( le ‘ 𝐾 )
ltrniotavalb.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
ltrniotavalb.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
ltrniotavalb.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrniotavalbN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑃 ) = 𝑄 ↔ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 ltrniotavalb.l ⊢ ≤ = ( le ‘ 𝐾 )
2 ltrniotavalb.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 ltrniotavalb.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 ltrniotavalb.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑄 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑄 ) → 𝐹 ∈ 𝑇 )
7 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑄 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
8 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑄 ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
9 eqid ⊢ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )
10 1 2 3 4 9 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ∈ 𝑇 )
11 5 7 8 10 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑄 ) → ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ∈ 𝑇 )
12 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑄 ) → ( 𝐹 ‘ 𝑃 ) = 𝑄 )
13 1 2 3 4 9 ltrniotaval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ‘ 𝑃 ) = 𝑄 )
14 5 7 8 13 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑄 ) → ( ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ‘ 𝑃 ) = 𝑄 )
15 12 14 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑄 ) → ( 𝐹 ‘ 𝑃 ) = ( ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ‘ 𝑃 ) )
16 1 2 3 4 cdlemd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ‘ 𝑃 ) = ( ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ‘ 𝑃 ) ) → 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) )
17 5 6 11 7 15 16 syl311anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐹 ‘ 𝑃 ) = 𝑄 ) → 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) )
18 fveq1 ⊢ ( 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) → ( 𝐹 ‘ 𝑃 ) = ( ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ‘ 𝑃 ) )
19 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
20 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
21 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
22 19 20 21 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) → ( ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ‘ 𝑃 ) = 𝑄 )
23 18 22 sylan9eqr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ) → ( 𝐹 ‘ 𝑃 ) = 𝑄 )
24 17 23 impbida ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑃 ) = 𝑄 ↔ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 ) ) )