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

Metamath Proof Explorer

Theorem restco

Description: Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion restco ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐽 ↾t 𝐴 ) ↾t 𝐵 ) = ( 𝐽 ↾t ( 𝐴 ∩ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑦 ∈ V
2 1 inex1 ⊢ ( 𝑦 ∩ 𝐴 ) ∈ V
3 ineq1 ⊢ ( 𝑥 = ( 𝑦 ∩ 𝐴 ) → ( 𝑥 ∩ 𝐵 ) = ( ( 𝑦 ∩ 𝐴 ) ∩ 𝐵 ) )
4 inass ⊢ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝐵 ) = ( 𝑦 ∩ ( 𝐴 ∩ 𝐵 ) )
5 3 4 eqtrdi ⊢ ( 𝑥 = ( 𝑦 ∩ 𝐴 ) → ( 𝑥 ∩ 𝐵 ) = ( 𝑦 ∩ ( 𝐴 ∩ 𝐵 ) ) )
6 2 5 abrexco ⊢ { 𝑧 ∣ ∃ 𝑥 ∈ { 𝑤 ∣ ∃ 𝑦 ∈ 𝐽 𝑤 = ( 𝑦 ∩ 𝐴 ) } 𝑧 = ( 𝑥 ∩ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐽 𝑧 = ( 𝑦 ∩ ( 𝐴 ∩ 𝐵 ) ) }
7 eqid ⊢ ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) = ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) )
8 7 rnmpt ⊢ ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) = { 𝑤 ∣ ∃ 𝑦 ∈ 𝐽 𝑤 = ( 𝑦 ∩ 𝐴 ) }
9 8 mpteq1i ⊢ ( 𝑥 ∈ ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) ↦ ( 𝑥 ∩ 𝐵 ) ) = ( 𝑥 ∈ { 𝑤 ∣ ∃ 𝑦 ∈ 𝐽 𝑤 = ( 𝑦 ∩ 𝐴 ) } ↦ ( 𝑥 ∩ 𝐵 ) )
10 9 rnmpt ⊢ ran ( 𝑥 ∈ ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) ↦ ( 𝑥 ∩ 𝐵 ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ { 𝑤 ∣ ∃ 𝑦 ∈ 𝐽 𝑤 = ( 𝑦 ∩ 𝐴 ) } 𝑧 = ( 𝑥 ∩ 𝐵 ) }
11 eqid ⊢ ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ ( 𝐴 ∩ 𝐵 ) ) ) = ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ ( 𝐴 ∩ 𝐵 ) ) )
12 11 rnmpt ⊢ ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ ( 𝐴 ∩ 𝐵 ) ) ) = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐽 𝑧 = ( 𝑦 ∩ ( 𝐴 ∩ 𝐵 ) ) }
13 6 10 12 3eqtr4i ⊢ ran ( 𝑥 ∈ ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) ↦ ( 𝑥 ∩ 𝐵 ) ) = ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ ( 𝐴 ∩ 𝐵 ) ) )
14 restval ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐽 ↾t 𝐴 ) = ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) )
15 14 3adant3 ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) = ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) )
16 15 oveq1d ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐽 ↾t 𝐴 ) ↾t 𝐵 ) = ( ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) ↾t 𝐵 ) )
17 ovex ⊢ ( 𝐽 ↾t 𝐴 ) ∈ V
18 15 17 eqeltrrdi ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) → ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) ∈ V )
19 simp3 ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
20 restval ⊢ ( ( ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) ∈ V ∧ 𝐵 ∈ 𝑋 ) → ( ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) ↾t 𝐵 ) = ran ( 𝑥 ∈ ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) ↦ ( 𝑥 ∩ 𝐵 ) ) )
21 18 19 20 syl2anc ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) → ( ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) ↾t 𝐵 ) = ran ( 𝑥 ∈ ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) ↦ ( 𝑥 ∩ 𝐵 ) ) )
22 16 21 eqtrd ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐽 ↾t 𝐴 ) ↾t 𝐵 ) = ran ( 𝑥 ∈ ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ 𝐴 ) ) ↦ ( 𝑥 ∩ 𝐵 ) ) )
23 simp1 ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) → 𝐽 ∈ 𝑉 )
24 inex1g ⊢ ( 𝐴 ∈ 𝑊 → ( 𝐴 ∩ 𝐵 ) ∈ V )
25 24 3ad2ant2 ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∩ 𝐵 ) ∈ V )
26 restval ⊢ ( ( 𝐽 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ∈ V ) → ( 𝐽 ↾t ( 𝐴 ∩ 𝐵 ) ) = ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ ( 𝐴 ∩ 𝐵 ) ) ) )
27 23 25 26 syl2anc ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐽 ↾t ( 𝐴 ∩ 𝐵 ) ) = ran ( 𝑦 ∈ 𝐽 ↦ ( 𝑦 ∩ ( 𝐴 ∩ 𝐵 ) ) ) )
28 13 22 27 3eqtr4a ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐽 ↾t 𝐴 ) ↾t 𝐵 ) = ( 𝐽 ↾t ( 𝐴 ∩ 𝐵 ) ) )