Theorem tglinecom

Description: Commutativity law for lines. Part of theorem 6.17 of Schwabhauser p. 45. (Contributed by Thierry Arnoux, 17-May-2019)

	Ref	Expression
Hypotheses	tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglineelsb2.1	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
	tglineelsb2.2	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
	tglineelsb2.4	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
Assertion	tglinecom	⊢ ( 𝜑 → ( 𝑃 𝐿 𝑄 ) = ( 𝑄 𝐿 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tglineelsb2.1	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
6		tglineelsb2.2	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
7		tglineelsb2.4	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
8	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝐺 ∈ TarskiG )
9	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑄 ∈ 𝐵 )
10	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑃 ∈ 𝐵 )
11	1 3 2 4 5 6 7	tglnssp	⊢ ( 𝜑 → ( 𝑃 𝐿 𝑄 ) ⊆ 𝐵 )
12	11	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑥 ∈ 𝐵 )
13	7	necomd	⊢ ( 𝜑 → 𝑄 ≠ 𝑃 )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑄 ≠ 𝑃 )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) )
16	1 2 3 8 9 10 12 14 15	lncom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑥 ∈ ( 𝑄 𝐿 𝑃 ) )
17	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑄 𝐿 𝑃 ) ) → 𝐺 ∈ TarskiG )
18	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑄 𝐿 𝑃 ) ) → 𝑃 ∈ 𝐵 )
19	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑄 𝐿 𝑃 ) ) → 𝑄 ∈ 𝐵 )
20	1 3 2 4 6 5 13	tglnssp	⊢ ( 𝜑 → ( 𝑄 𝐿 𝑃 ) ⊆ 𝐵 )
21	20	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑄 𝐿 𝑃 ) ) → 𝑥 ∈ 𝐵 )
22	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑄 𝐿 𝑃 ) ) → 𝑃 ≠ 𝑄 )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑄 𝐿 𝑃 ) ) → 𝑥 ∈ ( 𝑄 𝐿 𝑃 ) )
24	1 2 3 17 18 19 21 22 23	lncom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑄 𝐿 𝑃 ) ) → 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) )
25	16 24	impbida	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ↔ 𝑥 ∈ ( 𝑄 𝐿 𝑃 ) ) )
26	25	eqrdv	⊢ ( 𝜑 → ( 𝑃 𝐿 𝑄 ) = ( 𝑄 𝐿 𝑃 ) )