Metamath Proof Explorer


Theorem cdlemg1cex

Description: Any translation is one of our F s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf ? (Contributed by NM, 17-Apr-2013)

Ref Expression
Hypotheses cdlemg1c.l = ( le ‘ 𝐾 )
cdlemg1c.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemg1c.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemg1c.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemg1cex ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝐹𝑇 ↔ ∃ 𝑝𝐴𝑞𝐴 ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemg1c.l = ( le ‘ 𝐾 )
2 cdlemg1c.a 𝐴 = ( Atoms ‘ 𝐾 )
3 cdlemg1c.h 𝐻 = ( LHyp ‘ 𝐾 )
4 cdlemg1c.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 1 2 3 4 ltrnel ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ) → ( ( 𝐹𝑝 ) ∈ 𝐴 ∧ ¬ ( 𝐹𝑝 ) 𝑊 ) )
6 5 3expa ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ) → ( ( 𝐹𝑝 ) ∈ 𝐴 ∧ ¬ ( 𝐹𝑝 ) 𝑊 ) )
7 6 simpld ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ) → ( 𝐹𝑝 ) ∈ 𝐴 )
8 simprr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ) → ¬ 𝑝 𝑊 )
9 6 simprd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ) → ¬ ( 𝐹𝑝 ) 𝑊 )
10 simpll ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
11 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ) → ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) )
12 simplr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ) → 𝐹𝑇 )
13 1 2 3 4 cdlemeiota ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ∧ 𝐹𝑇 ) → 𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = ( 𝐹𝑝 ) ) )
14 10 11 12 13 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ) → 𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = ( 𝐹𝑝 ) ) )
15 breq1 ( 𝑞 = ( 𝐹𝑝 ) → ( 𝑞 𝑊 ↔ ( 𝐹𝑝 ) 𝑊 ) )
16 15 notbid ( 𝑞 = ( 𝐹𝑝 ) → ( ¬ 𝑞 𝑊 ↔ ¬ ( 𝐹𝑝 ) 𝑊 ) )
17 eqeq2 ( 𝑞 = ( 𝐹𝑝 ) → ( ( 𝑓𝑝 ) = 𝑞 ↔ ( 𝑓𝑝 ) = ( 𝐹𝑝 ) ) )
18 17 riotabidv ( 𝑞 = ( 𝐹𝑝 ) → ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) = ( 𝑓𝑇 ( 𝑓𝑝 ) = ( 𝐹𝑝 ) ) )
19 18 eqeq2d ( 𝑞 = ( 𝐹𝑝 ) → ( 𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ↔ 𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = ( 𝐹𝑝 ) ) ) )
20 16 19 3anbi23d ( 𝑞 = ( 𝐹𝑝 ) → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ↔ ( ¬ 𝑝 𝑊 ∧ ¬ ( 𝐹𝑝 ) 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = ( 𝐹𝑝 ) ) ) ) )
21 20 rspcev ( ( ( 𝐹𝑝 ) ∈ 𝐴 ∧ ( ¬ 𝑝 𝑊 ∧ ¬ ( 𝐹𝑝 ) 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = ( 𝐹𝑝 ) ) ) ) → ∃ 𝑞𝐴 ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) )
22 7 8 9 14 21 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ) → ∃ 𝑞𝐴 ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) )
23 1 2 3 lhpexnle ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 ¬ 𝑝 𝑊 )
24 23 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ∃ 𝑝𝐴 ¬ 𝑝 𝑊 )
25 22 24 reximddv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ∃ 𝑝𝐴𝑞𝐴 ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) )
26 25 ex ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝐹𝑇 → ∃ 𝑝𝐴𝑞𝐴 ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ) )
27 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑞𝐴 ) ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
28 simp2l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑞𝐴 ) ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ) → 𝑝𝐴 )
29 simp31 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑞𝐴 ) ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ) → ¬ 𝑝 𝑊 )
30 28 29 jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑞𝐴 ) ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ) → ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) )
31 simp2r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑞𝐴 ) ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ) → 𝑞𝐴 )
32 simp32 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑞𝐴 ) ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ) → ¬ 𝑞 𝑊 )
33 31 32 jca ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑞𝐴 ) ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ) → ( 𝑞𝐴 ∧ ¬ 𝑞 𝑊 ) )
34 simp33 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑞𝐴 ) ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ) → 𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) )
35 1 2 3 4 cdlemg1ci2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 𝑊 ) ∧ ( 𝑞𝐴 ∧ ¬ 𝑞 𝑊 ) ) ∧ 𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) → 𝐹𝑇 )
36 27 30 33 34 35 syl31anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑝𝐴𝑞𝐴 ) ∧ ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ) → 𝐹𝑇 )
37 36 3exp ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( 𝑝𝐴𝑞𝐴 ) → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) → 𝐹𝑇 ) ) )
38 37 rexlimdvv ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ∃ 𝑝𝐴𝑞𝐴 ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) → 𝐹𝑇 ) )
39 26 38 impbid ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝐹𝑇 ↔ ∃ 𝑝𝐴𝑞𝐴 ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊𝐹 = ( 𝑓𝑇 ( 𝑓𝑝 ) = 𝑞 ) ) ) )