Metamath Proof Explorer


Theorem dalemrotyz

Description: Lemma for dath . Rotate triangles Y = P Q R and Z = S T U to allow reuse of analogous proofs. (Contributed by NM, 19-Aug-2012)

Ref Expression
Hypotheses dalema.ph φ K HL C Base K P A Q A R A S A T A U A Y O Z O ¬ C ˙ P ˙ Q ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ S ˙ T ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S C ˙ P ˙ S C ˙ Q ˙ T C ˙ R ˙ U
dalemc.l ˙ = K
dalemc.j ˙ = join K
dalemc.a A = Atoms K
dalemrot.y Y = P ˙ Q ˙ R
dalemrot.z Z = S ˙ T ˙ U
Assertion dalemrotyz φ Y = Z Q ˙ R ˙ P = T ˙ U ˙ S

Proof

Step Hyp Ref Expression
1 dalema.ph φ K HL C Base K P A Q A R A S A T A U A Y O Z O ¬ C ˙ P ˙ Q ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ S ˙ T ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S C ˙ P ˙ S C ˙ Q ˙ T C ˙ R ˙ U
2 dalemc.l ˙ = K
3 dalemc.j ˙ = join K
4 dalemc.a A = Atoms K
5 dalemrot.y Y = P ˙ Q ˙ R
6 dalemrot.z Z = S ˙ T ˙ U
7 simpr φ Y = Z Y = Z
8 1 3 4 dalemqrprot φ Q ˙ R ˙ P = P ˙ Q ˙ R
9 5 8 eqtr4id φ Y = Q ˙ R ˙ P
10 9 adantr φ Y = Z Y = Q ˙ R ˙ P
11 1 dalemkehl φ K HL
12 1 dalemtea φ T A
13 1 dalemuea φ U A
14 1 dalemsea φ S A
15 3 4 hlatjrot K HL T A U A S A T ˙ U ˙ S = S ˙ T ˙ U
16 11 12 13 14 15 syl13anc φ T ˙ U ˙ S = S ˙ T ˙ U
17 6 16 eqtr4id φ Z = T ˙ U ˙ S
18 17 adantr φ Y = Z Z = T ˙ U ˙ S
19 7 10 18 3eqtr3d φ Y = Z Q ˙ R ˙ P = T ˙ U ˙ S