# Metamath Proof Explorer

## Theorem hdmapip0com

Description: Commutation property of Baer's sigma map (Holland's A map). Line 20 of Holland95 p. 14. Also part of Lemma 1 of Baer p. 110 line 7. (Contributed by NM, 9-Jun-2015)

Ref Expression
Hypotheses hdmapip0com.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmapip0com.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmapip0com.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmapip0com.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
hdmapip0com.z
hdmapip0com.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
hdmapip0com.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hdmapip0com.x ${⊢}{\phi }\to {X}\in {V}$
hdmapip0com.y ${⊢}{\phi }\to {Y}\in {V}$
Assertion hdmapip0com

### Proof

Step Hyp Ref Expression
1 hdmapip0com.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmapip0com.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hdmapip0com.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 hdmapip0com.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
5 hdmapip0com.z
6 hdmapip0com.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
7 hdmapip0com.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
8 hdmapip0com.x ${⊢}{\phi }\to {X}\in {V}$
9 hdmapip0com.y ${⊢}{\phi }\to {Y}\in {V}$
10 eqid ${⊢}\mathrm{ocH}\left({K}\right)\left({W}\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)$
11 1 10 2 3 7 9 8 dochsncom ${⊢}{\phi }\to \left({Y}\in \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\left\{{X}\right\}\right)↔{X}\in \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\left\{{Y}\right\}\right)\right)$
12 1 10 2 3 4 5 6 7 8 9 hdmapellkr
13 1 10 2 3 4 5 6 7 9 8 hdmapellkr
14 11 12 13 3bitr4d