Metamath Proof Explorer

Theorem isplng

Description: The property of being a plane. (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
isplng.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
Assertion isplng ( 𝜑 → ∃ 𝑎 ∈ ran 𝐿 ∃ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) 𝐻 = ( 𝑎 𝐸 𝑟 ) )

Proof

Step Hyp Ref Expression
1 plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
5 plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 isplng.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
7 df-plng ⊢ hlG = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) , 𝑟 ∈ ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } ) )
8 fveq2 ⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = ( LineG ‘ 𝐺 ) )
9 8 3 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = 𝐿 )
10 9 rneqd ⊢ ( 𝑔 = 𝐺 → ran ( LineG ‘ 𝑔 ) = ran 𝐿 )
11 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
12 11 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
13 12 difeq1d ⊢ ( 𝑔 = 𝐺 → ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) = ( 𝑃 ∖ 𝑎 ) )
14 biidd ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ 𝑎 ↔ 𝑥 ∈ 𝑎 ) )
15 fveq2 ⊢ ( 𝑔 = 𝐺 → ( hpG ‘ 𝑔 ) = ( hpG ‘ 𝐺 ) )
16 15 fveq1d ⊢ ( 𝑔 = 𝐺 → ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) = ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) )
17 16 breqd ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ↔ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ) )
18 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = ( Itv ‘ 𝐺 ) )
19 18 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = 𝐼 )
20 19 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) = ( 𝑥 𝐼 𝑟 ) )
21 20 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ↔ 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) )
22 21 rexbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ↔ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) )
23 14 17 22 3orbi123d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) ↔ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) ) )
24 12 23 rabeqbidv ⊢ ( 𝑔 = 𝐺 → { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } )
25 10 13 24 mpoeq123dv ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) , 𝑟 ∈ ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } ) = ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) )
26 5 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
27 3 fvexi ⊢ 𝐿 ∈ V
28 27 rnex ⊢ ran 𝐿 ∈ V
29 28 a1i ⊢ ( 𝜑 → ran 𝐿 ∈ V )
30 1 fvexi ⊢ 𝑃 ∈ V
31 30 difexi ⊢ ( 𝑃 ∖ 𝑎 ) ∈ V
32 31 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) → ( 𝑃 ∖ 𝑎 ) ∈ V )
33 29 32 mpoexd ⊢ ( 𝜑 → ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) ∈ V )
34 7 25 26 33 fvmptd3 ⊢ ( 𝜑 → ( hlG ‘ 𝐺 ) = ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) )
35 4 34 eqtrid ⊢ ( 𝜑 → 𝐸 = ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) )
36 35 rneqd ⊢ ( 𝜑 → ran 𝐸 = ran ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) )
37 6 36 eleqtrd ⊢ ( 𝜑 → 𝐻 ∈ ran ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) )
38 eqid ⊢ ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) = ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } )
39 30 rabex ⊢ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ∈ V
40 38 39 elrnmpo ⊢ ( 𝐻 ∈ ran ( 𝑎 ∈ ran 𝐿 , 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ↦ { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) ↔ ∃ 𝑎 ∈ ran 𝐿 ∃ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) 𝐻 = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } )
41 37 40 sylib ⊢ ( 𝜑 → ∃ 𝑎 ∈ ran 𝐿 ∃ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) 𝐻 = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } )
42 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) → 𝐺 ∈ TarskiG )
43 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) → 𝑎 ∈ ran 𝐿 )
44 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) → 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) )
45 1 2 3 4 42 43 44 plngval ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) → ( 𝑎 𝐸 𝑟 ) = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } )
46 45 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) → ( 𝐻 = ( 𝑎 𝐸 𝑟 ) ↔ 𝐻 = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } ) )
47 46 biimprd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) → ( 𝐻 = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } → 𝐻 = ( 𝑎 𝐸 𝑟 ) ) )
48 47 anasss ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran 𝐿 ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ) → ( 𝐻 = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } → 𝐻 = ( 𝑎 𝐸 𝑟 ) ) )
49 48 reximdvva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ran 𝐿 ∃ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) 𝐻 = { 𝑥 ∈ 𝑃 ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝐺 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 𝐼 𝑟 ) ) } → ∃ 𝑎 ∈ ran 𝐿 ∃ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) 𝐻 = ( 𝑎 𝐸 𝑟 ) ) )
50 41 49 mpd ⊢ ( 𝜑 → ∃ 𝑎 ∈ ran 𝐿 ∃ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) 𝐻 = ( 𝑎 𝐸 𝑟 ) )