Theorem mapdunirnN

Description: Union of the range of the map defined by df-mapd . (Contributed by NM, 13-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdrn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	mapdrn.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	mapdrn.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	mapdrn.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	mapdrn.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	mapdrn.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	mapdunirn.c	⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
	mapdunirn.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	mapdunirnN	⊢ ( 𝜑 → ∪ ran 𝑀 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		mapdrn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		mapdrn.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		mapdrn.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
4		mapdrn.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		mapdrn.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6		mapdrn.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
7		mapdunirn.c	⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
8		mapdunirn.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		eqid	⊢ ( LDual ‘ 𝑈 ) = ( LDual ‘ 𝑈 )
10		eqid	⊢ ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) = ( LSubSp ‘ ( LDual ‘ 𝑈 ) )
11	1 2 3 4 5 6 9 10 7 8	mapdrn	⊢ ( 𝜑 → ran 𝑀 = ( ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ 𝒫 𝐶 ) )
12	11	unieqd	⊢ ( 𝜑 → ∪ ran 𝑀 = ∪ ( ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ 𝒫 𝐶 ) )
13		uniin	⊢ ∪ ( ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ 𝒫 𝐶 ) ⊆ ( ∪ ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ ∪ 𝒫 𝐶 )
14		eqid	⊢ ( Base ‘ ( LDual ‘ 𝑈 ) ) = ( Base ‘ ( LDual ‘ 𝑈 ) )
15	1 4 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
16	9 15	lduallmod	⊢ ( 𝜑 → ( LDual ‘ 𝑈 ) ∈ LMod )
17	14 10 16	lssuni	⊢ ( 𝜑 → ∪ ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) = ( Base ‘ ( LDual ‘ 𝑈 ) ) )
18	5 9 14 15	ldualvbase	⊢ ( 𝜑 → ( Base ‘ ( LDual ‘ 𝑈 ) ) = 𝐹 )
19	17 18	eqtrd	⊢ ( 𝜑 → ∪ ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) = 𝐹 )
20		unipw	⊢ ∪ 𝒫 𝐶 = 𝐶
21	20	a1i	⊢ ( 𝜑 → ∪ 𝒫 𝐶 = 𝐶 )
22	19 21	ineq12d	⊢ ( 𝜑 → ( ∪ ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ ∪ 𝒫 𝐶 ) = ( 𝐹 ∩ 𝐶 ) )
23		ssrab2	⊢ { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) } ⊆ 𝐹
24	7 23	eqsstri	⊢ 𝐶 ⊆ 𝐹
25		sseqin2	⊢ ( 𝐶 ⊆ 𝐹 ↔ ( 𝐹 ∩ 𝐶 ) = 𝐶 )
26	24 25	mpbi	⊢ ( 𝐹 ∩ 𝐶 ) = 𝐶
27	26	a1i	⊢ ( 𝜑 → ( 𝐹 ∩ 𝐶 ) = 𝐶 )
28	22 27	eqtrd	⊢ ( 𝜑 → ( ∪ ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ ∪ 𝒫 𝐶 ) = 𝐶 )
29	13 28	sseqtrid	⊢ ( 𝜑 → ∪ ( ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ 𝒫 𝐶 ) ⊆ 𝐶 )
30	1 4 2 5 6 9 10 7 8	lclkr	⊢ ( 𝜑 → 𝐶 ∈ ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) )
31	5	fvexi	⊢ 𝐹 ∈ V
32	7 31	rabex2	⊢ 𝐶 ∈ V
33	32	pwid	⊢ 𝐶 ∈ 𝒫 𝐶
34	33	a1i	⊢ ( 𝜑 → 𝐶 ∈ 𝒫 𝐶 )
35	30 34	elind	⊢ ( 𝜑 → 𝐶 ∈ ( ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ 𝒫 𝐶 ) )
36		elssuni	⊢ ( 𝐶 ∈ ( ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ 𝒫 𝐶 ) → 𝐶 ⊆ ∪ ( ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ 𝒫 𝐶 ) )
37	35 36	syl	⊢ ( 𝜑 → 𝐶 ⊆ ∪ ( ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ 𝒫 𝐶 ) )
38	29 37	eqssd	⊢ ( 𝜑 → ∪ ( ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ 𝒫 𝐶 ) = 𝐶 )
39	12 38	eqtrd	⊢ ( 𝜑 → ∪ ran 𝑀 = 𝐶 )