# Metamath Proof Explorer

## Theorem cdj3lem3

Description: Lemma for cdj3i . Value of the second-component function T . (Contributed by NM, 23-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses cdj3lem2.1 ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
cdj3lem2.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
cdj3lem3.3 ${⊢}{T}=\left({x}\in \left({A}{+}_{ℋ}{B}\right)⟼\left(\iota {w}\in {B}|\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{w}\right)\right)$
Assertion cdj3lem3 ${⊢}\left({C}\in {A}\wedge {D}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to {T}\left({C}{+}_{ℎ}{D}\right)={D}$

### Proof

Step Hyp Ref Expression
1 cdj3lem2.1 ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
2 cdj3lem2.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
3 cdj3lem3.3 ${⊢}{T}=\left({x}\in \left({A}{+}_{ℋ}{B}\right)⟼\left(\iota {w}\in {B}|\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{w}\right)\right)$
4 incom ${⊢}{A}\cap {B}={B}\cap {A}$
5 4 eqeq1i ${⊢}{A}\cap {B}={0}_{ℋ}↔{B}\cap {A}={0}_{ℋ}$
6 2 sheli ${⊢}{D}\in {B}\to {D}\in ℋ$
7 1 sheli ${⊢}{C}\in {A}\to {C}\in ℋ$
8 ax-hvcom ${⊢}\left({D}\in ℋ\wedge {C}\in ℋ\right)\to {D}{+}_{ℎ}{C}={C}{+}_{ℎ}{D}$
9 6 7 8 syl2an ${⊢}\left({D}\in {B}\wedge {C}\in {A}\right)\to {D}{+}_{ℎ}{C}={C}{+}_{ℎ}{D}$
10 9 fveq2d ${⊢}\left({D}\in {B}\wedge {C}\in {A}\right)\to {T}\left({D}{+}_{ℎ}{C}\right)={T}\left({C}{+}_{ℎ}{D}\right)$
11 10 3adant3 ${⊢}\left({D}\in {B}\wedge {C}\in {A}\wedge {B}\cap {A}={0}_{ℋ}\right)\to {T}\left({D}{+}_{ℎ}{C}\right)={T}\left({C}{+}_{ℎ}{D}\right)$
12 2 1 shscomi ${⊢}{B}{+}_{ℋ}{A}={A}{+}_{ℋ}{B}$
13 2 sheli ${⊢}{w}\in {B}\to {w}\in ℋ$
14 1 sheli ${⊢}{z}\in {A}\to {z}\in ℋ$
15 ax-hvcom ${⊢}\left({w}\in ℋ\wedge {z}\in ℋ\right)\to {w}{+}_{ℎ}{z}={z}{+}_{ℎ}{w}$
16 13 14 15 syl2an ${⊢}\left({w}\in {B}\wedge {z}\in {A}\right)\to {w}{+}_{ℎ}{z}={z}{+}_{ℎ}{w}$
17 16 eqeq2d ${⊢}\left({w}\in {B}\wedge {z}\in {A}\right)\to \left({x}={w}{+}_{ℎ}{z}↔{x}={z}{+}_{ℎ}{w}\right)$
18 17 rexbidva ${⊢}{w}\in {B}\to \left(\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}={w}{+}_{ℎ}{z}↔\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{w}\right)$
19 18 riotabiia ${⊢}\left(\iota {w}\in {B}|\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}={w}{+}_{ℎ}{z}\right)=\left(\iota {w}\in {B}|\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{w}\right)$
20 12 19 mpteq12i ${⊢}\left({x}\in \left({B}{+}_{ℋ}{A}\right)⟼\left(\iota {w}\in {B}|\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}={w}{+}_{ℎ}{z}\right)\right)=\left({x}\in \left({A}{+}_{ℋ}{B}\right)⟼\left(\iota {w}\in {B}|\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}={z}{+}_{ℎ}{w}\right)\right)$
21 3 20 eqtr4i ${⊢}{T}=\left({x}\in \left({B}{+}_{ℋ}{A}\right)⟼\left(\iota {w}\in {B}|\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{x}={w}{+}_{ℎ}{z}\right)\right)$
22 2 1 21 cdj3lem2 ${⊢}\left({D}\in {B}\wedge {C}\in {A}\wedge {B}\cap {A}={0}_{ℋ}\right)\to {T}\left({D}{+}_{ℎ}{C}\right)={D}$
23 11 22 eqtr3d ${⊢}\left({D}\in {B}\wedge {C}\in {A}\wedge {B}\cap {A}={0}_{ℋ}\right)\to {T}\left({C}{+}_{ℎ}{D}\right)={D}$
24 5 23 syl3an3b ${⊢}\left({D}\in {B}\wedge {C}\in {A}\wedge {A}\cap {B}={0}_{ℋ}\right)\to {T}\left({C}{+}_{ℎ}{D}\right)={D}$
25 24 3com12 ${⊢}\left({C}\in {A}\wedge {D}\in {B}\wedge {A}\cap {B}={0}_{ℋ}\right)\to {T}\left({C}{+}_{ℎ}{D}\right)={D}$