tgaaddcpbllem2

	Ref	Expression
Hypotheses	tgaaddcpbl.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgaaddcpbl.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgaaddcpbl.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tgaaddcpbl.c	⊢ ∼ = ( cgrA ‘ 𝐺 )
	tgaaddcpbl.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	tgaaddcpbl.q	⊢ 𝑄 = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 𝑇 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) }
	tgaaddcpbl.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgaaddcpbl.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
	tgaaddcpbl.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
	tgaaddcpbl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
	tgaaddcpbl.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
	tgaaddcpbl.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
	tgaaddcpbl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	tgaaddcpbl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	tgaaddcpbl.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	tgaaddcpbl.2	⊢ ( 𝜑 → 𝑌 ≠ 𝑆 )
	tgaaddcpbl.3	⊢ ( 𝜑 → 𝑉 ≠ 𝑇 )
	tgaaddcpbl.4	⊢ ( 𝜑 → 𝑋 𝑂 𝑍 )
	tgaaddcpbl.5	⊢ ( 𝜑 → 𝑈 𝑄 𝑊 )
	tgaaddcpbl.6	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
	tgaaddcpbl.7	⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
	tgaaddcpbllem3.1	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
	tgaaddcpbllem2.1	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑌 𝐿 𝑆 ) )
	tgaaddcpbllem2.2	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐼 𝑍 ) )
	tgaaddcpbllem2.3	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑆 𝐼 𝑅 ) )
	tgaaddcpbllem2.m	⊢ 𝑀 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑉 )
	tgaaddcpbllem2.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
