Metamath Proof Explorer

Theorem doca3N

Description: Double orthocomplement of partial isomorphism A. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses doca2.h ⊢ H = LHyp ⁡ K
doca2.i ⊢ I = DIsoA ⁡ K ⁡ W
doca2.n ⊢ ⊥ ˙ = ocA ⁡ K ⁡ W
Assertion doca3N ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X

Proof

Step Hyp Ref Expression
1 doca2.h ⊢ H = LHyp ⁡ K
2 doca2.i ⊢ I = DIsoA ⁡ K ⁡ W
3 doca2.n ⊢ ⊥ ˙ = ocA ⁡ K ⁡ W
4 1 2 diacnvclN ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ dom ⁡ I
5 1 2 3 doca2N ⊢ K ∈ HL ∧ W ∈ H ∧ I -1 ⁡ X ∈ dom ⁡ I → ⊥ ˙ ⁡ ⊥ ˙ ⁡ I ⁡ I -1 ⁡ X = I ⁡ I -1 ⁡ X
6 4 5 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → ⊥ ˙ ⁡ ⊥ ˙ ⁡ I ⁡ I -1 ⁡ X = I ⁡ I -1 ⁡ X
7 1 2 diaf11N ⊢ K ∈ HL ∧ W ∈ H → I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I
8 f1ocnvfv2 ⊢ I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I ∧ X ∈ ran ⁡ I → I ⁡ I -1 ⁡ X = X
9 7 8 sylan ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I ⁡ I -1 ⁡ X = X
10 9 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → ⊥ ˙ ⁡ I ⁡ I -1 ⁡ X = ⊥ ˙ ⁡ X
11 10 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → ⊥ ˙ ⁡ ⊥ ˙ ⁡ I ⁡ I -1 ⁡ X = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
12 6 11 9 3eqtr3d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X