This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmtrdifellem3

Description: Lemma 3 for pmtrdifel . (Contributed by AV, 15-Jan-2019)

Ref Expression
Hypotheses pmtrdifel.t ⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
pmtrdifel.r ⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
pmtrdifel.0 ⊢ 𝑆 = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) )
Assertion pmtrdifellem3 ( 𝑄 ∈ 𝑇 → ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 pmtrdifel.t ⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
2 pmtrdifel.r ⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
3 pmtrdifel.0 ⊢ 𝑆 = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑄 ∖ I ) )
4 1 2 3 pmtrdifellem2 ⊢ ( 𝑄 ∈ 𝑇 → dom ( 𝑆 ∖ I ) = dom ( 𝑄 ∖ I ) )
5 4 adantr ⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → dom ( 𝑆 ∖ I ) = dom ( 𝑄 ∖ I ) )
6 5 eleq2d ⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑥 ∈ dom ( 𝑆 ∖ I ) ↔ 𝑥 ∈ dom ( 𝑄 ∖ I ) ) )
7 4 difeq1d ⊢ ( 𝑄 ∈ 𝑇 → ( dom ( 𝑆 ∖ I ) ∖ { 𝑥 } ) = ( dom ( 𝑄 ∖ I ) ∖ { 𝑥 } ) )
8 7 unieqd ⊢ ( 𝑄 ∈ 𝑇 → ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝑥 } ) = ∪ ( dom ( 𝑄 ∖ I ) ∖ { 𝑥 } ) )
9 8 adantr ⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝑥 } ) = ∪ ( dom ( 𝑄 ∖ I ) ∖ { 𝑥 } ) )
10 6 9 ifbieq1d ⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → if ( 𝑥 ∈ dom ( 𝑆 ∖ I ) , ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝑥 } ) , 𝑥 ) = if ( 𝑥 ∈ dom ( 𝑄 ∖ I ) , ∪ ( dom ( 𝑄 ∖ I ) ∖ { 𝑥 } ) , 𝑥 ) )
11 1 2 3 pmtrdifellem1 ⊢ ( 𝑄 ∈ 𝑇 → 𝑆 ∈ 𝑅 )
12 eldifi ⊢ ( 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) → 𝑥 ∈ 𝑁 )
13 eqid ⊢ ( pmTrsp ‘ 𝑁 ) = ( pmTrsp ‘ 𝑁 )
14 eqid ⊢ dom ( 𝑆 ∖ I ) = dom ( 𝑆 ∖ I )
15 13 2 14 pmtrffv ⊢ ( ( 𝑆 ∈ 𝑅 ∧ 𝑥 ∈ 𝑁 ) → ( 𝑆 ‘ 𝑥 ) = if ( 𝑥 ∈ dom ( 𝑆 ∖ I ) , ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝑥 } ) , 𝑥 ) )
16 11 12 15 syl2an ⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑆 ‘ 𝑥 ) = if ( 𝑥 ∈ dom ( 𝑆 ∖ I ) , ∪ ( dom ( 𝑆 ∖ I ) ∖ { 𝑥 } ) , 𝑥 ) )
17 eqid ⊢ ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
18 eqid ⊢ dom ( 𝑄 ∖ I ) = dom ( 𝑄 ∖ I )
19 17 1 18 pmtrffv ⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑄 ‘ 𝑥 ) = if ( 𝑥 ∈ dom ( 𝑄 ∖ I ) , ∪ ( dom ( 𝑄 ∖ I ) ∖ { 𝑥 } ) , 𝑥 ) )
20 10 16 19 3eqtr4rd ⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑄 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
21 20 ralrimiva ⊢ ( 𝑄 ∈ 𝑇 → ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑄 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )