Theorem mapdcnvatN

Description: Atoms are preserved by the map defined by df-mapd . (Contributed by NM, 29-May-2015) (New usage is discouraged.)

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

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		mapdcnvat.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
9		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
10	1 3 7	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
11		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
12	11 9	lsssn0	⊢ ( 𝑈 ∈ LMod → { ( 0g ‘ 𝑈 ) } ∈ ( LSubSp ‘ 𝑈 ) )
13	10 12	syl	⊢ ( 𝜑 → { ( 0g ‘ 𝑈 ) } ∈ ( LSubSp ‘ 𝑈 ) )
14	1 2 3 9 7 13	mapdcnvid1N	⊢ ( 𝜑 → ( ◡ 𝑀 ‘ ( 𝑀 ‘ { ( 0g ‘ 𝑈 ) } ) ) = { ( 0g ‘ 𝑈 ) } )
15		eqid	⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
16	1 2 3 11 5 15 7	mapd0	⊢ ( 𝜑 → ( 𝑀 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝐶 ) } )
17	16	fveq2d	⊢ ( 𝜑 → ( ◡ 𝑀 ‘ ( 𝑀 ‘ { ( 0g ‘ 𝑈 ) } ) ) = ( ◡ 𝑀 ‘ { ( 0g ‘ 𝐶 ) } ) )
18	14 17	eqtr3d	⊢ ( 𝜑 → { ( 0g ‘ 𝑈 ) } = ( ◡ 𝑀 ‘ { ( 0g ‘ 𝐶 ) } ) )
19		eqid	⊢ ( ⋖L ‘ 𝐶 ) = ( ⋖L ‘ 𝐶 )
20	1 5 7	lcdlvec	⊢ ( 𝜑 → 𝐶 ∈ LVec )
21	15 6 19 20 8	lsatcv0	⊢ ( 𝜑 → { ( 0g ‘ 𝐶 ) } ( ⋖L ‘ 𝐶 ) 𝑄 )
22	1 5 7	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
23		eqid	⊢ ( LSubSp ‘ 𝐶 ) = ( LSubSp ‘ 𝐶 )
24	15 23	lsssn0	⊢ ( 𝐶 ∈ LMod → { ( 0g ‘ 𝐶 ) } ∈ ( LSubSp ‘ 𝐶 ) )
25	22 24	syl	⊢ ( 𝜑 → { ( 0g ‘ 𝐶 ) } ∈ ( LSubSp ‘ 𝐶 ) )
26	1 2 5 23 7	mapdrn2	⊢ ( 𝜑 → ran 𝑀 = ( LSubSp ‘ 𝐶 ) )
27	25 26	eleqtrrd	⊢ ( 𝜑 → { ( 0g ‘ 𝐶 ) } ∈ ran 𝑀 )
28	1 2 7 27	mapdcnvid2	⊢ ( 𝜑 → ( 𝑀 ‘ ( ◡ 𝑀 ‘ { ( 0g ‘ 𝐶 ) } ) ) = { ( 0g ‘ 𝐶 ) } )
29	23 6 22 8	lsatlssel	⊢ ( 𝜑 → 𝑄 ∈ ( LSubSp ‘ 𝐶 ) )
30	29 26	eleqtrrd	⊢ ( 𝜑 → 𝑄 ∈ ran 𝑀 )
31	1 2 7 30	mapdcnvid2	⊢ ( 𝜑 → ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑄 ) ) = 𝑄 )
32	21 28 31	3brtr4d	⊢ ( 𝜑 → ( 𝑀 ‘ ( ◡ 𝑀 ‘ { ( 0g ‘ 𝐶 ) } ) ) ( ⋖L ‘ 𝐶 ) ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑄 ) ) )
33		eqid	⊢ ( ⋖L ‘ 𝑈 ) = ( ⋖L ‘ 𝑈 )
34	1 2 3 9 7 27	mapdcnvcl	⊢ ( 𝜑 → ( ◡ 𝑀 ‘ { ( 0g ‘ 𝐶 ) } ) ∈ ( LSubSp ‘ 𝑈 ) )
35	1 2 3 9 7 30	mapdcnvcl	⊢ ( 𝜑 → ( ◡ 𝑀 ‘ 𝑄 ) ∈ ( LSubSp ‘ 𝑈 ) )
36	1 2 3 9 33 5 19 7 34 35	mapdcv	⊢ ( 𝜑 → ( ( ◡ 𝑀 ‘ { ( 0g ‘ 𝐶 ) } ) ( ⋖L ‘ 𝑈 ) ( ◡ 𝑀 ‘ 𝑄 ) ↔ ( 𝑀 ‘ ( ◡ 𝑀 ‘ { ( 0g ‘ 𝐶 ) } ) ) ( ⋖L ‘ 𝐶 ) ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝑄 ) ) ) )
37	32 36	mpbird	⊢ ( 𝜑 → ( ◡ 𝑀 ‘ { ( 0g ‘ 𝐶 ) } ) ( ⋖L ‘ 𝑈 ) ( ◡ 𝑀 ‘ 𝑄 ) )
38	18 37	eqbrtrd	⊢ ( 𝜑 → { ( 0g ‘ 𝑈 ) } ( ⋖L ‘ 𝑈 ) ( ◡ 𝑀 ‘ 𝑄 ) )
39	1 3 7	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
40	11 9 4 33 39 35	lsat0cv	⊢ ( 𝜑 → ( ( ◡ 𝑀 ‘ 𝑄 ) ∈ 𝐴 ↔ { ( 0g ‘ 𝑈 ) } ( ⋖L ‘ 𝑈 ) ( ◡ 𝑀 ‘ 𝑄 ) ) )
41	38 40	mpbird	⊢ ( 𝜑 → ( ◡ 𝑀 ‘ 𝑄 ) ∈ 𝐴 )