Metamath Proof Explorer


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 ( 𝜑 → ( 𝑃 𝐿 𝑄 ) = ( 𝑄 𝐿 𝑃 ) )