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 φKHLCBaseKPAQARASATAUAYOZO¬C˙P˙Q¬C˙Q˙R¬C˙R˙P¬C˙S˙T¬C˙T˙U¬C˙U˙SC˙P˙SC˙Q˙TC˙R˙U
dalemc.l ˙=K
dalemc.j ˙=joinK
dalemc.a A=AtomsK
dalemrot.y Y=P˙Q˙R
dalemrot.z Z=S˙T˙U
Assertion dalemrotyz φY=ZQ˙R˙P=T˙U˙S

Proof

Step Hyp Ref Expression
1 dalema.ph φKHLCBaseKPAQARASATAUAYOZO¬C˙P˙Q¬C˙Q˙R¬C˙R˙P¬C˙S˙T¬C˙T˙U¬C˙U˙SC˙P˙SC˙Q˙TC˙R˙U
2 dalemc.l ˙=K
3 dalemc.j ˙=joinK
4 dalemc.a A=AtomsK
5 dalemrot.y Y=P˙Q˙R
6 dalemrot.z Z=S˙T˙U
7 simpr φY=ZY=Z
8 1 3 4 dalemqrprot φQ˙R˙P=P˙Q˙R
9 5 8 eqtr4id φY=Q˙R˙P
10 9 adantr φY=ZY=Q˙R˙P
11 1 dalemkehl φKHL
12 1 dalemtea φTA
13 1 dalemuea φUA
14 1 dalemsea φSA
15 3 4 hlatjrot KHLTAUASAT˙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=ZZ=T˙U˙S
19 7 10 18 3eqtr3d φY=ZQ˙R˙P=T˙U˙S