Metamath Proof Explorer


Theorem iscgra

Description: Property for two angles ABC and DEF to be congruent. This is a modified version of the definition 11.3 of Schwabhauser p. 95. where the number of constructed points has been reduced to two. We chose this version rather than the textbook version because it is shorter and therefore simpler to work with. Theorem dfcgra2 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020)

Ref Expression
Hypotheses iscgra.p P = Base G
iscgra.i I = Itv G
iscgra.k K = hl 𝒢 G
iscgra.g φ G 𝒢 Tarski
iscgra.a φ A P
iscgra.b φ B P
iscgra.c φ C P
iscgra.d φ D P
iscgra.e φ E P
iscgra.f φ F P
Assertion iscgra φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F

Proof

Step Hyp Ref Expression
1 iscgra.p P = Base G
2 iscgra.i I = Itv G
3 iscgra.k K = hl 𝒢 G
4 iscgra.g φ G 𝒢 Tarski
5 iscgra.a φ A P
6 iscgra.b φ B P
7 iscgra.c φ C P
8 iscgra.d φ D P
9 iscgra.e φ E P
10 iscgra.f φ F P
11 simpl a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ a = ⟨“ ABC ”⟩
12 eqidd a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ x = x
13 simpr a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ b = ⟨“ DEF ”⟩
14 13 fveq1d a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ b 1 = ⟨“ DEF ”⟩ 1
15 eqidd a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ y = y
16 12 14 15 s3eqd a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ ⟨“ x b 1 y ”⟩ = ⟨“ x ⟨“ DEF ”⟩ 1 y ”⟩
17 11 16 breq12d a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ a 𝒢 G ⟨“ x b 1 y ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ x ⟨“ DEF ”⟩ 1 y ”⟩
18 14 fveq2d a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ K b 1 = K ⟨“ DEF ”⟩ 1
19 13 fveq1d a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ b 0 = ⟨“ DEF ”⟩ 0
20 12 18 19 breq123d a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ x K b 1 b 0 x K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 0
21 13 fveq1d a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ b 2 = ⟨“ DEF ”⟩ 2
22 15 18 21 breq123d a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ y K b 1 b 2 y K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 2
23 17 20 22 3anbi123d a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2 ⟨“ ABC ”⟩ 𝒢 G ⟨“ x ⟨“ DEF ”⟩ 1 y ”⟩ x K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 0 y K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 2
24 23 2rexbidv a = ⟨“ ABC ”⟩ b = ⟨“ DEF ”⟩ x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2 x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ x ⟨“ DEF ”⟩ 1 y ”⟩ x K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 0 y K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 2
25 eqid a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2 = a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
26 24 25 brab2a ⟨“ ABC ”⟩ a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2 ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ P 0 ..^ 3 ⟨“ DEF ”⟩ P 0 ..^ 3 x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ x ⟨“ DEF ”⟩ 1 y ”⟩ x K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 0 y K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 2
27 eqidd φ x P y P x = x
28 s3fv1 E P ⟨“ DEF ”⟩ 1 = E
29 9 28 syl φ ⟨“ DEF ”⟩ 1 = E
30 29 adantr φ x P y P ⟨“ DEF ”⟩ 1 = E
31 eqidd φ x P y P y = y
32 27 30 31 s3eqd φ x P y P ⟨“ x ⟨“ DEF ”⟩ 1 y ”⟩ = ⟨“ xEy ”⟩
33 32 breq2d φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ x ⟨“ DEF ”⟩ 1 y ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩
34 30 fveq2d φ x P y P K ⟨“ DEF ”⟩ 1 = K E
35 s3fv0 D P ⟨“ DEF ”⟩ 0 = D
36 8 35 syl φ ⟨“ DEF ”⟩ 0 = D
37 36 adantr φ x P y P ⟨“ DEF ”⟩ 0 = D
38 27 34 37 breq123d φ x P y P x K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 0 x K E D
39 s3fv2 F P ⟨“ DEF ”⟩ 2 = F
40 10 39 syl φ ⟨“ DEF ”⟩ 2 = F
41 40 adantr φ x P y P ⟨“ DEF ”⟩ 2 = F
42 31 34 41 breq123d φ x P y P y K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 2 y K E F
43 33 38 42 3anbi123d φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ x ⟨“ DEF ”⟩ 1 y ”⟩ x K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 0 y K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 2 ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F
44 43 2rexbidva φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ x ⟨“ DEF ”⟩ 1 y ”⟩ x K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 0 y K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 2 x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F
45 44 anbi2d φ ⟨“ ABC ”⟩ P 0 ..^ 3 ⟨“ DEF ”⟩ P 0 ..^ 3 x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ x ⟨“ DEF ”⟩ 1 y ”⟩ x K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 0 y K ⟨“ DEF ”⟩ 1 ⟨“ DEF ”⟩ 2 ⟨“ ABC ”⟩ P 0 ..^ 3 ⟨“ DEF ”⟩ P 0 ..^ 3 x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F
46 26 45 bitrid φ ⟨“ ABC ”⟩ a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2 ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ P 0 ..^ 3 ⟨“ DEF ”⟩ P 0 ..^ 3 x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F
47 elex G 𝒢 Tarski G V
48 simpl p = P k = K p = P
49 48 oveq1d p = P k = K p 0 ..^ 3 = P 0 ..^ 3
50 49 eleq2d p = P k = K a p 0 ..^ 3 a P 0 ..^ 3
51 49 eleq2d p = P k = K b p 0 ..^ 3 b P 0 ..^ 3
52 50 51 anbi12d p = P k = K a p 0 ..^ 3 b p 0 ..^ 3 a P 0 ..^ 3 b P 0 ..^ 3
53 simpr p = P k = K k = K
54 53 fveq1d p = P k = K k b 1 = K b 1
55 54 breqd p = P k = K x k b 1 b 0 x K b 1 b 0
56 54 breqd p = P k = K y k b 1 b 2 y K b 1 b 2
57 55 56 3anbi23d p = P k = K a 𝒢 g ⟨“ x b 1 y ”⟩ x k b 1 b 0 y k b 1 b 2 a 𝒢 g ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
58 48 57 rexeqbidv p = P k = K y p a 𝒢 g ⟨“ x b 1 y ”⟩ x k b 1 b 0 y k b 1 b 2 y P a 𝒢 g ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
59 48 58 rexeqbidv p = P k = K x p y p a 𝒢 g ⟨“ x b 1 y ”⟩ x k b 1 b 0 y k b 1 b 2 x P y P a 𝒢 g ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
60 52 59 anbi12d p = P k = K a p 0 ..^ 3 b p 0 ..^ 3 x p y p a 𝒢 g ⟨“ x b 1 y ”⟩ x k b 1 b 0 y k b 1 b 2 a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 g ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
61 1 3 60 sbcie2s g = G [˙Base g / p]˙ [˙ hl 𝒢 g / k]˙ a p 0 ..^ 3 b p 0 ..^ 3 x p y p a 𝒢 g ⟨“ x b 1 y ”⟩ x k b 1 b 0 y k b 1 b 2 a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 g ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
62 61 opabbidv g = G a b | [˙Base g / p]˙ [˙ hl 𝒢 g / k]˙ a p 0 ..^ 3 b p 0 ..^ 3 x p y p a 𝒢 g ⟨“ x b 1 y ”⟩ x k b 1 b 0 y k b 1 b 2 = a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 g ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
63 fveq2 g = G 𝒢 g = 𝒢 G
64 63 breqd g = G a 𝒢 g ⟨“ x b 1 y ”⟩ a 𝒢 G ⟨“ x b 1 y ”⟩
65 64 3anbi1d g = G a 𝒢 g ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2 a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
66 65 2rexbidv g = G x P y P a 𝒢 g ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
67 66 anbi2d g = G a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 g ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2 a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
68 67 opabbidv g = G a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 g ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2 = a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
69 62 68 eqtrd g = G a b | [˙Base g / p]˙ [˙ hl 𝒢 g / k]˙ a p 0 ..^ 3 b p 0 ..^ 3 x p y p a 𝒢 g ⟨“ x b 1 y ”⟩ x k b 1 b 0 y k b 1 b 2 = a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
70 df-cgra 𝒢 = g V a b | [˙Base g / p]˙ [˙ hl 𝒢 g / k]˙ a p 0 ..^ 3 b p 0 ..^ 3 x p y p a 𝒢 g ⟨“ x b 1 y ”⟩ x k b 1 b 0 y k b 1 b 2
71 ovex P 0 ..^ 3 V
72 71 71 xpex P 0 ..^ 3 × P 0 ..^ 3 V
73 opabssxp a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2 P 0 ..^ 3 × P 0 ..^ 3
74 72 73 ssexi a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2 V
75 69 70 74 fvmpt G V 𝒢 G = a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
76 4 47 75 3syl φ 𝒢 G = a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2
77 76 breqd φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ a b | a P 0 ..^ 3 b P 0 ..^ 3 x P y P a 𝒢 G ⟨“ x b 1 y ”⟩ x K b 1 b 0 y K b 1 b 2 ⟨“ DEF ”⟩
78 5 6 7 s3cld φ ⟨“ ABC ”⟩ Word P
79 s3len ⟨“ ABC ”⟩ = 3
80 1 fvexi P V
81 3nn0 3 0
82 wrdmap P V 3 0 ⟨“ ABC ”⟩ Word P ⟨“ ABC ”⟩ = 3 ⟨“ ABC ”⟩ P 0 ..^ 3
83 80 81 82 mp2an ⟨“ ABC ”⟩ Word P ⟨“ ABC ”⟩ = 3 ⟨“ ABC ”⟩ P 0 ..^ 3
84 78 79 83 sylanblc φ ⟨“ ABC ”⟩ P 0 ..^ 3
85 8 9 10 s3cld φ ⟨“ DEF ”⟩ Word P
86 s3len ⟨“ DEF ”⟩ = 3
87 wrdmap P V 3 0 ⟨“ DEF ”⟩ Word P ⟨“ DEF ”⟩ = 3 ⟨“ DEF ”⟩ P 0 ..^ 3
88 80 81 87 mp2an ⟨“ DEF ”⟩ Word P ⟨“ DEF ”⟩ = 3 ⟨“ DEF ”⟩ P 0 ..^ 3
89 85 86 88 sylanblc φ ⟨“ DEF ”⟩ P 0 ..^ 3
90 84 89 jca φ ⟨“ ABC ”⟩ P 0 ..^ 3 ⟨“ DEF ”⟩ P 0 ..^ 3
91 90 biantrurd φ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F ⟨“ ABC ”⟩ P 0 ..^ 3 ⟨“ DEF ”⟩ P 0 ..^ 3 x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F
92 46 77 91 3bitr4d φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ x P y P ⟨“ ABC ”⟩ 𝒢 G ⟨“ xEy ”⟩ x K E D y K E F