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 ( 𝐴 ∩ 𝐵 ) ) )