Metamath Proof Explorer


Theorem isleag

Description: Geometrical "less than" property for angles. Definition 11.27 of Schwabhauser p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020)

Ref Expression
Hypotheses isleag.p P=BaseG
isleag.g φG𝒢Tarski
isleag.a φAP
isleag.b φBP
isleag.c φCP
isleag.d φDP
isleag.e φEP
isleag.f φFP
Assertion isleag φ⟨“ABC”⟩𝒢G⟨“DEF”⟩xPx𝒢G⟨“DEF”⟩⟨“ABC”⟩𝒢G⟨“DEx”⟩

Proof

Step Hyp Ref Expression
1 isleag.p P=BaseG
2 isleag.g φG𝒢Tarski
3 isleag.a φAP
4 isleag.b φBP
5 isleag.c φCP
6 isleag.d φDP
7 isleag.e φEP
8 isleag.f φFP
9 3 4 5 s3cld φ⟨“ABC”⟩WordP
10 s3len ⟨“ABC”⟩=3
11 1 fvexi PV
12 3nn0 30
13 wrdmap PV30⟨“ABC”⟩WordP⟨“ABC”⟩=3⟨“ABC”⟩P0..^3
14 11 12 13 mp2an ⟨“ABC”⟩WordP⟨“ABC”⟩=3⟨“ABC”⟩P0..^3
15 9 10 14 sylanblc φ⟨“ABC”⟩P0..^3
16 6 7 8 s3cld φ⟨“DEF”⟩WordP
17 s3len ⟨“DEF”⟩=3
18 wrdmap PV30⟨“DEF”⟩WordP⟨“DEF”⟩=3⟨“DEF”⟩P0..^3
19 11 12 18 mp2an ⟨“DEF”⟩WordP⟨“DEF”⟩=3⟨“DEF”⟩P0..^3
20 16 17 19 sylanblc φ⟨“DEF”⟩P0..^3
21 15 20 jca φ⟨“ABC”⟩P0..^3⟨“DEF”⟩P0..^3
22 elex G𝒢TarskiGV
23 fveq2 g=GBaseg=BaseG
24 23 1 eqtr4di g=GBaseg=P
25 24 oveq1d g=GBaseg0..^3=P0..^3
26 25 eleq2d g=GaBaseg0..^3aP0..^3
27 25 eleq2d g=GbBaseg0..^3bP0..^3
28 26 27 anbi12d g=GaBaseg0..^3bBaseg0..^3aP0..^3bP0..^3
29 fveq2 g=G𝒢g=𝒢G
30 29 breqd g=Gx𝒢g⟨“b0b1b2”⟩x𝒢G⟨“b0b1b2”⟩
31 fveq2 g=G𝒢g=𝒢G
32 31 breqd g=G⟨“a0a1a2”⟩𝒢g⟨“b0b1x”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩
33 30 32 anbi12d g=Gx𝒢g⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢g⟨“b0b1x”⟩x𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩
34 24 33 rexeqbidv g=GxBasegx𝒢g⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢g⟨“b0b1x”⟩xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩
35 28 34 anbi12d g=GaBaseg0..^3bBaseg0..^3xBasegx𝒢g⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢g⟨“b0b1x”⟩aP0..^3bP0..^3xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩
36 35 opabbidv g=Gab|aBaseg0..^3bBaseg0..^3xBasegx𝒢g⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢g⟨“b0b1x”⟩=ab|aP0..^3bP0..^3xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩
37 df-leag 𝒢=gVab|aBaseg0..^3bBaseg0..^3xBasegx𝒢g⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢g⟨“b0b1x”⟩
38 ovex P0..^3V
39 38 38 xpex P0..^3×P0..^3V
40 opabssxp ab|aP0..^3bP0..^3xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩P0..^3×P0..^3
41 39 40 ssexi ab|aP0..^3bP0..^3xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩V
42 36 37 41 fvmpt GV𝒢G=ab|aP0..^3bP0..^3xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩
43 2 22 42 3syl φ𝒢G=ab|aP0..^3bP0..^3xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩
44 43 breqd φ⟨“ABC”⟩𝒢G⟨“DEF”⟩⟨“ABC”⟩ab|aP0..^3bP0..^3xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩⟨“DEF”⟩
45 simpr a=⟨“ABC”⟩b=⟨“DEF”⟩b=⟨“DEF”⟩
46 45 fveq1d a=⟨“ABC”⟩b=⟨“DEF”⟩b0=⟨“DEF”⟩0
47 45 fveq1d a=⟨“ABC”⟩b=⟨“DEF”⟩b1=⟨“DEF”⟩1
48 45 fveq1d a=⟨“ABC”⟩b=⟨“DEF”⟩b2=⟨“DEF”⟩2
49 46 47 48 s3eqd a=⟨“ABC”⟩b=⟨“DEF”⟩⟨“b0b1b2”⟩=⟨“⟨“DEF”⟩0⟨“DEF”⟩1⟨“DEF”⟩2”⟩
50 49 breq2d a=⟨“ABC”⟩b=⟨“DEF”⟩x𝒢G⟨“b0b1b2”⟩x𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1⟨“DEF”⟩2”⟩
51 simpl a=⟨“ABC”⟩b=⟨“DEF”⟩a=⟨“ABC”⟩
52 51 fveq1d a=⟨“ABC”⟩b=⟨“DEF”⟩a0=⟨“ABC”⟩0
53 51 fveq1d a=⟨“ABC”⟩b=⟨“DEF”⟩a1=⟨“ABC”⟩1
54 51 fveq1d a=⟨“ABC”⟩b=⟨“DEF”⟩a2=⟨“ABC”⟩2
55 52 53 54 s3eqd a=⟨“ABC”⟩b=⟨“DEF”⟩⟨“a0a1a2”⟩=⟨“⟨“ABC”⟩0⟨“ABC”⟩1⟨“ABC”⟩2”⟩
56 eqidd a=⟨“ABC”⟩b=⟨“DEF”⟩x=x
57 46 47 56 s3eqd a=⟨“ABC”⟩b=⟨“DEF”⟩⟨“b0b1x”⟩=⟨“⟨“DEF”⟩0⟨“DEF”⟩1x”⟩
58 55 57 breq12d a=⟨“ABC”⟩b=⟨“DEF”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩⟨“⟨“ABC”⟩0⟨“ABC”⟩1⟨“ABC”⟩2”⟩𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1x”⟩
59 50 58 anbi12d a=⟨“ABC”⟩b=⟨“DEF”⟩x𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩x𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1⟨“DEF”⟩2”⟩⟨“⟨“ABC”⟩0⟨“ABC”⟩1⟨“ABC”⟩2”⟩𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1x”⟩
60 59 rexbidv a=⟨“ABC”⟩b=⟨“DEF”⟩xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩xPx𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1⟨“DEF”⟩2”⟩⟨“⟨“ABC”⟩0⟨“ABC”⟩1⟨“ABC”⟩2”⟩𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1x”⟩
61 eqid ab|aP0..^3bP0..^3xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩=ab|aP0..^3bP0..^3xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩
62 60 61 brab2a ⟨“ABC”⟩ab|aP0..^3bP0..^3xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩⟨“DEF”⟩⟨“ABC”⟩P0..^3⟨“DEF”⟩P0..^3xPx𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1⟨“DEF”⟩2”⟩⟨“⟨“ABC”⟩0⟨“ABC”⟩1⟨“ABC”⟩2”⟩𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1x”⟩
63 62 a1i φ⟨“ABC”⟩ab|aP0..^3bP0..^3xPx𝒢G⟨“b0b1b2”⟩⟨“a0a1a2”⟩𝒢G⟨“b0b1x”⟩⟨“DEF”⟩⟨“ABC”⟩P0..^3⟨“DEF”⟩P0..^3xPx𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1⟨“DEF”⟩2”⟩⟨“⟨“ABC”⟩0⟨“ABC”⟩1⟨“ABC”⟩2”⟩𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1x”⟩
64 s3fv0 DP⟨“DEF”⟩0=D
65 6 64 syl φ⟨“DEF”⟩0=D
66 s3fv1 EP⟨“DEF”⟩1=E
67 7 66 syl φ⟨“DEF”⟩1=E
68 s3fv2 FP⟨“DEF”⟩2=F
69 8 68 syl φ⟨“DEF”⟩2=F
70 65 67 69 s3eqd φ⟨“⟨“DEF”⟩0⟨“DEF”⟩1⟨“DEF”⟩2”⟩=⟨“DEF”⟩
71 70 breq2d φx𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1⟨“DEF”⟩2”⟩x𝒢G⟨“DEF”⟩
72 s3fv0 AP⟨“ABC”⟩0=A
73 3 72 syl φ⟨“ABC”⟩0=A
74 s3fv1 BP⟨“ABC”⟩1=B
75 4 74 syl φ⟨“ABC”⟩1=B
76 s3fv2 CP⟨“ABC”⟩2=C
77 5 76 syl φ⟨“ABC”⟩2=C
78 73 75 77 s3eqd φ⟨“⟨“ABC”⟩0⟨“ABC”⟩1⟨“ABC”⟩2”⟩=⟨“ABC”⟩
79 eqidd φx=x
80 65 67 79 s3eqd φ⟨“⟨“DEF”⟩0⟨“DEF”⟩1x”⟩=⟨“DEx”⟩
81 78 80 breq12d φ⟨“⟨“ABC”⟩0⟨“ABC”⟩1⟨“ABC”⟩2”⟩𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1x”⟩⟨“ABC”⟩𝒢G⟨“DEx”⟩
82 71 81 anbi12d φx𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1⟨“DEF”⟩2”⟩⟨“⟨“ABC”⟩0⟨“ABC”⟩1⟨“ABC”⟩2”⟩𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1x”⟩x𝒢G⟨“DEF”⟩⟨“ABC”⟩𝒢G⟨“DEx”⟩
83 82 rexbidv φxPx𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1⟨“DEF”⟩2”⟩⟨“⟨“ABC”⟩0⟨“ABC”⟩1⟨“ABC”⟩2”⟩𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1x”⟩xPx𝒢G⟨“DEF”⟩⟨“ABC”⟩𝒢G⟨“DEx”⟩
84 83 anbi2d φ⟨“ABC”⟩P0..^3⟨“DEF”⟩P0..^3xPx𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1⟨“DEF”⟩2”⟩⟨“⟨“ABC”⟩0⟨“ABC”⟩1⟨“ABC”⟩2”⟩𝒢G⟨“⟨“DEF”⟩0⟨“DEF”⟩1x”⟩⟨“ABC”⟩P0..^3⟨“DEF”⟩P0..^3xPx𝒢G⟨“DEF”⟩⟨“ABC”⟩𝒢G⟨“DEx”⟩
85 44 63 84 3bitrd φ⟨“ABC”⟩𝒢G⟨“DEF”⟩⟨“ABC”⟩P0..^3⟨“DEF”⟩P0..^3xPx𝒢G⟨“DEF”⟩⟨“ABC”⟩𝒢G⟨“DEx”⟩
86 21 85 mpbirand φ⟨“ABC”⟩𝒢G⟨“DEF”⟩xPx𝒢G⟨“DEF”⟩⟨“ABC”⟩𝒢G⟨“DEx”⟩