This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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