Theorem mapdat

Description: Atoms are preserved by the map defined by df-mapd . Property (g) in Baer p. 41. (Contributed by NM, 14-Mar-2015)

	Ref	Expression
Hypotheses	mapdat.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	mapdat.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	mapdat.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	mapdat.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
	mapdat.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	mapdat.b	⊢ 𝐵 = ( LSAtoms ‘ 𝐶 )
	mapdat.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	mapdat.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion	mapdat	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑄 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mapdat.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		mapdat.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3		mapdat.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		mapdat.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
5		mapdat.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		mapdat.b	⊢ 𝐵 = ( LSAtoms ‘ 𝐶 )
7		mapdat.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		mapdat.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
9		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
10		eqid	⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
11	1 2 3 9 5 10 7	mapd0	⊢ ( 𝜑 → ( 𝑀 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝐶 ) } )
12		eqid	⊢ ( ⋖L ‘ 𝑈 ) = ( ⋖L ‘ 𝑈 )
13	1 3 7	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
14	9 4 12 13 8	lsatcv0	⊢ ( 𝜑 → { ( 0g ‘ 𝑈 ) } ( ⋖L ‘ 𝑈 ) 𝑄 )
15		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
16		eqid	⊢ ( ⋖L ‘ 𝐶 ) = ( ⋖L ‘ 𝐶 )
17	1 3 7	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
18	9 15	lsssn0	⊢ ( 𝑈 ∈ LMod → { ( 0g ‘ 𝑈 ) } ∈ ( LSubSp ‘ 𝑈 ) )
19	17 18	syl	⊢ ( 𝜑 → { ( 0g ‘ 𝑈 ) } ∈ ( LSubSp ‘ 𝑈 ) )
20	15 4 17 8	lsatlssel	⊢ ( 𝜑 → 𝑄 ∈ ( LSubSp ‘ 𝑈 ) )
21	1 2 3 15 12 5 16 7 19 20	mapdcv	⊢ ( 𝜑 → ( { ( 0g ‘ 𝑈 ) } ( ⋖L ‘ 𝑈 ) 𝑄 ↔ ( 𝑀 ‘ { ( 0g ‘ 𝑈 ) } ) ( ⋖L ‘ 𝐶 ) ( 𝑀 ‘ 𝑄 ) ) )
22	14 21	mpbid	⊢ ( 𝜑 → ( 𝑀 ‘ { ( 0g ‘ 𝑈 ) } ) ( ⋖L ‘ 𝐶 ) ( 𝑀 ‘ 𝑄 ) )
23	11 22	eqbrtrrd	⊢ ( 𝜑 → { ( 0g ‘ 𝐶 ) } ( ⋖L ‘ 𝐶 ) ( 𝑀 ‘ 𝑄 ) )
24		eqid	⊢ ( LSubSp ‘ 𝐶 ) = ( LSubSp ‘ 𝐶 )
25	1 5 7	lcdlvec	⊢ ( 𝜑 → 𝐶 ∈ LVec )
26	1 2 3 15 5 24 7 20	mapdcl2	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝐶 ) )
27	10 24 6 16 25 26	lsat0cv	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑄 ) ∈ 𝐵 ↔ { ( 0g ‘ 𝐶 ) } ( ⋖L ‘ 𝐶 ) ( 𝑀 ‘ 𝑄 ) ) )
28	23 27	mpbird	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑄 ) ∈ 𝐵 )