HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  cdj3lem3 Structured version   Visualization version   GIF version

Theorem cdj3lem3 29598
Description: Lemma for cdj3i 29601. Value of the second-component function 𝑇. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
Hypotheses
Ref Expression
cdj3lem2.1 𝐴S
cdj3lem2.2 𝐵S
cdj3lem3.3 𝑇 = (𝑥 ∈ (𝐴 + 𝐵) ↦ (𝑤𝐵𝑧𝐴 𝑥 = (𝑧 + 𝑤)))
Assertion
Ref Expression
cdj3lem3 ((𝐶𝐴𝐷𝐵 ∧ (𝐴𝐵) = 0) → (𝑇‘(𝐶 + 𝐷)) = 𝐷)
Distinct variable groups:   𝑥,𝑧,𝑤,𝐴   𝑥,𝐵,𝑧,𝑤   𝑥,𝐶,𝑧,𝑤   𝑥,𝐷,𝑧,𝑤
Allowed substitution hints:   𝑇(𝑥,𝑧,𝑤)

Proof of Theorem cdj3lem3
StepHypRef Expression
1 incom 3940 . . . 4 (𝐴𝐵) = (𝐵𝐴)
21eqeq1i 2757 . . 3 ((𝐴𝐵) = 0 ↔ (𝐵𝐴) = 0)
3 cdj3lem2.2 . . . . . . . 8 𝐵S
43sheli 28372 . . . . . . 7 (𝐷𝐵𝐷 ∈ ℋ)
5 cdj3lem2.1 . . . . . . . 8 𝐴S
65sheli 28372 . . . . . . 7 (𝐶𝐴𝐶 ∈ ℋ)
7 ax-hvcom 28159 . . . . . . 7 ((𝐷 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐷 + 𝐶) = (𝐶 + 𝐷))
84, 6, 7syl2an 495 . . . . . 6 ((𝐷𝐵𝐶𝐴) → (𝐷 + 𝐶) = (𝐶 + 𝐷))
98fveq2d 6348 . . . . 5 ((𝐷𝐵𝐶𝐴) → (𝑇‘(𝐷 + 𝐶)) = (𝑇‘(𝐶 + 𝐷)))
1093adant3 1126 . . . 4 ((𝐷𝐵𝐶𝐴 ∧ (𝐵𝐴) = 0) → (𝑇‘(𝐷 + 𝐶)) = (𝑇‘(𝐶 + 𝐷)))
11 cdj3lem3.3 . . . . . 6 𝑇 = (𝑥 ∈ (𝐴 + 𝐵) ↦ (𝑤𝐵𝑧𝐴 𝑥 = (𝑧 + 𝑤)))
123, 5shscomi 28523 . . . . . . 7 (𝐵 + 𝐴) = (𝐴 + 𝐵)
133sheli 28372 . . . . . . . . . . 11 (𝑤𝐵𝑤 ∈ ℋ)
145sheli 28372 . . . . . . . . . . 11 (𝑧𝐴𝑧 ∈ ℋ)
15 ax-hvcom 28159 . . . . . . . . . . 11 ((𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑤 + 𝑧) = (𝑧 + 𝑤))
1613, 14, 15syl2an 495 . . . . . . . . . 10 ((𝑤𝐵𝑧𝐴) → (𝑤 + 𝑧) = (𝑧 + 𝑤))
1716eqeq2d 2762 . . . . . . . . 9 ((𝑤𝐵𝑧𝐴) → (𝑥 = (𝑤 + 𝑧) ↔ 𝑥 = (𝑧 + 𝑤)))
1817rexbidva 3179 . . . . . . . 8 (𝑤𝐵 → (∃𝑧𝐴 𝑥 = (𝑤 + 𝑧) ↔ ∃𝑧𝐴 𝑥 = (𝑧 + 𝑤)))
1918riotabiia 6783 . . . . . . 7 (𝑤𝐵𝑧𝐴 𝑥 = (𝑤 + 𝑧)) = (𝑤𝐵𝑧𝐴 𝑥 = (𝑧 + 𝑤))
2012, 19mpteq12i 4886 . . . . . 6 (𝑥 ∈ (𝐵 + 𝐴) ↦ (𝑤𝐵𝑧𝐴 𝑥 = (𝑤 + 𝑧))) = (𝑥 ∈ (𝐴 + 𝐵) ↦ (𝑤𝐵𝑧𝐴 𝑥 = (𝑧 + 𝑤)))
2111, 20eqtr4i 2777 . . . . 5 𝑇 = (𝑥 ∈ (𝐵 + 𝐴) ↦ (𝑤𝐵𝑧𝐴 𝑥 = (𝑤 + 𝑧)))
223, 5, 21cdj3lem2 29595 . . . 4 ((𝐷𝐵𝐶𝐴 ∧ (𝐵𝐴) = 0) → (𝑇‘(𝐷 + 𝐶)) = 𝐷)
2310, 22eqtr3d 2788 . . 3 ((𝐷𝐵𝐶𝐴 ∧ (𝐵𝐴) = 0) → (𝑇‘(𝐶 + 𝐷)) = 𝐷)
242, 23syl3an3b 1508 . 2 ((𝐷𝐵𝐶𝐴 ∧ (𝐴𝐵) = 0) → (𝑇‘(𝐶 + 𝐷)) = 𝐷)
25243com12 1117 1 ((𝐶𝐴𝐷𝐵 ∧ (𝐴𝐵) = 0) → (𝑇‘(𝐶 + 𝐷)) = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1624  wcel 2131  wrex 3043  cin 3706  cmpt 4873  cfv 6041  crio 6765  (class class class)co 6805  chil 28077   + cva 28078   S csh 28086   + cph 28089  0c0h 28093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-hilex 28157  ax-hfvadd 28158  ax-hvcom 28159  ax-hvass 28160  ax-hv0cl 28161  ax-hvaddid 28162  ax-hfvmul 28163  ax-hvmulid 28164  ax-hvmulass 28165  ax-hvdistr1 28166  ax-hvdistr2 28167  ax-hvmul0 28168
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-po 5179  df-so 5180  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-er 7903  df-en 8114  df-dom 8115  df-sdom 8116  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-grpo 27648  df-ablo 27700  df-hvsub 28129  df-sh 28365  df-ch0 28411  df-shs 28468
This theorem is referenced by:  cdj3lem3a  29599  cdj3i  29601
  Copyright terms: Public domain W3C validator