Metamath Proof Explorer


Theorem isleagd

Description: Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020)

Ref Expression
Hypotheses isleag.p P = Base G
isleag.g φ G 𝒢 Tarski
isleag.a φ A P
isleag.b φ B P
isleag.c φ C P
isleag.d φ D P
isleag.e φ E P
isleag.f φ F P
isleagd.s ˙ = 𝒢 G
isleagd.x φ X P
isleagd.1 φ X 𝒢 G ⟨“ DEF ”⟩
isleagd.2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEX ”⟩
Assertion isleagd φ ⟨“ ABC ”⟩ ˙ ⟨“ DEF ”⟩

Proof

Step Hyp Ref Expression
1 isleag.p P = Base G
2 isleag.g φ G 𝒢 Tarski
3 isleag.a φ A P
4 isleag.b φ B P
5 isleag.c φ C P
6 isleag.d φ D P
7 isleag.e φ E P
8 isleag.f φ F P
9 isleagd.s ˙ = 𝒢 G
10 isleagd.x φ X P
11 isleagd.1 φ X 𝒢 G ⟨“ DEF ”⟩
12 isleagd.2 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEX ”⟩
13 9 eqcomi 𝒢 G = ˙
14 13 a1i φ 𝒢 G = ˙
15 simpr φ x = X x = X
16 15 breq1d φ x = X x 𝒢 G ⟨“ DEF ”⟩ X 𝒢 G ⟨“ DEF ”⟩
17 eqidd φ x = X D = D
18 eqidd φ x = X E = E
19 17 18 15 s3eqd φ x = X ⟨“ DEx ”⟩ = ⟨“ DEX ”⟩
20 19 breq2d φ x = X ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEX ”⟩
21 16 20 anbi12d φ x = X x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩ X 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEX ”⟩
22 11 12 jca φ X 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEX ”⟩
23 10 21 22 rspcedvd φ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩
24 1 2 3 4 5 6 7 8 isleag φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩
25 23 24 mpbird φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
26 14 25 breqdi φ ⟨“ ABC ”⟩ ˙ ⟨“ DEF ”⟩