Assertion	tgaaddcpbllem2	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		tgaaddcpbl.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgaaddcpbl.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tgaaddcpbl.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tgaaddcpbl.c	⊢ ∼ = ( cgrA ‘ 𝐺 )
5		tgaaddcpbl.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) }
6		tgaaddcpbl.q	⊢ 𝑄 = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 𝑇 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) }
7		tgaaddcpbl.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8		tgaaddcpbl.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
9		tgaaddcpbl.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
10		tgaaddcpbl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
11		tgaaddcpbl.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
12		tgaaddcpbl.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
13		tgaaddcpbl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
14		tgaaddcpbl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
15		tgaaddcpbl.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
16		tgaaddcpbl.2	⊢ ( 𝜑 → 𝑌 ≠ 𝑆 )
17		tgaaddcpbl.3	⊢ ( 𝜑 → 𝑉 ≠ 𝑇 )
18		tgaaddcpbl.4	⊢ ( 𝜑 → 𝑋 𝑂 𝑍 )
19		tgaaddcpbl.5	⊢ ( 𝜑 → 𝑈 𝑄 𝑊 )
20		tgaaddcpbl.6	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
21		tgaaddcpbl.7	⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
22		tgaaddcpbllem3.1	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
23		tgaaddcpbllem2.1	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑌 𝐿 𝑆 ) )
24		tgaaddcpbllem2.2	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐼 𝑍 ) )
25		tgaaddcpbllem2.3	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑆 𝐼 𝑅 ) )
26		tgaaddcpbllem2.m	⊢ 𝑀 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑉 )
27		tgaaddcpbllem2.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
28		eleq1w	⊢ ( 𝑒 = 𝑠 → ( 𝑒 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) )
29	28	cbvrexvw	⊢ ( ∃ 𝑒 ∈ ( 𝑌 𝐿 𝑅 ) 𝑒 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑅 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) )
30	29	anbi2i	⊢ ( ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑅 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑅 ) ) ) ∧ ∃ 𝑒 ∈ ( 𝑌 𝐿 𝑅 ) 𝑒 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑅 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑅 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑅 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) )
31	30	opabbii	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑅 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑅 ) ) ) ∧ ∃ 𝑒 ∈ ( 𝑌 𝐿 𝑅 ) 𝑒 ∈ ( 𝑎 𝐼 𝑏 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑅 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑅 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑅 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) }
32		eleq1w	⊢ ( 𝑎 = 𝑐 → ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ↔ 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) )
33		eleq1w	⊢ ( 𝑏 = 𝑑 → ( 𝑏 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ↔ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) )
34	32 33	bi2anan9	⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) ↔ ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) ) )
35		oveq12	⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 𝐼 𝑏 ) = ( 𝑐 𝐼 𝑑 ) )
36	35	eleq2d	⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑓 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑓 ∈ ( 𝑐 𝐼 𝑑 ) ) )
37	36	rexbidv	⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ∃ 𝑓 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑓 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑓 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑓 ∈ ( 𝑐 𝐼 𝑑 ) ) )
38		eleq1w	⊢ ( 𝑓 = 𝑡 → ( 𝑓 ∈ ( 𝑐 𝐼 𝑑 ) ↔ 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) )
39	38	cbvrexvw	⊢ ( ∃ 𝑓 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑓 ∈ ( 𝑐 𝐼 𝑑 ) ↔ ∃ 𝑡 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) )
40	37 39	bitrdi	⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ∃ 𝑓 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑓 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑡 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) )
41	34 40	anbi12d	⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) ∧ ∃ 𝑓 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑓 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) ) )
42	41	cbvopabv	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) ∧ ∃ 𝑓 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑓 ∈ ( 𝑎 𝐼 𝑏 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) }
43	1 2 3 7 14 8 16	tgelrnln	⊢ ( 𝜑 → ( 𝑌 𝐿 𝑆 ) ∈ ran 𝐿 )
44	1 3 2 7 43 23	tglnpt	⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
45		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
46		eqid	⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
47	1 45 2 3 46 7 11 26 9	mircl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) ∈ 𝑃 )
48	24 22	elnelneq2d	⊢ ( 𝜑 → ¬ 𝑅 = 𝑌 )
49	48	neqned	⊢ ( 𝜑 → 𝑅 ≠ 𝑌 )
50	49	necomd	⊢ ( 𝜑 → 𝑌 ≠ 𝑅 )
51	17	necomd	⊢ ( 𝜑 → 𝑇 ≠ 𝑉 )
52	1 45 2 3 46 7 11 26 9 51	mirne	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) ≠ 𝑉 )
53	52	necomd	⊢ ( 𝜑 → 𝑉 ≠ ( 𝑀 ‘ 𝑇 ) )
54	1 2 3 7 14 44 50	tglinerflx2	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑌 𝐿 𝑅 ) )
55	1 45 2 5 3 43 7 13 15 18	oppne1	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) )
56	1 2 3 7 14 8 16 44 49 23	tglineelsb2	⊢ ( 𝜑 → ( 𝑌 𝐿 𝑆 ) = ( 𝑌 𝐿 𝑅 ) )
57	55 56	neleqtrd	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑅 ) )
58	1 45 2 5 3 43 7 13 15 18	oppne2	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) )
59	58 56	neleqtrd	⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑅 ) )
60	1 45 2 31 13 15 54 57 59 24	islnoppd	⊢ ( 𝜑 → 𝑋 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑅 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑅 ) ) ) ∧ ∃ 𝑒 ∈ ( 𝑌 𝐿 𝑅 ) 𝑒 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑍 )
61	1 45 2 3 46 7 11 26 9	mirbtwn	⊢ ( 𝜑 → 𝑉 ∈ ( ( 𝑀 ‘ 𝑇 ) 𝐼 𝑇 ) )
62	1 2 3 7 11 9 47 17 61	btwnlng2	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) ∈ ( 𝑉 𝐿 𝑇 ) )
63	1 2 3 7 11 9 17 47 52 62	tglineelsb2	⊢ ( 𝜑 → ( 𝑉 𝐿 𝑇 ) = ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) )
64	63	difeq2d	⊢ ( 𝜑 → ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) = ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) )
65	64	eleq2d	⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ↔ 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) )
66	64	eleq2d	⊢ ( 𝜑 → ( 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ↔ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) )
67	65 66	anbi12d	⊢ ( 𝜑 → ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ↔ ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) ) )
68	63	rexeqdv	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ( 𝑉 𝐿 𝑇 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ↔ ∃ 𝑡 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) )
69	67 68	anbi12d	⊢ ( 𝜑 → ( ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 𝑇 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) ↔ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) ) )
70	69	opabbidv	⊢ ( 𝜑 → { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 𝑇 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) } )
71	70 6 42	3eqtr4g	⊢ ( 𝜑 → 𝑄 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) ∧ ∃ 𝑓 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑓 ∈ ( 𝑎 𝐼 𝑏 ) ) } )
72	71 19	breqdi	⊢ ( 𝜑 → 𝑈 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) ) ) ∧ ∃ 𝑓 ∈ ( 𝑉 𝐿 ( 𝑀 ‘ 𝑇 ) ) 𝑓 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑊 )
73	4	a1i	⊢ ( 𝜑 → ∼ = ( cgrA ‘ 𝐺 ) )
74	73	eqcomd	⊢ ( 𝜑 → ( cgrA ‘ 𝐺 ) = ∼ )
75	73 20	breqdi	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
76	1 2 45 7 13 14 8 10 11 9 75	cgraswaplr	⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑋 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑈 ”⟩ )
77	1 45 2 7 47 11 9 61	tgbtwncom	⊢ ( 𝜑 → 𝑉 ∈ ( 𝑇 𝐼 ( 𝑀 ‘ 𝑇 ) ) )
78	1 2 45 7 8 14 13 9 11 10 44 47 76 25 77 50 53	sacgr	⊢ ( 𝜑 → ⟨“ 𝑅 𝑌 𝑋 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑀 ‘ 𝑇 ) 𝑉 𝑈 ”⟩ )
79	1 2 45 7 44 14 13 47 11 10 78	cgraswaplr	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑅 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 ( 𝑀 ‘ 𝑇 ) ”⟩ )
80	74 79	breqdi	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑅 ”⟩ ∼ ⟨“ 𝑈 𝑉 ( 𝑀 ‘ 𝑇 ) ”⟩ )
81	73 21	breqdi	⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
82	1 2 45 7 8 14 15 9 11 12 44 47 81 25 77 50 53	sacgr	⊢ ( 𝜑 → ⟨“ 𝑅 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( 𝑀 ‘ 𝑇 ) 𝑉 𝑊 ”⟩ )
83	74 82	breqdi	⊢ ( 𝜑 → ⟨“ 𝑅 𝑌 𝑍 ”⟩ ∼ ⟨“ ( 𝑀 ‘ 𝑇 ) 𝑉 𝑊 ”⟩ )
84	1 2 27 44 13 14 7 49	hlid	⊢ ( 𝜑 → 𝑅 ( 𝐾 ‘ 𝑌 ) 𝑅 )
85	1 2 3 4 31 42 7 44 47 10 11 12 13 14 15 50 53 60 72 80 83 22 27 54 24 84	tgaaddcpbllem1	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )

Metamath Proof Explorer

Theorem tgaaddcpbllem2

Proof