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	|- B = ( Base ` G )
	tglineelsb2.i	|- I = ( Itv ` G )
	tglineelsb2.l	|- L = ( LineG ` G )
	tglineelsb2.g	|- ( ph -> G e. TarskiG )
	tglineelsb2.1	|- ( ph -> P e. B )
	tglineelsb2.2	|- ( ph -> Q e. B )
	tglineelsb2.4	|- ( ph -> P =/= Q )
Assertion	tglinecom	|- ( ph -> ( P L Q ) = ( Q L P ) )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	|- B = ( Base ` G )
2		tglineelsb2.i	|- I = ( Itv ` G )
3		tglineelsb2.l	|- L = ( LineG ` G )
4		tglineelsb2.g	|- ( ph -> G e. TarskiG )
5		tglineelsb2.1	|- ( ph -> P e. B )
6		tglineelsb2.2	|- ( ph -> Q e. B )
7		tglineelsb2.4	|- ( ph -> P =/= Q )
8	4	adantr	|- ( ( ph /\ x e. ( P L Q ) ) -> G e. TarskiG )
9	6	adantr	|- ( ( ph /\ x e. ( P L Q ) ) -> Q e. B )
10	5	adantr	|- ( ( ph /\ x e. ( P L Q ) ) -> P e. B )
11	1 3 2 4 5 6 7	tglnssp	|- ( ph -> ( P L Q ) C_ B )
12	11	sselda	|- ( ( ph /\ x e. ( P L Q ) ) -> x e. B )
13	7	necomd	|- ( ph -> Q =/= P )
14	13	adantr	|- ( ( ph /\ x e. ( P L Q ) ) -> Q =/= P )
15		simpr	|- ( ( ph /\ x e. ( P L Q ) ) -> x e. ( P L Q ) )
16	1 2 3 8 9 10 12 14 15	lncom	|- ( ( ph /\ x e. ( P L Q ) ) -> x e. ( Q L P ) )
17	4	adantr	|- ( ( ph /\ x e. ( Q L P ) ) -> G e. TarskiG )
18	5	adantr	|- ( ( ph /\ x e. ( Q L P ) ) -> P e. B )
19	6	adantr	|- ( ( ph /\ x e. ( Q L P ) ) -> Q e. B )
20	1 3 2 4 6 5 13	tglnssp	|- ( ph -> ( Q L P ) C_ B )
21	20	sselda	|- ( ( ph /\ x e. ( Q L P ) ) -> x e. B )
22	7	adantr	|- ( ( ph /\ x e. ( Q L P ) ) -> P =/= Q )
23		simpr	|- ( ( ph /\ x e. ( Q L P ) ) -> x e. ( Q L P ) )
24	1 2 3 17 18 19 21 22 23	lncom	|- ( ( ph /\ x e. ( Q L P ) ) -> x e. ( P L Q ) )
25	16 24	impbida	|- ( ph -> ( x e. ( P L Q ) <-> x e. ( Q L P ) ) )
26	25	eqrdv	|- ( ph -> ( P L Q ) = ( Q L P ) )